Fix string non empty option

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -85,6 +85,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
     object_factory_parameters.max_nondet_string_length =
       safe_string2size_t(cmd.get_value("max-nondet-string-length"));
   }
+  if(cmd.isset("string-non-empty"))
+    object_factory_parameters.min_nondet_string_length = 1;
 
   object_factory_parameters.string_printable = cmd.isset("string-printable");
   if(cmd.isset("java-max-vla-length"))

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -573,6 +573,7 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
 bool initialize_nondet_string_fields(
   struct_exprt &struct_expr,
   code_blockt &code,
+  const std::size_t &min_nondet_string_length,
   const std::size_t &max_nondet_string_length,
   const source_locationt &loc,
   const irep_idt &function_id,
@@ -627,11 +628,10 @@ bool initialize_nondet_string_fields(
   code.add(code_declt(length_expr));
   code.add(code_assignt(length_expr, nondet_length));
 
-  // assume (length_expr >= 0);
-  code.add(
-    code_assumet(
-      binary_relation_exprt(
-        length_expr, ID_ge, from_integer(0, java_int_type()))));
+  // assume (length_expr >= min_nondet_string_length);
+  const exprt min_length =
+    from_integer(min_nondet_string_length, java_int_type());
+  code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length)));
 
   // assume (length_expr <= max_input_length)
   if(max_nondet_string_length <= max_value(length_expr.type()))
@@ -1048,6 +1048,7 @@ void java_object_factoryt::gen_nondet_struct_init(
       initialize_nondet_string_fields(
         to_struct_expr(initial_object),
         assignments,
+        object_factory_parameters.min_nondet_string_length,
         object_factory_parameters.max_nondet_string_length,
         loc,
         object_factory_parameters.function_id,

jbmc/src/java_bytecode/object_factory_parameters.h

@@ -28,6 +28,9 @@ struct object_factory_parameterst final
   /// Maximum value for the non-deterministically-chosen length of a string.
   size_t max_nondet_string_length=MAX_NONDET_STRING_LENGTH;
 
+  /// Maximum value for the non-deterministically-chosen length of a string.
+  size_t min_nondet_string_length = 0;
+
   /// Maximum depth for object hierarchy on input.
   /// Used to prevent object factory to loop infinitely during the
   /// generation of code that allocates/initializes data structures of recursive