diff --git a/jbmc/regression/CMakeLists.txt b/jbmc/regression/CMakeLists.txt index 33d5ce64a0f..efc2260903a 100644 --- a/jbmc/regression/CMakeLists.txt +++ b/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) diff --git a/jbmc/regression/Makefile b/jbmc/regression/Makefile index 42a479942e2..74625373415 100644 --- a/jbmc/regression/Makefile +++ b/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 \ diff --git a/jbmc/regression/janalyzer/CMakeLists.txt b/jbmc/regression/janalyzer/CMakeLists.txt new file mode 100644 index 00000000000..d8ebffaf7de --- /dev/null +++ b/jbmc/regression/janalyzer/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "$" +) diff --git a/jbmc/regression/janalyzer/Makefile b/jbmc/regression/janalyzer/Makefile new file mode 100644 index 00000000000..7b513b64647 --- /dev/null +++ b/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 diff --git a/jbmc/regression/janalyzer/string-initializer/Basic1.class b/jbmc/regression/janalyzer/string-initializer/Basic1.class new file mode 100644 index 00000000000..49e41ebb0be Binary files /dev/null and b/jbmc/regression/janalyzer/string-initializer/Basic1.class differ diff --git a/jbmc/regression/janalyzer/string-initializer/Basic1.java b/jbmc/regression/janalyzer/string-initializer/Basic1.java new file mode 100644 index 00000000000..b70ad5c2bce --- /dev/null +++ b/jbmc/regression/janalyzer/string-initializer/Basic1.java @@ -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!"); + } +}; + diff --git a/jbmc/regression/janalyzer/string-initializer/test.desc b/jbmc/regression/janalyzer/string-initializer/test.desc new file mode 100644 index 00000000000..a7cb9b3b1c7 --- /dev/null +++ b/jbmc/regression/janalyzer/string-initializer/test.desc @@ -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 diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index d4845f12489..26feac02184 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -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); } diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index 654f7058a9a..1493fdcfd6e 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.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);