Add test for string initializers

Author: Owen Jones

jbmc/regression/CMakeLists.txt

@@ -7,6 +7,7 @@ add_subdirectory(jbmc)
 add_subdirectory(strings-smoke-tests)
 add_subdirectory(jbmc-strings)
 add_subdirectory(jdiff)
+add_subdirectory(janalyzer)
 add_subdirectory(janalyzer-taint)
 add_subdirectory(jbmc-concurrency)
 add_subdirectory(jbmc-inheritance)

jbmc/regression/Makefile

@@ -1,7 +1,8 @@
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are
 # listed with decreasing runtimes (i.e. longest running at the top)
-DIRS = janalyzer-taint \
+DIRS = janalyzer \
+       janalyzer-taint \
        jbmc \
        jbmc-concurrency \
        jbmc-inheritance \

jbmc/regression/janalyzer/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:janalyzer>"
+)

jbmc/regression/janalyzer/Makefile

@@ -0,0 +1,21 @@
+default: tests.log
+
+include ../../src/config.inc
+
+test:
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
+
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
+
+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

jbmc/regression/janalyzer/string-initializer/Basic1.class

@@ -0,0 +1,10 @@
+class Basic1
+{
+    public static void main(String[] args) {
+        String s = "Hello ";
+        s +=  "World!";
+        if(s.equals("Hello World!"))
+            System.out.printf("Hello World!");
+    }
+};
+

jbmc/regression/janalyzer/string-initializer/Basic1.java

@@ -0,0 +1,9 @@
+CORE
+Basic1.class
+--location-sensitive --constants --show
+^EXIT=0$
+^SIGNAL=0$
+Hello_20 = \{ \.@class_identifier="java::java\.lang\.String" \};
+java::java\.lang\.String\.Literal\.Hello_20=\{ \.@class_identifier="java::java\.lang\.String" \}
+--
+^warning: ignoring