Fix a bug with class identifier of nondet strings TG-1581

regression/jbmc-strings/instanceof/Test.java

@@ -0,0 +1,9 @@
+public class Test {
+
+    public static String check(String s) {
+        if (s == null)
+            return "null";
+        assert(s instanceof String);
+        return "non-null";
+    }
+}

regression/jbmc-strings/instanceof/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --function Test.check
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 6 .* SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--

src/java_bytecode/java_object_factory.cpp

@@ -554,7 +554,7 @@ codet initialize_nondet_string_struct(
 
   // `obj` is `*expr`
   const struct_typet &struct_type = to_struct_type(ns.follow(obj.type()));
-  const irep_idt &class_id = struct_type.get_tag();
+  const irep_idt &class_id = "java::" + id2string(struct_type.get_tag());
 
   // @clsid = String and @lock = false:
   const symbol_typet jlo_symbol("java::java.lang.Object");

src/java_bytecode/java_root_class.cpp

@@ -57,7 +57,8 @@ void java_root_class(symbolt &class_symbol)
 /// \param jlo [out] : object to initialize
 /// \param root_type: type of the root class
 /// \param lock: lock field
-/// \param class_identifier: class identifier field
+/// \param class_identifier: class identifier field, generally begins with
+///        "java::" prefix.
 void java_root_class_init(
   struct_exprt &jlo,
   const struct_typet &root_type,

unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

@@ -79,7 +79,7 @@ SCENARIO(
           "return_array = cprover_associate_length_to_array_func"
           "(nondet_infinite_array, tmp_object_factory);",
           "arg = { [email protected]={ .@class_identifier"
-          "=\"java.lang.String\", .@lock=false },"
+          "=\"java::java.lang.String\", .@lock=false },"
           " .length=tmp_object_factory, "
           ".data=nondet_infinite_array };"};