Merge pull request #212 from smowton/java_clsid_fix

Java clsid fix

Author: Daniel Kroening

regression/cbmc-java/virtual5/child.class

@@ -0,0 +1,6 @@
+CORE
+virtual5.class
+--function virtual5.test
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

regression/cbmc-java/virtual5/parent.class

@@ -0,0 +1,23 @@
+public class virtual5 {
+
+  public static void test(parent p, child c) {
+
+    if(p==null)
+      return;
+    assert(p.get()==1);
+
+  }
+
+}
+
+class parent {
+
+  public int get() { return 1; }
+
+}
+
+class child extends parent {
+
+  public int get() { return 2; }
+
+}

regression/cbmc-java/virtual5/test.desc

@@ -111,7 +111,8 @@ void gen_nondet_init(
 
       if(name=="@class_identifier")
       {
-        constant_exprt ci(class_identifier, string_typet());
+        irep_idt qualified_clsid="java::"+as_string(class_identifier);
+	constant_exprt ci(qualified_clsid,string_typet());
 
         code_assignt code(me, ci);
         init_code.copy_to_operands(code);