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