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

Previously this would incorrectly leave a branch on which the object was not
initialised at all. Now it is always initialised, falling back to conventional
initialisation when string-specific init is not possible.

Author: smowton

regression/cbmc-java/NondetCharSequence/NondetCharSequence.class

@@ -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/NondetCharSequence.java

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

regression/cbmc-java/NondetCharSequence/test.desc

@@ -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/NondetString.class

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

regression/cbmc-java/NondetString/NondetString.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/NondetString/test.desc

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

regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class

@@ -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/NondetStringBuffer/NondetStringBuffer.java

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

regression/cbmc-java/NondetStringBuffer/test.desc

@@ -841,20 +841,19 @@ 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()))
-  {
-    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
+  // 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.
+  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))
   {
     gen_pointer_target_init(
       non_null_inst,