Test symex can resolve class identifier

Test that symex knows the class identifier of nondet-initialised inputs
to the entrypoint function.

Author: Owen

jbmc/regression/jbmc/symex_should_resolve_class_identifiers/Test$A.class

@@ -0,0 +1,23 @@
+public class Test {
+
+    public static class A {
+        public int getInteger() {
+            return 0;
+        }
+    }
+
+    public static class B extends A {
+        public int getInteger() {
+            return 1;
+        }
+    }
+
+    public static void test(A a) {
+        // Need to instantiate B to make sure it's loaded
+        B dummyB = new B();
+
+        int zero = a.getInteger();
+        assert(zero == 2);
+    }
+
+}

jbmc/regression/jbmc/symex_should_resolve_class_identifiers/Test$B.class

@@ -0,0 +1,16 @@
+CORE
+Test.class
+--function Test.test --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+--
+java::Test\$B\.getInteger
+^warning: ignoring
+--
+Symex should have the values of all class_identifier fields in its constant
+propagation map, so that it can run efficiently and create a simpler equation.
+If an argument to the entrypoint is nondet-initialised using automatic local
+initialisation then symex thinks its class identifier might be uninitialised,
+and hence could be anything, because that's what happens in the null case (but
+we never access the class identifier in this case). Hence we have switched to
+dynamic allocation for this situation.