Add test for CProver.classIdentifier

This tests that the new builtin cprover function is working.

Author: romainbrenguier

jbmc/regression/jbmc/classIdentifier/Test.class

@@ -0,0 +1,20 @@
+public class Test {
+  public String check(int assertId) {
+    Object o;
+    o = "foo";
+    String classId = org.cprover.CProver.classIdentifier(o);
+    if(assertId == 1) {
+      assert org.cprover.CProverString.equals(classId, "java.lang.String");
+    } else if(assertId == 2) {
+      assert org.cprover.CProverString.equals(classId, "java.lang.Integer");
+    }
+    o = new Integer(42);
+    classId = org.cprover.CProver.classIdentifier(o);
+    if(assertId == 3) {
+      assert org.cprover.CProverString.equals(classId, "java.lang.String");
+    } else if(assertId == 4) {
+      assert org.cprover.CProverString.equals(classId, "java.lang.Integer");
+    }
+    return classId;
+  }
+}

jbmc/regression/jbmc/classIdentifier/Test.java

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.check --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 7 .*: SUCCESS
+assertion at file Test.java line 9 .*: FAILURE
+assertion at file Test.java line 14 .*: FAILURE
+assertion at file Test.java line 16 .*: SUCCESS