Add a printable option to string initialization

This will force characters to be printable when the string is
initialized.
This is set to false by default for now, but should then be activated
when string-printable is given.

Author: romainbrenguier

src/java_bytecode/java_object_factory.cpp

@@ -542,7 +542,8 @@ codet initialize_nondet_string_struct(
   const exprt &obj,
   const std::size_t &max_nondet_string_length,
   const source_locationt &loc,
-  symbol_tablet &symbol_table)
+  symbol_tablet &symbol_table,
+  bool printable)
 {
   PRECONDITION(
     java_string_library_preprocesst::implements_java_char_sequence(obj.type()));
@@ -605,6 +606,13 @@ codet initialize_nondet_string_struct(
 
     add_array_to_length_association(
       data_expr, length_expr, symbol_table, loc, code);
+
+    // Printable ASCII characters are between ' ' and '~'.
+    if(printable)
+    {
+      add_character_set_constraint(
+        array_pointer, length_expr, " -~", symbol_table, loc, code);
+    }
   }
 
   // tmp_object = struct_expr;

src/java_bytecode/java_object_factory.h

@@ -156,6 +156,7 @@ codet initialize_nondet_string_struct(
   const exprt &obj,
   const std::size_t &max_nondet_string_length,
   const source_locationt &loc,
-  symbol_tablet &symbol_table);
+  symbol_tablet &symbol_table,
+  bool printable = false);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H