Merge pull request #3657 from owen-jones-diffblue/fix-string-initialiser-type

Fix String initialiser type when java.lang.String is a stub

Author: owen-jones-diffblue

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

jbmc/regression/janalyzer/string-initializer/test.desc

@@ -66,6 +66,8 @@ janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
 
 void janalyzer_parse_optionst::register_languages()
 {
+  // Need ansi C language for __CPROVER_rounding_mode
+  register_language(new_ansi_c_language);
   register_language(new_java_bytecode_language);
 }
 

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -204,6 +204,7 @@ symbol_exprt get_or_create_string_literal_symbol(
     // Case where java.lang.String was stubbed, and so directly defines
     // @class_identifier
     new_symbol.value = jlo_init;
+    new_symbol.value.type() = string_type;
   }
 
   bool add_failed = symbol_table.add(new_symbol);