Add tests for generic type erasure

Ensure that moving generic type information out of a comment doesn't
cause type errors.

Author: thk123

jbmc/regression/CMakeLists.txt

@@ -11,3 +11,4 @@ add_subdirectory(janalyzer-taint)
 add_subdirectory(jbmc-concurrency)
 add_subdirectory(jbmc-inheritance)
 add_subdirectory(jbmc-cover)
+add_subdirectory(generics)

jbmc/regression/Makefile

@@ -9,6 +9,7 @@ DIRS = janalzyer-taint \
        jbmc-strings \
        jdiff \
        string-smoke-tests \
+       generics \
        # Empty last line
 
 # Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks

jbmc/regression/generics/CMakeLists.txt

@@ -0,0 +1,10 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:jbmc>"
+)
+
+add_test_pl_profile(
+    "jbmc-symex-driven-lazy-loading"
+    "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
+    "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
+    "CORE"
+)

jbmc/regression/generics/Makefile

@@ -0,0 +1,36 @@
+default: tests.log
+
+include ../../src/config.inc
+
+test:
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+
+%.class: %.java ../../src/org.cprover.jar
+	javac -g -cp ../../src/org.cprover.jar:. $<
+
+nondet_java_files := $(shell find . -name "Nondet*.java")
+nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files))
+
+.PHONY: nondet-class-files
+nondet-class-files: $(nondet_class_files)
+
+.PHONY: clean-nondet-class-files
+clean-nondet-class-files:
+	-rm $(nondet_class_files)

jbmc/regression/generics/type_erasure/BWrapper.class

@@ -0,0 +1,35 @@
+class Gen<T> {
+  public T t;
+}
+
+class IWrapper {
+  public int i;
+}
+
+class BWrapper {
+  public boolean b;
+}
+
+class TestClass {
+  static void testFunction() {
+    Gen<IWrapper> a = new Gen<>();
+    Gen b = a;
+    assert(b ==  a);
+    Gen<BWrapper> c;
+    c = b;
+    assert(c == b);
+    // below assertion is incorrectly labelled as failure
+    // assert(c.equals(a));
+  }
+
+  static void testFunctionWithInput(Gen a, Gen<IWrapper> b, Gen<BWrapper> c) {
+    if(a != null && b != null && c != null &&
+      a.t != null && b.t != null && c.t != null)
+    {
+      b = a;
+      assert(b == a);
+      a = c;
+      assert(a == c);
+    }
+  }
+}

jbmc/regression/generics/type_erasure/Gen.class

@@ -0,0 +1,6 @@
+CORE
+TestClass.class
+--function TestClass.testFunction
+EXIT=0
+SIGNAL=0
+VERIFICATION SUCCESSFUL

jbmc/regression/generics/type_erasure/IWrapper.class

@@ -0,0 +1,6 @@
+CORE
+TestClass.class
+--function TestClass.testFunctionWithInput
+EXIT=0
+SIGNAL=0
+VERIFICATION SUCCESSFUL