Fix String type initialisation when --refine-strings is not active

regression/cbmc-java/NondetCharSequence/NondetCharSequence.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetCharSequence
+{
+  static void main()
+  {
+    CharSequence x = CProver.nondetWithNull();
+    assert x == null || x instanceof CharSequence;
+  }
+}

regression/cbmc-java/NondetCharSequence/test.desc

@@ -0,0 +1,8 @@
+CORE
+NondetCharSequence.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-java/NondetString/NondetString.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetString
+{
+  static void main()
+  {
+    String x = CProver.nondetWithNull();
+    assert x == null || x instanceof String;
+  }
+}

regression/cbmc-java/NondetString/test.desc

@@ -0,0 +1,8 @@
+CORE
+NondetString.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetStringBuffer
+{
+  static void main()
+  {
+    StringBuffer x = CProver.nondetWithNull();
+    assert x == null || x instanceof StringBuffer;
+  }
+}

regression/cbmc-java/NondetStringBuffer/test.desc

@@ -0,0 +1,8 @@
+CORE
+NondetStringBuffer.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class NondetStringBuilder
+{
+  static void main()
+  {
+    StringBuilder x = CProver.nondetWithNull();
+    assert x == null || x instanceof StringBuilder;
+  }
+}

regression/cbmc-java/NondetStringBuilder/test.desc

@@ -0,0 +1,8 @@
+CORE
+NondetStringBuilder.class
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/java_bytecode/java_object_factory.cpp

@@ -841,20 +841,27 @@ void java_object_factoryt::gen_nondet_pointer_init(
   // and asign to `expr` the address of such object
   code_blockt non_null_inst;
 
-  if(
-    java_string_library_preprocesst::implements_java_char_sequence_pointer(
-      expr.type()))
+  // Note string-type-specific initialization might fail, e.g. if java.lang.CharSequence does not
+  // have the expected fields (typically this happens if --refine-strings was not passed). In this
+  // case we fall back to normal pointer target init.
+
+  bool string_init_succeeded = false;
+
+  if(java_string_library_preprocesst::implements_java_char_sequence_pointer(
+       expr.type()))
   {
-    add_nondet_string_pointer_initialization(
-      expr,
-      object_factory_parameters.max_nondet_string_length,
-      object_factory_parameters.string_printable,
-      symbol_table,
-      loc,
-      object_factory_parameters.function_id,
-      assignments);
+    string_init_succeeded =
+      !add_nondet_string_pointer_initialization(
+        expr,
+        object_factory_parameters.max_nondet_string_length,
+        object_factory_parameters.string_printable,
+        symbol_table,
+        loc,
+        object_factory_parameters.function_id,
+        assignments);
   }
-  else
+
+  if(!string_init_succeeded)
   {
     gen_pointer_target_init(
       non_null_inst,