diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 58558146ecd..e3bf553e7c5 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -35,6 +35,7 @@ add_subdirectory(goto-diff) add_subdirectory(goto-instrument) add_subdirectory(goto-instrument-typedef) add_subdirectory(invariants) +add_subdirectory(jbmc-strings) add_subdirectory(strings) add_subdirectory(strings-smoke-tests) add_subdirectory(test-script) diff --git a/regression/Makefile b/regression/Makefile index 418a2501dde..025c9127ccd 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -14,6 +14,7 @@ DIRS = ansi-c \ goto-instrument-typedef \ invariants \ strings \ + jbmc-strings \ strings-smoke-tests \ test-script \ # Empty last line diff --git a/regression/cbmc-java-inheritance/CMakeLists.txt b/regression/cbmc-java-inheritance/CMakeLists.txt index 93d5ee716c2..afe0ea5761a 100644 --- a/regression/cbmc-java-inheritance/CMakeLists.txt +++ b/regression/cbmc-java-inheritance/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$" ) diff --git a/regression/cbmc-java-inheritance/Makefile b/regression/cbmc-java-inheritance/Makefile index dcdf752aea1..2aa697dd691 100644 --- a/regression/cbmc-java-inheritance/Makefile +++ b/regression/cbmc-java-inheritance/Makefile @@ -1,13 +1,13 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ ../failed-tests-printer.pl ; \ exit 1 ; \ fi tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ ../failed-tests-printer.pl ; \ exit 1 ; \ fi diff --git a/regression/cbmc-java/CMakeLists.txt b/regression/cbmc-java/CMakeLists.txt index 93d5ee716c2..afe0ea5761a 100644 --- a/regression/cbmc-java/CMakeLists.txt +++ b/regression/cbmc-java/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$" ) diff --git a/regression/cbmc-java/Makefile b/regression/cbmc-java/Makefile index dcdf752aea1..2aa697dd691 100644 --- a/regression/cbmc-java/Makefile +++ b/regression/cbmc-java/Makefile @@ -1,13 +1,13 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ ../failed-tests-printer.pl ; \ exit 1 ; \ fi tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ ../failed-tests-printer.pl ; \ exit 1 ; \ fi diff --git a/regression/cbmc/trace_class_identifier/TestGenTest.class b/regression/cbmc-java/trace_class_identifier/TestGenTest.class similarity index 100% rename from regression/cbmc/trace_class_identifier/TestGenTest.class rename to regression/cbmc-java/trace_class_identifier/TestGenTest.class diff --git a/regression/cbmc/trace_class_identifier/TestGenTest.java b/regression/cbmc-java/trace_class_identifier/TestGenTest.java similarity index 100% rename from regression/cbmc/trace_class_identifier/TestGenTest.java rename to regression/cbmc-java/trace_class_identifier/TestGenTest.java diff --git a/regression/cbmc/trace_class_identifier/test.desc b/regression/cbmc-java/trace_class_identifier/test.desc similarity index 100% rename from regression/cbmc/trace_class_identifier/test.desc rename to regression/cbmc-java/trace_class_identifier/test.desc diff --git a/regression/cbmc-cover/unique-bytecode1/Test.class b/regression/jbmc-cover/unique-bytecode1/Test.class similarity index 100% rename from regression/cbmc-cover/unique-bytecode1/Test.class rename to regression/jbmc-cover/unique-bytecode1/Test.class diff --git a/regression/cbmc-cover/unique-bytecode1/Test.java b/regression/jbmc-cover/unique-bytecode1/Test.java similarity index 100% rename from regression/cbmc-cover/unique-bytecode1/Test.java rename to regression/jbmc-cover/unique-bytecode1/Test.java diff --git a/regression/cbmc-cover/unique-bytecode1/test.desc b/regression/jbmc-cover/unique-bytecode1/test.desc similarity index 100% rename from regression/cbmc-cover/unique-bytecode1/test.desc rename to regression/jbmc-cover/unique-bytecode1/test.desc diff --git a/regression/cbmc-cover/unique-bytecode2/Test.class b/regression/jbmc-cover/unique-bytecode2/Test.class similarity index 100% rename from regression/cbmc-cover/unique-bytecode2/Test.class rename to regression/jbmc-cover/unique-bytecode2/Test.class diff --git a/regression/cbmc-cover/unique-bytecode2/Test.java b/regression/jbmc-cover/unique-bytecode2/Test.java similarity index 100% rename from regression/cbmc-cover/unique-bytecode2/Test.java rename to regression/jbmc-cover/unique-bytecode2/Test.java diff --git a/regression/cbmc-cover/unique-bytecode2/test.desc b/regression/jbmc-cover/unique-bytecode2/test.desc similarity index 100% rename from regression/cbmc-cover/unique-bytecode2/test.desc rename to regression/jbmc-cover/unique-bytecode2/test.desc diff --git a/regression/cbmc-cover/unique-bytecode3/Test.class b/regression/jbmc-cover/unique-bytecode3/Test.class similarity index 100% rename from regression/cbmc-cover/unique-bytecode3/Test.class rename to regression/jbmc-cover/unique-bytecode3/Test.class diff --git a/regression/cbmc-cover/unique-bytecode3/Test.java b/regression/jbmc-cover/unique-bytecode3/Test.java similarity index 100% rename from regression/cbmc-cover/unique-bytecode3/Test.java rename to regression/jbmc-cover/unique-bytecode3/Test.java diff --git a/regression/cbmc-cover/unique-bytecode3/test.desc b/regression/jbmc-cover/unique-bytecode3/test.desc similarity index 100% rename from regression/cbmc-cover/unique-bytecode3/test.desc rename to regression/jbmc-cover/unique-bytecode3/test.desc diff --git a/regression/jbmc-strings/CMakeLists.txt b/regression/jbmc-strings/CMakeLists.txt new file mode 100644 index 00000000000..afe0ea5761a --- /dev/null +++ b/regression/jbmc-strings/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "$" +) diff --git a/regression/strings/CharacterGetNumericValue/test.class b/regression/jbmc-strings/CharacterGetNumericValue/test.class similarity index 100% rename from regression/strings/CharacterGetNumericValue/test.class rename to regression/jbmc-strings/CharacterGetNumericValue/test.class diff --git a/regression/strings/CharacterGetNumericValue/test.desc b/regression/jbmc-strings/CharacterGetNumericValue/test.desc similarity index 100% rename from regression/strings/CharacterGetNumericValue/test.desc rename to regression/jbmc-strings/CharacterGetNumericValue/test.desc diff --git a/regression/strings/CharacterGetNumericValue/test.java b/regression/jbmc-strings/CharacterGetNumericValue/test.java similarity index 100% rename from regression/strings/CharacterGetNumericValue/test.java rename to regression/jbmc-strings/CharacterGetNumericValue/test.java diff --git a/regression/jbmc-strings/Makefile b/regression/jbmc-strings/Makefile new file mode 100644 index 00000000000..e45465e6130 --- /dev/null +++ b/regression/jbmc-strings/Makefile @@ -0,0 +1,38 @@ +default: tests.log + +test: + @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +testfuture: + @if ! ../test.pl -c ../../../src/jbmc/jbmc -CF ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +testall: + @if ! ../test.pl -c ../../../src/jbmc/jbmc -CFTK ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +tests.log: ../test.pl + @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ + ../failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + $(RM) tests.log + diff --git a/regression/strings/RegexMatches01/RegexMatches01.class b/regression/jbmc-strings/RegexMatches01/RegexMatches01.class similarity index 100% rename from regression/strings/RegexMatches01/RegexMatches01.class rename to regression/jbmc-strings/RegexMatches01/RegexMatches01.class diff --git a/regression/strings/RegexMatches01/RegexMatches01.java b/regression/jbmc-strings/RegexMatches01/RegexMatches01.java similarity index 100% rename from regression/strings/RegexMatches01/RegexMatches01.java rename to regression/jbmc-strings/RegexMatches01/RegexMatches01.java diff --git a/regression/strings/RegexMatches01/test.desc b/regression/jbmc-strings/RegexMatches01/test.desc similarity index 100% rename from regression/strings/RegexMatches01/test.desc rename to regression/jbmc-strings/RegexMatches01/test.desc diff --git a/regression/strings/RegexMatches02/RegexMatches02.class b/regression/jbmc-strings/RegexMatches02/RegexMatches02.class similarity index 100% rename from regression/strings/RegexMatches02/RegexMatches02.class rename to regression/jbmc-strings/RegexMatches02/RegexMatches02.class diff --git a/regression/strings/RegexMatches02/RegexMatches02.java b/regression/jbmc-strings/RegexMatches02/RegexMatches02.java similarity index 100% rename from regression/strings/RegexMatches02/RegexMatches02.java rename to regression/jbmc-strings/RegexMatches02/RegexMatches02.java diff --git a/regression/strings/RegexMatches02/test.desc b/regression/jbmc-strings/RegexMatches02/test.desc similarity index 100% rename from regression/strings/RegexMatches02/test.desc rename to regression/jbmc-strings/RegexMatches02/test.desc diff --git a/regression/strings/RegexSubstitution01/RegexSubstitution01.class b/regression/jbmc-strings/RegexSubstitution01/RegexSubstitution01.class similarity index 100% rename from regression/strings/RegexSubstitution01/RegexSubstitution01.class rename to regression/jbmc-strings/RegexSubstitution01/RegexSubstitution01.class diff --git a/regression/strings/RegexSubstitution01/RegexSubstitution01.java b/regression/jbmc-strings/RegexSubstitution01/RegexSubstitution01.java similarity index 100% rename from regression/strings/RegexSubstitution01/RegexSubstitution01.java rename to regression/jbmc-strings/RegexSubstitution01/RegexSubstitution01.java diff --git a/regression/strings/RegexSubstitution01/test.desc b/regression/jbmc-strings/RegexSubstitution01/test.desc similarity index 100% rename from regression/strings/RegexSubstitution01/test.desc rename to regression/jbmc-strings/RegexSubstitution01/test.desc diff --git a/regression/strings/RegexSubstitution02/RegexSubstitution02.class b/regression/jbmc-strings/RegexSubstitution02/RegexSubstitution02.class similarity index 100% rename from regression/strings/RegexSubstitution02/RegexSubstitution02.class rename to regression/jbmc-strings/RegexSubstitution02/RegexSubstitution02.class diff --git a/regression/strings/RegexSubstitution02/RegexSubstitution02.java b/regression/jbmc-strings/RegexSubstitution02/RegexSubstitution02.java similarity index 100% rename from regression/strings/RegexSubstitution02/RegexSubstitution02.java rename to regression/jbmc-strings/RegexSubstitution02/RegexSubstitution02.java diff --git a/regression/strings/RegexSubstitution02/test.desc b/regression/jbmc-strings/RegexSubstitution02/test.desc similarity index 100% rename from regression/strings/RegexSubstitution02/test.desc rename to regression/jbmc-strings/RegexSubstitution02/test.desc diff --git a/regression/strings/RegexSubstitution03/RegexSubstitution03.class b/regression/jbmc-strings/RegexSubstitution03/RegexSubstitution03.class similarity index 100% rename from regression/strings/RegexSubstitution03/RegexSubstitution03.class rename to regression/jbmc-strings/RegexSubstitution03/RegexSubstitution03.class diff --git a/regression/strings/RegexSubstitution03/RegexSubstitution03.java b/regression/jbmc-strings/RegexSubstitution03/RegexSubstitution03.java similarity index 100% rename from regression/strings/RegexSubstitution03/RegexSubstitution03.java rename to regression/jbmc-strings/RegexSubstitution03/RegexSubstitution03.java diff --git a/regression/strings/RegexSubstitution03/test.desc b/regression/jbmc-strings/RegexSubstitution03/test.desc similarity index 100% rename from regression/strings/RegexSubstitution03/test.desc rename to regression/jbmc-strings/RegexSubstitution03/test.desc diff --git a/regression/strings/StaticCharMethods01/StaticCharMethods01.class b/regression/jbmc-strings/StaticCharMethods01/StaticCharMethods01.class similarity index 100% rename from regression/strings/StaticCharMethods01/StaticCharMethods01.class rename to regression/jbmc-strings/StaticCharMethods01/StaticCharMethods01.class diff --git a/regression/strings/StaticCharMethods01/StaticCharMethods01.java b/regression/jbmc-strings/StaticCharMethods01/StaticCharMethods01.java similarity index 100% rename from regression/strings/StaticCharMethods01/StaticCharMethods01.java rename to regression/jbmc-strings/StaticCharMethods01/StaticCharMethods01.java diff --git a/regression/strings/StaticCharMethods01/test.desc b/regression/jbmc-strings/StaticCharMethods01/test.desc similarity index 100% rename from regression/strings/StaticCharMethods01/test.desc rename to regression/jbmc-strings/StaticCharMethods01/test.desc diff --git a/regression/strings/StaticCharMethods02/StaticCharMethods02.class b/regression/jbmc-strings/StaticCharMethods02/StaticCharMethods02.class similarity index 100% rename from regression/strings/StaticCharMethods02/StaticCharMethods02.class rename to regression/jbmc-strings/StaticCharMethods02/StaticCharMethods02.class diff --git a/regression/strings/StaticCharMethods02/StaticCharMethods02.java b/regression/jbmc-strings/StaticCharMethods02/StaticCharMethods02.java similarity index 100% rename from regression/strings/StaticCharMethods02/StaticCharMethods02.java rename to regression/jbmc-strings/StaticCharMethods02/StaticCharMethods02.java diff --git a/regression/strings/StaticCharMethods02/test.desc b/regression/jbmc-strings/StaticCharMethods02/test.desc similarity index 100% rename from regression/strings/StaticCharMethods02/test.desc rename to regression/jbmc-strings/StaticCharMethods02/test.desc diff --git a/regression/strings/StaticCharMethods03/StaticCharMethods03.class b/regression/jbmc-strings/StaticCharMethods03/StaticCharMethods03.class similarity index 100% rename from regression/strings/StaticCharMethods03/StaticCharMethods03.class rename to regression/jbmc-strings/StaticCharMethods03/StaticCharMethods03.class diff --git a/regression/strings/StaticCharMethods03/StaticCharMethods03.java b/regression/jbmc-strings/StaticCharMethods03/StaticCharMethods03.java similarity index 100% rename from regression/strings/StaticCharMethods03/StaticCharMethods03.java rename to regression/jbmc-strings/StaticCharMethods03/StaticCharMethods03.java diff --git a/regression/strings/StaticCharMethods03/test.desc b/regression/jbmc-strings/StaticCharMethods03/test.desc similarity index 100% rename from regression/strings/StaticCharMethods03/test.desc rename to regression/jbmc-strings/StaticCharMethods03/test.desc diff --git a/regression/strings/StaticCharMethods04/StaticCharMethods04.class b/regression/jbmc-strings/StaticCharMethods04/StaticCharMethods04.class similarity index 100% rename from regression/strings/StaticCharMethods04/StaticCharMethods04.class rename to regression/jbmc-strings/StaticCharMethods04/StaticCharMethods04.class diff --git a/regression/strings/StaticCharMethods04/StaticCharMethods04.java b/regression/jbmc-strings/StaticCharMethods04/StaticCharMethods04.java similarity index 100% rename from regression/strings/StaticCharMethods04/StaticCharMethods04.java rename to regression/jbmc-strings/StaticCharMethods04/StaticCharMethods04.java diff --git a/regression/strings/StaticCharMethods04/test.desc b/regression/jbmc-strings/StaticCharMethods04/test.desc similarity index 100% rename from regression/strings/StaticCharMethods04/test.desc rename to regression/jbmc-strings/StaticCharMethods04/test.desc diff --git a/regression/strings/StaticCharMethods05/StaticCharMethods05.class b/regression/jbmc-strings/StaticCharMethods05/StaticCharMethods05.class similarity index 100% rename from regression/strings/StaticCharMethods05/StaticCharMethods05.class rename to regression/jbmc-strings/StaticCharMethods05/StaticCharMethods05.class diff --git a/regression/strings/StaticCharMethods05/StaticCharMethods05.java b/regression/jbmc-strings/StaticCharMethods05/StaticCharMethods05.java similarity index 100% rename from regression/strings/StaticCharMethods05/StaticCharMethods05.java rename to regression/jbmc-strings/StaticCharMethods05/StaticCharMethods05.java diff --git a/regression/strings/StaticCharMethods05/test.desc b/regression/jbmc-strings/StaticCharMethods05/test.desc similarity index 100% rename from regression/strings/StaticCharMethods05/test.desc rename to regression/jbmc-strings/StaticCharMethods05/test.desc diff --git a/regression/strings/StaticCharMethods06/StaticCharMethods06.class b/regression/jbmc-strings/StaticCharMethods06/StaticCharMethods06.class similarity index 100% rename from regression/strings/StaticCharMethods06/StaticCharMethods06.class rename to regression/jbmc-strings/StaticCharMethods06/StaticCharMethods06.class diff --git a/regression/strings/StaticCharMethods06/StaticCharMethods06.java b/regression/jbmc-strings/StaticCharMethods06/StaticCharMethods06.java similarity index 100% rename from regression/strings/StaticCharMethods06/StaticCharMethods06.java rename to regression/jbmc-strings/StaticCharMethods06/StaticCharMethods06.java diff --git a/regression/strings/StaticCharMethods06/test.desc b/regression/jbmc-strings/StaticCharMethods06/test.desc similarity index 100% rename from regression/strings/StaticCharMethods06/test.desc rename to regression/jbmc-strings/StaticCharMethods06/test.desc diff --git a/regression/strings/StringBuilderAppend01/StringBuilderAppend01.class b/regression/jbmc-strings/StringBuilderAppend01/StringBuilderAppend01.class similarity index 100% rename from regression/strings/StringBuilderAppend01/StringBuilderAppend01.class rename to regression/jbmc-strings/StringBuilderAppend01/StringBuilderAppend01.class diff --git a/regression/strings/StringBuilderAppend01/StringBuilderAppend01.java b/regression/jbmc-strings/StringBuilderAppend01/StringBuilderAppend01.java similarity index 100% rename from regression/strings/StringBuilderAppend01/StringBuilderAppend01.java rename to regression/jbmc-strings/StringBuilderAppend01/StringBuilderAppend01.java diff --git a/regression/strings/StringBuilderAppend01/test.desc b/regression/jbmc-strings/StringBuilderAppend01/test.desc similarity index 100% rename from regression/strings/StringBuilderAppend01/test.desc rename to regression/jbmc-strings/StringBuilderAppend01/test.desc diff --git a/regression/strings/StringBuilderAppend02/StringBuilderAppend02.class b/regression/jbmc-strings/StringBuilderAppend02/StringBuilderAppend02.class similarity index 100% rename from regression/strings/StringBuilderAppend02/StringBuilderAppend02.class rename to regression/jbmc-strings/StringBuilderAppend02/StringBuilderAppend02.class diff --git a/regression/strings/StringBuilderAppend02/StringBuilderAppend02.java b/regression/jbmc-strings/StringBuilderAppend02/StringBuilderAppend02.java similarity index 100% rename from regression/strings/StringBuilderAppend02/StringBuilderAppend02.java rename to regression/jbmc-strings/StringBuilderAppend02/StringBuilderAppend02.java diff --git a/regression/strings/StringBuilderAppend02/test.desc b/regression/jbmc-strings/StringBuilderAppend02/test.desc similarity index 100% rename from regression/strings/StringBuilderAppend02/test.desc rename to regression/jbmc-strings/StringBuilderAppend02/test.desc diff --git a/regression/strings/StringBuilderCapLen01/StringBuilderCapLen01.class b/regression/jbmc-strings/StringBuilderCapLen01/StringBuilderCapLen01.class similarity index 100% rename from regression/strings/StringBuilderCapLen01/StringBuilderCapLen01.class rename to regression/jbmc-strings/StringBuilderCapLen01/StringBuilderCapLen01.class diff --git a/regression/strings/StringBuilderCapLen01/StringBuilderCapLen01.java b/regression/jbmc-strings/StringBuilderCapLen01/StringBuilderCapLen01.java similarity index 100% rename from regression/strings/StringBuilderCapLen01/StringBuilderCapLen01.java rename to regression/jbmc-strings/StringBuilderCapLen01/StringBuilderCapLen01.java diff --git a/regression/strings/StringBuilderCapLen01/test.desc b/regression/jbmc-strings/StringBuilderCapLen01/test.desc similarity index 100% rename from regression/strings/StringBuilderCapLen01/test.desc rename to regression/jbmc-strings/StringBuilderCapLen01/test.desc diff --git a/regression/strings/StringBuilderCapLen02/StringBuilderCapLen02.class b/regression/jbmc-strings/StringBuilderCapLen02/StringBuilderCapLen02.class similarity index 100% rename from regression/strings/StringBuilderCapLen02/StringBuilderCapLen02.class rename to regression/jbmc-strings/StringBuilderCapLen02/StringBuilderCapLen02.class diff --git a/regression/strings/StringBuilderCapLen02/StringBuilderCapLen02.java b/regression/jbmc-strings/StringBuilderCapLen02/StringBuilderCapLen02.java similarity index 100% rename from regression/strings/StringBuilderCapLen02/StringBuilderCapLen02.java rename to regression/jbmc-strings/StringBuilderCapLen02/StringBuilderCapLen02.java diff --git a/regression/strings/StringBuilderCapLen02/test.desc b/regression/jbmc-strings/StringBuilderCapLen02/test.desc similarity index 100% rename from regression/strings/StringBuilderCapLen02/test.desc rename to regression/jbmc-strings/StringBuilderCapLen02/test.desc diff --git a/regression/strings/StringBuilderCapLen03/StringBuilderCapLen03.class b/regression/jbmc-strings/StringBuilderCapLen03/StringBuilderCapLen03.class similarity index 100% rename from regression/strings/StringBuilderCapLen03/StringBuilderCapLen03.class rename to regression/jbmc-strings/StringBuilderCapLen03/StringBuilderCapLen03.class diff --git a/regression/strings/StringBuilderCapLen03/StringBuilderCapLen03.java b/regression/jbmc-strings/StringBuilderCapLen03/StringBuilderCapLen03.java similarity index 100% rename from regression/strings/StringBuilderCapLen03/StringBuilderCapLen03.java rename to regression/jbmc-strings/StringBuilderCapLen03/StringBuilderCapLen03.java diff --git a/regression/strings/StringBuilderCapLen03/test.desc b/regression/jbmc-strings/StringBuilderCapLen03/test.desc similarity index 100% rename from regression/strings/StringBuilderCapLen03/test.desc rename to regression/jbmc-strings/StringBuilderCapLen03/test.desc diff --git a/regression/strings/StringBuilderCapLen04/StringBuilderCapLen04.class b/regression/jbmc-strings/StringBuilderCapLen04/StringBuilderCapLen04.class similarity index 100% rename from regression/strings/StringBuilderCapLen04/StringBuilderCapLen04.class rename to regression/jbmc-strings/StringBuilderCapLen04/StringBuilderCapLen04.class diff --git a/regression/strings/StringBuilderCapLen04/StringBuilderCapLen04.java b/regression/jbmc-strings/StringBuilderCapLen04/StringBuilderCapLen04.java similarity index 100% rename from regression/strings/StringBuilderCapLen04/StringBuilderCapLen04.java rename to regression/jbmc-strings/StringBuilderCapLen04/StringBuilderCapLen04.java diff --git a/regression/strings/StringBuilderCapLen04/test.desc b/regression/jbmc-strings/StringBuilderCapLen04/test.desc similarity index 100% rename from regression/strings/StringBuilderCapLen04/test.desc rename to regression/jbmc-strings/StringBuilderCapLen04/test.desc diff --git a/regression/strings/StringBuilderChars01/StringBuilderChars01.class b/regression/jbmc-strings/StringBuilderChars01/StringBuilderChars01.class similarity index 100% rename from regression/strings/StringBuilderChars01/StringBuilderChars01.class rename to regression/jbmc-strings/StringBuilderChars01/StringBuilderChars01.class diff --git a/regression/strings/StringBuilderChars01/StringBuilderChars01.java b/regression/jbmc-strings/StringBuilderChars01/StringBuilderChars01.java similarity index 100% rename from regression/strings/StringBuilderChars01/StringBuilderChars01.java rename to regression/jbmc-strings/StringBuilderChars01/StringBuilderChars01.java diff --git a/regression/strings/StringBuilderChars01/test.desc b/regression/jbmc-strings/StringBuilderChars01/test.desc similarity index 100% rename from regression/strings/StringBuilderChars01/test.desc rename to regression/jbmc-strings/StringBuilderChars01/test.desc diff --git a/regression/strings/StringBuilderChars02/StringBuilderChars02.class b/regression/jbmc-strings/StringBuilderChars02/StringBuilderChars02.class similarity index 100% rename from regression/strings/StringBuilderChars02/StringBuilderChars02.class rename to regression/jbmc-strings/StringBuilderChars02/StringBuilderChars02.class diff --git a/regression/strings/StringBuilderChars02/StringBuilderChars02.java b/regression/jbmc-strings/StringBuilderChars02/StringBuilderChars02.java similarity index 100% rename from regression/strings/StringBuilderChars02/StringBuilderChars02.java rename to regression/jbmc-strings/StringBuilderChars02/StringBuilderChars02.java diff --git a/regression/strings/StringBuilderChars02/test.desc b/regression/jbmc-strings/StringBuilderChars02/test.desc similarity index 100% rename from regression/strings/StringBuilderChars02/test.desc rename to regression/jbmc-strings/StringBuilderChars02/test.desc diff --git a/regression/strings/StringBuilderChars03/StringBuilderChars03.class b/regression/jbmc-strings/StringBuilderChars03/StringBuilderChars03.class similarity index 100% rename from regression/strings/StringBuilderChars03/StringBuilderChars03.class rename to regression/jbmc-strings/StringBuilderChars03/StringBuilderChars03.class diff --git a/regression/strings/StringBuilderChars03/StringBuilderChars03.java b/regression/jbmc-strings/StringBuilderChars03/StringBuilderChars03.java similarity index 100% rename from regression/strings/StringBuilderChars03/StringBuilderChars03.java rename to regression/jbmc-strings/StringBuilderChars03/StringBuilderChars03.java diff --git a/regression/strings/StringBuilderChars03/test.desc b/regression/jbmc-strings/StringBuilderChars03/test.desc similarity index 100% rename from regression/strings/StringBuilderChars03/test.desc rename to regression/jbmc-strings/StringBuilderChars03/test.desc diff --git a/regression/strings/StringBuilderChars04/StringBuilderChars04.class b/regression/jbmc-strings/StringBuilderChars04/StringBuilderChars04.class similarity index 100% rename from regression/strings/StringBuilderChars04/StringBuilderChars04.class rename to regression/jbmc-strings/StringBuilderChars04/StringBuilderChars04.class diff --git a/regression/strings/StringBuilderChars04/StringBuilderChars04.java b/regression/jbmc-strings/StringBuilderChars04/StringBuilderChars04.java similarity index 100% rename from regression/strings/StringBuilderChars04/StringBuilderChars04.java rename to regression/jbmc-strings/StringBuilderChars04/StringBuilderChars04.java diff --git a/regression/strings/StringBuilderChars04/test.desc b/regression/jbmc-strings/StringBuilderChars04/test.desc similarity index 100% rename from regression/strings/StringBuilderChars04/test.desc rename to regression/jbmc-strings/StringBuilderChars04/test.desc diff --git a/regression/strings/StringBuilderChars05/StringBuilderChars05.class b/regression/jbmc-strings/StringBuilderChars05/StringBuilderChars05.class similarity index 100% rename from regression/strings/StringBuilderChars05/StringBuilderChars05.class rename to regression/jbmc-strings/StringBuilderChars05/StringBuilderChars05.class diff --git a/regression/strings/StringBuilderChars05/StringBuilderChars05.java b/regression/jbmc-strings/StringBuilderChars05/StringBuilderChars05.java similarity index 100% rename from regression/strings/StringBuilderChars05/StringBuilderChars05.java rename to regression/jbmc-strings/StringBuilderChars05/StringBuilderChars05.java diff --git a/regression/strings/StringBuilderChars05/test.desc b/regression/jbmc-strings/StringBuilderChars05/test.desc similarity index 100% rename from regression/strings/StringBuilderChars05/test.desc rename to regression/jbmc-strings/StringBuilderChars05/test.desc diff --git a/regression/strings/StringBuilderChars06/StringBuilderChars06.class b/regression/jbmc-strings/StringBuilderChars06/StringBuilderChars06.class similarity index 100% rename from regression/strings/StringBuilderChars06/StringBuilderChars06.class rename to regression/jbmc-strings/StringBuilderChars06/StringBuilderChars06.class diff --git a/regression/strings/StringBuilderChars06/StringBuilderChars06.java b/regression/jbmc-strings/StringBuilderChars06/StringBuilderChars06.java similarity index 100% rename from regression/strings/StringBuilderChars06/StringBuilderChars06.java rename to regression/jbmc-strings/StringBuilderChars06/StringBuilderChars06.java diff --git a/regression/strings/StringBuilderChars06/test.desc b/regression/jbmc-strings/StringBuilderChars06/test.desc similarity index 100% rename from regression/strings/StringBuilderChars06/test.desc rename to regression/jbmc-strings/StringBuilderChars06/test.desc diff --git a/regression/strings/StringBuilderConstructors01/StringBuilderConstructors01.class b/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.class similarity index 100% rename from regression/strings/StringBuilderConstructors01/StringBuilderConstructors01.class rename to regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.class diff --git a/regression/strings/StringBuilderConstructors01/StringBuilderConstructors01.java b/regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java similarity index 100% rename from regression/strings/StringBuilderConstructors01/StringBuilderConstructors01.java rename to regression/jbmc-strings/StringBuilderConstructors01/StringBuilderConstructors01.java diff --git a/regression/strings/StringBuilderConstructors01/test.desc b/regression/jbmc-strings/StringBuilderConstructors01/test.desc similarity index 100% rename from regression/strings/StringBuilderConstructors01/test.desc rename to regression/jbmc-strings/StringBuilderConstructors01/test.desc diff --git a/regression/strings/StringBuilderConstructors02/StringBuilderConstructors02.class b/regression/jbmc-strings/StringBuilderConstructors02/StringBuilderConstructors02.class similarity index 100% rename from regression/strings/StringBuilderConstructors02/StringBuilderConstructors02.class rename to regression/jbmc-strings/StringBuilderConstructors02/StringBuilderConstructors02.class diff --git a/regression/strings/StringBuilderConstructors02/StringBuilderConstructors02.java b/regression/jbmc-strings/StringBuilderConstructors02/StringBuilderConstructors02.java similarity index 100% rename from regression/strings/StringBuilderConstructors02/StringBuilderConstructors02.java rename to regression/jbmc-strings/StringBuilderConstructors02/StringBuilderConstructors02.java diff --git a/regression/strings/StringBuilderConstructors02/test.desc b/regression/jbmc-strings/StringBuilderConstructors02/test.desc similarity index 100% rename from regression/strings/StringBuilderConstructors02/test.desc rename to regression/jbmc-strings/StringBuilderConstructors02/test.desc diff --git a/regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.class b/regression/jbmc-strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.class similarity index 100% rename from regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.class rename to regression/jbmc-strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.class diff --git a/regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.java b/regression/jbmc-strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.java similarity index 100% rename from regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.java rename to regression/jbmc-strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.java diff --git a/regression/strings/StringBuilderInsertDelete01/test.desc b/regression/jbmc-strings/StringBuilderInsertDelete01/test.desc similarity index 100% rename from regression/strings/StringBuilderInsertDelete01/test.desc rename to regression/jbmc-strings/StringBuilderInsertDelete01/test.desc diff --git a/regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.class b/regression/jbmc-strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.class similarity index 100% rename from regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.class rename to regression/jbmc-strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.class diff --git a/regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.java b/regression/jbmc-strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.java similarity index 100% rename from regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.java rename to regression/jbmc-strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.java diff --git a/regression/strings/StringBuilderInsertDelete02/test.desc b/regression/jbmc-strings/StringBuilderInsertDelete02/test.desc similarity index 100% rename from regression/strings/StringBuilderInsertDelete02/test.desc rename to regression/jbmc-strings/StringBuilderInsertDelete02/test.desc diff --git a/regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.class b/regression/jbmc-strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.class similarity index 100% rename from regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.class rename to regression/jbmc-strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.class diff --git a/regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.java b/regression/jbmc-strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.java similarity index 100% rename from regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.java rename to regression/jbmc-strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.java diff --git a/regression/strings/StringBuilderInsertDelete03/test.desc b/regression/jbmc-strings/StringBuilderInsertDelete03/test.desc similarity index 100% rename from regression/strings/StringBuilderInsertDelete03/test.desc rename to regression/jbmc-strings/StringBuilderInsertDelete03/test.desc diff --git a/regression/strings/StringCompare01/StringCompare01.class b/regression/jbmc-strings/StringCompare01/StringCompare01.class similarity index 100% rename from regression/strings/StringCompare01/StringCompare01.class rename to regression/jbmc-strings/StringCompare01/StringCompare01.class diff --git a/regression/strings/StringCompare01/StringCompare01.java b/regression/jbmc-strings/StringCompare01/StringCompare01.java similarity index 100% rename from regression/strings/StringCompare01/StringCompare01.java rename to regression/jbmc-strings/StringCompare01/StringCompare01.java diff --git a/regression/strings/StringCompare01/test.desc b/regression/jbmc-strings/StringCompare01/test.desc similarity index 100% rename from regression/strings/StringCompare01/test.desc rename to regression/jbmc-strings/StringCompare01/test.desc diff --git a/regression/strings/StringCompare02/StringCompare02.class b/regression/jbmc-strings/StringCompare02/StringCompare02.class similarity index 100% rename from regression/strings/StringCompare02/StringCompare02.class rename to regression/jbmc-strings/StringCompare02/StringCompare02.class diff --git a/regression/strings/StringCompare02/StringCompare02.java b/regression/jbmc-strings/StringCompare02/StringCompare02.java similarity index 100% rename from regression/strings/StringCompare02/StringCompare02.java rename to regression/jbmc-strings/StringCompare02/StringCompare02.java diff --git a/regression/strings/StringCompare02/test.desc b/regression/jbmc-strings/StringCompare02/test.desc similarity index 100% rename from regression/strings/StringCompare02/test.desc rename to regression/jbmc-strings/StringCompare02/test.desc diff --git a/regression/strings/StringCompare03/StringCompare03.class b/regression/jbmc-strings/StringCompare03/StringCompare03.class similarity index 100% rename from regression/strings/StringCompare03/StringCompare03.class rename to regression/jbmc-strings/StringCompare03/StringCompare03.class diff --git a/regression/strings/StringCompare03/StringCompare03.java b/regression/jbmc-strings/StringCompare03/StringCompare03.java similarity index 100% rename from regression/strings/StringCompare03/StringCompare03.java rename to regression/jbmc-strings/StringCompare03/StringCompare03.java diff --git a/regression/strings/StringCompare03/test.desc b/regression/jbmc-strings/StringCompare03/test.desc similarity index 100% rename from regression/strings/StringCompare03/test.desc rename to regression/jbmc-strings/StringCompare03/test.desc diff --git a/regression/strings/StringCompare04/StringCompare04.class b/regression/jbmc-strings/StringCompare04/StringCompare04.class similarity index 100% rename from regression/strings/StringCompare04/StringCompare04.class rename to regression/jbmc-strings/StringCompare04/StringCompare04.class diff --git a/regression/strings/StringCompare04/StringCompare04.java b/regression/jbmc-strings/StringCompare04/StringCompare04.java similarity index 100% rename from regression/strings/StringCompare04/StringCompare04.java rename to regression/jbmc-strings/StringCompare04/StringCompare04.java diff --git a/regression/strings/StringCompare04/test.desc b/regression/jbmc-strings/StringCompare04/test.desc similarity index 100% rename from regression/strings/StringCompare04/test.desc rename to regression/jbmc-strings/StringCompare04/test.desc diff --git a/regression/strings/StringCompare05/StringCompare05.class b/regression/jbmc-strings/StringCompare05/StringCompare05.class similarity index 100% rename from regression/strings/StringCompare05/StringCompare05.class rename to regression/jbmc-strings/StringCompare05/StringCompare05.class diff --git a/regression/strings/StringCompare05/StringCompare05.java b/regression/jbmc-strings/StringCompare05/StringCompare05.java similarity index 100% rename from regression/strings/StringCompare05/StringCompare05.java rename to regression/jbmc-strings/StringCompare05/StringCompare05.java diff --git a/regression/strings/StringCompare05/test.desc b/regression/jbmc-strings/StringCompare05/test.desc similarity index 100% rename from regression/strings/StringCompare05/test.desc rename to regression/jbmc-strings/StringCompare05/test.desc diff --git a/regression/strings/StringConcatenation01/StringConcatenation01.class b/regression/jbmc-strings/StringConcatenation01/StringConcatenation01.class similarity index 100% rename from regression/strings/StringConcatenation01/StringConcatenation01.class rename to regression/jbmc-strings/StringConcatenation01/StringConcatenation01.class diff --git a/regression/strings/StringConcatenation01/StringConcatenation01.java b/regression/jbmc-strings/StringConcatenation01/StringConcatenation01.java similarity index 100% rename from regression/strings/StringConcatenation01/StringConcatenation01.java rename to regression/jbmc-strings/StringConcatenation01/StringConcatenation01.java diff --git a/regression/strings/StringConcatenation01/test.desc b/regression/jbmc-strings/StringConcatenation01/test.desc similarity index 100% rename from regression/strings/StringConcatenation01/test.desc rename to regression/jbmc-strings/StringConcatenation01/test.desc diff --git a/regression/strings/StringConcatenation02/StringConcatenation02.class b/regression/jbmc-strings/StringConcatenation02/StringConcatenation02.class similarity index 100% rename from regression/strings/StringConcatenation02/StringConcatenation02.class rename to regression/jbmc-strings/StringConcatenation02/StringConcatenation02.class diff --git a/regression/strings/StringConcatenation02/StringConcatenation02.java b/regression/jbmc-strings/StringConcatenation02/StringConcatenation02.java similarity index 100% rename from regression/strings/StringConcatenation02/StringConcatenation02.java rename to regression/jbmc-strings/StringConcatenation02/StringConcatenation02.java diff --git a/regression/strings/StringConcatenation02/test.desc b/regression/jbmc-strings/StringConcatenation02/test.desc similarity index 100% rename from regression/strings/StringConcatenation02/test.desc rename to regression/jbmc-strings/StringConcatenation02/test.desc diff --git a/regression/strings/StringConcatenation03/StringConcatenation03.class b/regression/jbmc-strings/StringConcatenation03/StringConcatenation03.class similarity index 100% rename from regression/strings/StringConcatenation03/StringConcatenation03.class rename to regression/jbmc-strings/StringConcatenation03/StringConcatenation03.class diff --git a/regression/strings/StringConcatenation03/StringConcatenation03.java b/regression/jbmc-strings/StringConcatenation03/StringConcatenation03.java similarity index 100% rename from regression/strings/StringConcatenation03/StringConcatenation03.java rename to regression/jbmc-strings/StringConcatenation03/StringConcatenation03.java diff --git a/regression/strings/StringConcatenation03/test.desc b/regression/jbmc-strings/StringConcatenation03/test.desc similarity index 100% rename from regression/strings/StringConcatenation03/test.desc rename to regression/jbmc-strings/StringConcatenation03/test.desc diff --git a/regression/strings/StringConcatenation04/StringConcatenation04.class b/regression/jbmc-strings/StringConcatenation04/StringConcatenation04.class similarity index 100% rename from regression/strings/StringConcatenation04/StringConcatenation04.class rename to regression/jbmc-strings/StringConcatenation04/StringConcatenation04.class diff --git a/regression/strings/StringConcatenation04/StringConcatenation04.java b/regression/jbmc-strings/StringConcatenation04/StringConcatenation04.java similarity index 100% rename from regression/strings/StringConcatenation04/StringConcatenation04.java rename to regression/jbmc-strings/StringConcatenation04/StringConcatenation04.java diff --git a/regression/strings/StringConcatenation04/test.desc b/regression/jbmc-strings/StringConcatenation04/test.desc similarity index 100% rename from regression/strings/StringConcatenation04/test.desc rename to regression/jbmc-strings/StringConcatenation04/test.desc diff --git a/regression/strings/StringConstructors01/StringConstructors01.class b/regression/jbmc-strings/StringConstructors01/StringConstructors01.class similarity index 100% rename from regression/strings/StringConstructors01/StringConstructors01.class rename to regression/jbmc-strings/StringConstructors01/StringConstructors01.class diff --git a/regression/strings/StringConstructors01/StringConstructors01.java b/regression/jbmc-strings/StringConstructors01/StringConstructors01.java similarity index 100% rename from regression/strings/StringConstructors01/StringConstructors01.java rename to regression/jbmc-strings/StringConstructors01/StringConstructors01.java diff --git a/regression/strings/StringConstructors01/test.desc b/regression/jbmc-strings/StringConstructors01/test.desc similarity index 100% rename from regression/strings/StringConstructors01/test.desc rename to regression/jbmc-strings/StringConstructors01/test.desc diff --git a/regression/strings/StringConstructors02/StringConstructors02.class b/regression/jbmc-strings/StringConstructors02/StringConstructors02.class similarity index 100% rename from regression/strings/StringConstructors02/StringConstructors02.class rename to regression/jbmc-strings/StringConstructors02/StringConstructors02.class diff --git a/regression/strings/StringConstructors02/StringConstructors02.java b/regression/jbmc-strings/StringConstructors02/StringConstructors02.java similarity index 100% rename from regression/strings/StringConstructors02/StringConstructors02.java rename to regression/jbmc-strings/StringConstructors02/StringConstructors02.java diff --git a/regression/strings/StringConstructors02/test.desc b/regression/jbmc-strings/StringConstructors02/test.desc similarity index 100% rename from regression/strings/StringConstructors02/test.desc rename to regression/jbmc-strings/StringConstructors02/test.desc diff --git a/regression/strings/StringConstructors03/StringConstructors03.class b/regression/jbmc-strings/StringConstructors03/StringConstructors03.class similarity index 100% rename from regression/strings/StringConstructors03/StringConstructors03.class rename to regression/jbmc-strings/StringConstructors03/StringConstructors03.class diff --git a/regression/strings/StringConstructors03/StringConstructors03.java b/regression/jbmc-strings/StringConstructors03/StringConstructors03.java similarity index 100% rename from regression/strings/StringConstructors03/StringConstructors03.java rename to regression/jbmc-strings/StringConstructors03/StringConstructors03.java diff --git a/regression/strings/StringConstructors03/test.desc b/regression/jbmc-strings/StringConstructors03/test.desc similarity index 100% rename from regression/strings/StringConstructors03/test.desc rename to regression/jbmc-strings/StringConstructors03/test.desc diff --git a/regression/strings/StringConstructors04/StringConstructors04.class b/regression/jbmc-strings/StringConstructors04/StringConstructors04.class similarity index 100% rename from regression/strings/StringConstructors04/StringConstructors04.class rename to regression/jbmc-strings/StringConstructors04/StringConstructors04.class diff --git a/regression/strings/StringConstructors04/StringConstructors04.java b/regression/jbmc-strings/StringConstructors04/StringConstructors04.java similarity index 100% rename from regression/strings/StringConstructors04/StringConstructors04.java rename to regression/jbmc-strings/StringConstructors04/StringConstructors04.java diff --git a/regression/strings/StringConstructors04/test.desc b/regression/jbmc-strings/StringConstructors04/test.desc similarity index 100% rename from regression/strings/StringConstructors04/test.desc rename to regression/jbmc-strings/StringConstructors04/test.desc diff --git a/regression/strings/StringConstructors05/StringConstructors05.class b/regression/jbmc-strings/StringConstructors05/StringConstructors05.class similarity index 100% rename from regression/strings/StringConstructors05/StringConstructors05.class rename to regression/jbmc-strings/StringConstructors05/StringConstructors05.class diff --git a/regression/strings/StringConstructors05/StringConstructors05.java b/regression/jbmc-strings/StringConstructors05/StringConstructors05.java similarity index 100% rename from regression/strings/StringConstructors05/StringConstructors05.java rename to regression/jbmc-strings/StringConstructors05/StringConstructors05.java diff --git a/regression/strings/StringConstructors05/test.desc b/regression/jbmc-strings/StringConstructors05/test.desc similarity index 100% rename from regression/strings/StringConstructors05/test.desc rename to regression/jbmc-strings/StringConstructors05/test.desc diff --git a/regression/strings/StringContains01/test.class b/regression/jbmc-strings/StringContains01/test.class similarity index 100% rename from regression/strings/StringContains01/test.class rename to regression/jbmc-strings/StringContains01/test.class diff --git a/regression/strings/StringContains01/test.desc b/regression/jbmc-strings/StringContains01/test.desc similarity index 100% rename from regression/strings/StringContains01/test.desc rename to regression/jbmc-strings/StringContains01/test.desc diff --git a/regression/strings/StringContains01/test.java b/regression/jbmc-strings/StringContains01/test.java similarity index 100% rename from regression/strings/StringContains01/test.java rename to regression/jbmc-strings/StringContains01/test.java diff --git a/regression/strings/StringContains02/test.class b/regression/jbmc-strings/StringContains02/test.class similarity index 100% rename from regression/strings/StringContains02/test.class rename to regression/jbmc-strings/StringContains02/test.class diff --git a/regression/strings/StringContains02/test.desc b/regression/jbmc-strings/StringContains02/test.desc similarity index 100% rename from regression/strings/StringContains02/test.desc rename to regression/jbmc-strings/StringContains02/test.desc diff --git a/regression/strings/StringContains02/test.java b/regression/jbmc-strings/StringContains02/test.java similarity index 100% rename from regression/strings/StringContains02/test.java rename to regression/jbmc-strings/StringContains02/test.java diff --git a/regression/strings/StringIndexMethods01/StringIndexMethods01.class b/regression/jbmc-strings/StringIndexMethods01/StringIndexMethods01.class similarity index 100% rename from regression/strings/StringIndexMethods01/StringIndexMethods01.class rename to regression/jbmc-strings/StringIndexMethods01/StringIndexMethods01.class diff --git a/regression/strings/StringIndexMethods01/StringIndexMethods01.java b/regression/jbmc-strings/StringIndexMethods01/StringIndexMethods01.java similarity index 100% rename from regression/strings/StringIndexMethods01/StringIndexMethods01.java rename to regression/jbmc-strings/StringIndexMethods01/StringIndexMethods01.java diff --git a/regression/strings/StringIndexMethods01/test.desc b/regression/jbmc-strings/StringIndexMethods01/test.desc similarity index 100% rename from regression/strings/StringIndexMethods01/test.desc rename to regression/jbmc-strings/StringIndexMethods01/test.desc diff --git a/regression/strings/StringIndexMethods02/StringIndexMethods02.class b/regression/jbmc-strings/StringIndexMethods02/StringIndexMethods02.class similarity index 100% rename from regression/strings/StringIndexMethods02/StringIndexMethods02.class rename to regression/jbmc-strings/StringIndexMethods02/StringIndexMethods02.class diff --git a/regression/strings/StringIndexMethods02/StringIndexMethods02.java b/regression/jbmc-strings/StringIndexMethods02/StringIndexMethods02.java similarity index 100% rename from regression/strings/StringIndexMethods02/StringIndexMethods02.java rename to regression/jbmc-strings/StringIndexMethods02/StringIndexMethods02.java diff --git a/regression/strings/StringIndexMethods02/test.desc b/regression/jbmc-strings/StringIndexMethods02/test.desc similarity index 100% rename from regression/strings/StringIndexMethods02/test.desc rename to regression/jbmc-strings/StringIndexMethods02/test.desc diff --git a/regression/strings/StringIndexMethods03/StringIndexMethods03.class b/regression/jbmc-strings/StringIndexMethods03/StringIndexMethods03.class similarity index 100% rename from regression/strings/StringIndexMethods03/StringIndexMethods03.class rename to regression/jbmc-strings/StringIndexMethods03/StringIndexMethods03.class diff --git a/regression/strings/StringIndexMethods03/StringIndexMethods03.java b/regression/jbmc-strings/StringIndexMethods03/StringIndexMethods03.java similarity index 100% rename from regression/strings/StringIndexMethods03/StringIndexMethods03.java rename to regression/jbmc-strings/StringIndexMethods03/StringIndexMethods03.java diff --git a/regression/strings/StringIndexMethods03/test.desc b/regression/jbmc-strings/StringIndexMethods03/test.desc similarity index 100% rename from regression/strings/StringIndexMethods03/test.desc rename to regression/jbmc-strings/StringIndexMethods03/test.desc diff --git a/regression/strings/StringIndexMethods04/StringIndexMethods04.class b/regression/jbmc-strings/StringIndexMethods04/StringIndexMethods04.class similarity index 100% rename from regression/strings/StringIndexMethods04/StringIndexMethods04.class rename to regression/jbmc-strings/StringIndexMethods04/StringIndexMethods04.class diff --git a/regression/strings/StringIndexMethods04/StringIndexMethods04.java b/regression/jbmc-strings/StringIndexMethods04/StringIndexMethods04.java similarity index 100% rename from regression/strings/StringIndexMethods04/StringIndexMethods04.java rename to regression/jbmc-strings/StringIndexMethods04/StringIndexMethods04.java diff --git a/regression/strings/StringIndexMethods04/test.desc b/regression/jbmc-strings/StringIndexMethods04/test.desc similarity index 100% rename from regression/strings/StringIndexMethods04/test.desc rename to regression/jbmc-strings/StringIndexMethods04/test.desc diff --git a/regression/strings/StringIndexMethods04/test_bug.desc b/regression/jbmc-strings/StringIndexMethods04/test_bug.desc similarity index 100% rename from regression/strings/StringIndexMethods04/test_bug.desc rename to regression/jbmc-strings/StringIndexMethods04/test_bug.desc diff --git a/regression/strings/StringIndexMethods05/StringIndexMethods05.class b/regression/jbmc-strings/StringIndexMethods05/StringIndexMethods05.class similarity index 100% rename from regression/strings/StringIndexMethods05/StringIndexMethods05.class rename to regression/jbmc-strings/StringIndexMethods05/StringIndexMethods05.class diff --git a/regression/strings/StringIndexMethods05/StringIndexMethods05.java b/regression/jbmc-strings/StringIndexMethods05/StringIndexMethods05.java similarity index 100% rename from regression/strings/StringIndexMethods05/StringIndexMethods05.java rename to regression/jbmc-strings/StringIndexMethods05/StringIndexMethods05.java diff --git a/regression/strings/StringIndexMethods05/test.desc b/regression/jbmc-strings/StringIndexMethods05/test.desc similarity index 100% rename from regression/strings/StringIndexMethods05/test.desc rename to regression/jbmc-strings/StringIndexMethods05/test.desc diff --git a/regression/strings/StringMiscellaneous01/StringMiscellaneous01.class b/regression/jbmc-strings/StringMiscellaneous01/StringMiscellaneous01.class similarity index 100% rename from regression/strings/StringMiscellaneous01/StringMiscellaneous01.class rename to regression/jbmc-strings/StringMiscellaneous01/StringMiscellaneous01.class diff --git a/regression/strings/StringMiscellaneous01/StringMiscellaneous01.java b/regression/jbmc-strings/StringMiscellaneous01/StringMiscellaneous01.java similarity index 100% rename from regression/strings/StringMiscellaneous01/StringMiscellaneous01.java rename to regression/jbmc-strings/StringMiscellaneous01/StringMiscellaneous01.java diff --git a/regression/strings/StringMiscellaneous01/test.desc b/regression/jbmc-strings/StringMiscellaneous01/test.desc similarity index 100% rename from regression/strings/StringMiscellaneous01/test.desc rename to regression/jbmc-strings/StringMiscellaneous01/test.desc diff --git a/regression/strings/StringMiscellaneous02/StringMiscellaneous02.class b/regression/jbmc-strings/StringMiscellaneous02/StringMiscellaneous02.class similarity index 100% rename from regression/strings/StringMiscellaneous02/StringMiscellaneous02.class rename to regression/jbmc-strings/StringMiscellaneous02/StringMiscellaneous02.class diff --git a/regression/strings/StringMiscellaneous02/StringMiscellaneous02.java b/regression/jbmc-strings/StringMiscellaneous02/StringMiscellaneous02.java similarity index 100% rename from regression/strings/StringMiscellaneous02/StringMiscellaneous02.java rename to regression/jbmc-strings/StringMiscellaneous02/StringMiscellaneous02.java diff --git a/regression/strings/StringMiscellaneous02/test.desc b/regression/jbmc-strings/StringMiscellaneous02/test.desc similarity index 100% rename from regression/strings/StringMiscellaneous02/test.desc rename to regression/jbmc-strings/StringMiscellaneous02/test.desc diff --git a/regression/strings/StringMiscellaneous03/StringMiscellaneous03.class b/regression/jbmc-strings/StringMiscellaneous03/StringMiscellaneous03.class similarity index 100% rename from regression/strings/StringMiscellaneous03/StringMiscellaneous03.class rename to regression/jbmc-strings/StringMiscellaneous03/StringMiscellaneous03.class diff --git a/regression/strings/StringMiscellaneous03/StringMiscellaneous03.java b/regression/jbmc-strings/StringMiscellaneous03/StringMiscellaneous03.java similarity index 100% rename from regression/strings/StringMiscellaneous03/StringMiscellaneous03.java rename to regression/jbmc-strings/StringMiscellaneous03/StringMiscellaneous03.java diff --git a/regression/strings/StringMiscellaneous03/test.desc b/regression/jbmc-strings/StringMiscellaneous03/test.desc similarity index 100% rename from regression/strings/StringMiscellaneous03/test.desc rename to regression/jbmc-strings/StringMiscellaneous03/test.desc diff --git a/regression/strings/StringMiscellaneous04/StringMiscellaneous04.class b/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class similarity index 100% rename from regression/strings/StringMiscellaneous04/StringMiscellaneous04.class rename to regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.class diff --git a/regression/strings/StringMiscellaneous04/StringMiscellaneous04.java b/regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java similarity index 100% rename from regression/strings/StringMiscellaneous04/StringMiscellaneous04.java rename to regression/jbmc-strings/StringMiscellaneous04/StringMiscellaneous04.java diff --git a/regression/strings/StringMiscellaneous04/test.desc b/regression/jbmc-strings/StringMiscellaneous04/test.desc similarity index 100% rename from regression/strings/StringMiscellaneous04/test.desc rename to regression/jbmc-strings/StringMiscellaneous04/test.desc diff --git a/regression/strings/StringStartEnd01/StringStartEnd01.class b/regression/jbmc-strings/StringStartEnd01/StringStartEnd01.class similarity index 100% rename from regression/strings/StringStartEnd01/StringStartEnd01.class rename to regression/jbmc-strings/StringStartEnd01/StringStartEnd01.class diff --git a/regression/strings/StringStartEnd01/StringStartEnd01.java b/regression/jbmc-strings/StringStartEnd01/StringStartEnd01.java similarity index 100% rename from regression/strings/StringStartEnd01/StringStartEnd01.java rename to regression/jbmc-strings/StringStartEnd01/StringStartEnd01.java diff --git a/regression/strings/StringStartEnd01/test.desc b/regression/jbmc-strings/StringStartEnd01/test.desc similarity index 100% rename from regression/strings/StringStartEnd01/test.desc rename to regression/jbmc-strings/StringStartEnd01/test.desc diff --git a/regression/strings/StringStartEnd02/StringStartEnd02.class b/regression/jbmc-strings/StringStartEnd02/StringStartEnd02.class similarity index 100% rename from regression/strings/StringStartEnd02/StringStartEnd02.class rename to regression/jbmc-strings/StringStartEnd02/StringStartEnd02.class diff --git a/regression/strings/StringStartEnd02/StringStartEnd02.java b/regression/jbmc-strings/StringStartEnd02/StringStartEnd02.java similarity index 100% rename from regression/strings/StringStartEnd02/StringStartEnd02.java rename to regression/jbmc-strings/StringStartEnd02/StringStartEnd02.java diff --git a/regression/strings/StringStartEnd02/test.desc b/regression/jbmc-strings/StringStartEnd02/test.desc similarity index 100% rename from regression/strings/StringStartEnd02/test.desc rename to regression/jbmc-strings/StringStartEnd02/test.desc diff --git a/regression/strings/StringStartEnd03/StringStartEnd03.class b/regression/jbmc-strings/StringStartEnd03/StringStartEnd03.class similarity index 100% rename from regression/strings/StringStartEnd03/StringStartEnd03.class rename to regression/jbmc-strings/StringStartEnd03/StringStartEnd03.class diff --git a/regression/strings/StringStartEnd03/StringStartEnd03.java b/regression/jbmc-strings/StringStartEnd03/StringStartEnd03.java similarity index 100% rename from regression/strings/StringStartEnd03/StringStartEnd03.java rename to regression/jbmc-strings/StringStartEnd03/StringStartEnd03.java diff --git a/regression/strings/StringStartEnd03/test.desc b/regression/jbmc-strings/StringStartEnd03/test.desc similarity index 100% rename from regression/strings/StringStartEnd03/test.desc rename to regression/jbmc-strings/StringStartEnd03/test.desc diff --git a/regression/strings/StringValueOf01/StringValueOf01.class b/regression/jbmc-strings/StringValueOf01/StringValueOf01.class similarity index 100% rename from regression/strings/StringValueOf01/StringValueOf01.class rename to regression/jbmc-strings/StringValueOf01/StringValueOf01.class diff --git a/regression/strings/StringValueOf01/StringValueOf01.java b/regression/jbmc-strings/StringValueOf01/StringValueOf01.java similarity index 100% rename from regression/strings/StringValueOf01/StringValueOf01.java rename to regression/jbmc-strings/StringValueOf01/StringValueOf01.java diff --git a/regression/strings/StringValueOf01/test.desc b/regression/jbmc-strings/StringValueOf01/test.desc similarity index 100% rename from regression/strings/StringValueOf01/test.desc rename to regression/jbmc-strings/StringValueOf01/test.desc diff --git a/regression/strings/StringValueOf02/StringValueOf02.class b/regression/jbmc-strings/StringValueOf02/StringValueOf02.class similarity index 100% rename from regression/strings/StringValueOf02/StringValueOf02.class rename to regression/jbmc-strings/StringValueOf02/StringValueOf02.class diff --git a/regression/strings/StringValueOf02/StringValueOf02.java b/regression/jbmc-strings/StringValueOf02/StringValueOf02.java similarity index 100% rename from regression/strings/StringValueOf02/StringValueOf02.java rename to regression/jbmc-strings/StringValueOf02/StringValueOf02.java diff --git a/regression/strings/StringValueOf02/test.desc b/regression/jbmc-strings/StringValueOf02/test.desc similarity index 100% rename from regression/strings/StringValueOf02/test.desc rename to regression/jbmc-strings/StringValueOf02/test.desc diff --git a/regression/strings/StringValueOf03/StringValueOf03.class b/regression/jbmc-strings/StringValueOf03/StringValueOf03.class similarity index 100% rename from regression/strings/StringValueOf03/StringValueOf03.class rename to regression/jbmc-strings/StringValueOf03/StringValueOf03.class diff --git a/regression/strings/StringValueOf03/StringValueOf03.java b/regression/jbmc-strings/StringValueOf03/StringValueOf03.java similarity index 100% rename from regression/strings/StringValueOf03/StringValueOf03.java rename to regression/jbmc-strings/StringValueOf03/StringValueOf03.java diff --git a/regression/strings/StringValueOf03/test.desc b/regression/jbmc-strings/StringValueOf03/test.desc similarity index 100% rename from regression/strings/StringValueOf03/test.desc rename to regression/jbmc-strings/StringValueOf03/test.desc diff --git a/regression/strings/StringValueOf04/StringValueOf04.class b/regression/jbmc-strings/StringValueOf04/StringValueOf04.class similarity index 100% rename from regression/strings/StringValueOf04/StringValueOf04.class rename to regression/jbmc-strings/StringValueOf04/StringValueOf04.class diff --git a/regression/strings/StringValueOf04/StringValueOf04.java b/regression/jbmc-strings/StringValueOf04/StringValueOf04.java similarity index 100% rename from regression/strings/StringValueOf04/StringValueOf04.java rename to regression/jbmc-strings/StringValueOf04/StringValueOf04.java diff --git a/regression/strings/StringValueOf04/test.desc b/regression/jbmc-strings/StringValueOf04/test.desc similarity index 100% rename from regression/strings/StringValueOf04/test.desc rename to regression/jbmc-strings/StringValueOf04/test.desc diff --git a/regression/strings/StringValueOf05/StringValueOf05.class b/regression/jbmc-strings/StringValueOf05/StringValueOf05.class similarity index 100% rename from regression/strings/StringValueOf05/StringValueOf05.class rename to regression/jbmc-strings/StringValueOf05/StringValueOf05.class diff --git a/regression/strings/StringValueOf05/StringValueOf05.java b/regression/jbmc-strings/StringValueOf05/StringValueOf05.java similarity index 100% rename from regression/strings/StringValueOf05/StringValueOf05.java rename to regression/jbmc-strings/StringValueOf05/StringValueOf05.java diff --git a/regression/strings/StringValueOf05/test.desc b/regression/jbmc-strings/StringValueOf05/test.desc similarity index 100% rename from regression/strings/StringValueOf05/test.desc rename to regression/jbmc-strings/StringValueOf05/test.desc diff --git a/regression/strings/StringValueOf06/StringValueOf06.class b/regression/jbmc-strings/StringValueOf06/StringValueOf06.class similarity index 100% rename from regression/strings/StringValueOf06/StringValueOf06.class rename to regression/jbmc-strings/StringValueOf06/StringValueOf06.class diff --git a/regression/strings/StringValueOf06/StringValueOf06.java b/regression/jbmc-strings/StringValueOf06/StringValueOf06.java similarity index 100% rename from regression/strings/StringValueOf06/StringValueOf06.java rename to regression/jbmc-strings/StringValueOf06/StringValueOf06.java diff --git a/regression/strings/StringValueOf06/test.desc b/regression/jbmc-strings/StringValueOf06/test.desc similarity index 100% rename from regression/strings/StringValueOf06/test.desc rename to regression/jbmc-strings/StringValueOf06/test.desc diff --git a/regression/strings/StringValueOf07/StringValueOf07.class b/regression/jbmc-strings/StringValueOf07/StringValueOf07.class similarity index 100% rename from regression/strings/StringValueOf07/StringValueOf07.class rename to regression/jbmc-strings/StringValueOf07/StringValueOf07.class diff --git a/regression/strings/StringValueOf07/StringValueOf07.java b/regression/jbmc-strings/StringValueOf07/StringValueOf07.java similarity index 100% rename from regression/strings/StringValueOf07/StringValueOf07.java rename to regression/jbmc-strings/StringValueOf07/StringValueOf07.java diff --git a/regression/strings/StringValueOf07/test.desc b/regression/jbmc-strings/StringValueOf07/test.desc similarity index 100% rename from regression/strings/StringValueOf07/test.desc rename to regression/jbmc-strings/StringValueOf07/test.desc diff --git a/regression/strings/StringValueOf08/StringValueOf08.class b/regression/jbmc-strings/StringValueOf08/StringValueOf08.class similarity index 100% rename from regression/strings/StringValueOf08/StringValueOf08.class rename to regression/jbmc-strings/StringValueOf08/StringValueOf08.class diff --git a/regression/strings/StringValueOf08/StringValueOf08.java b/regression/jbmc-strings/StringValueOf08/StringValueOf08.java similarity index 100% rename from regression/strings/StringValueOf08/StringValueOf08.java rename to regression/jbmc-strings/StringValueOf08/StringValueOf08.java diff --git a/regression/strings/StringValueOf08/test.desc b/regression/jbmc-strings/StringValueOf08/test.desc similarity index 100% rename from regression/strings/StringValueOf08/test.desc rename to regression/jbmc-strings/StringValueOf08/test.desc diff --git a/regression/strings/StringValueOf09/StringValueOf09.class b/regression/jbmc-strings/StringValueOf09/StringValueOf09.class similarity index 100% rename from regression/strings/StringValueOf09/StringValueOf09.class rename to regression/jbmc-strings/StringValueOf09/StringValueOf09.class diff --git a/regression/strings/StringValueOf09/StringValueOf09.java b/regression/jbmc-strings/StringValueOf09/StringValueOf09.java similarity index 100% rename from regression/strings/StringValueOf09/StringValueOf09.java rename to regression/jbmc-strings/StringValueOf09/StringValueOf09.java diff --git a/regression/strings/StringValueOf09/test.desc b/regression/jbmc-strings/StringValueOf09/test.desc similarity index 100% rename from regression/strings/StringValueOf09/test.desc rename to regression/jbmc-strings/StringValueOf09/test.desc diff --git a/regression/strings/StringValueOf10/StringValueOf10.class b/regression/jbmc-strings/StringValueOf10/StringValueOf10.class similarity index 100% rename from regression/strings/StringValueOf10/StringValueOf10.class rename to regression/jbmc-strings/StringValueOf10/StringValueOf10.class diff --git a/regression/strings/StringValueOf10/StringValueOf10.java b/regression/jbmc-strings/StringValueOf10/StringValueOf10.java similarity index 100% rename from regression/strings/StringValueOf10/StringValueOf10.java rename to regression/jbmc-strings/StringValueOf10/StringValueOf10.java diff --git a/regression/strings/StringValueOf10/test.desc b/regression/jbmc-strings/StringValueOf10/test.desc similarity index 100% rename from regression/strings/StringValueOf10/test.desc rename to regression/jbmc-strings/StringValueOf10/test.desc diff --git a/regression/strings/SubString01/SubString01.class b/regression/jbmc-strings/SubString01/SubString01.class similarity index 100% rename from regression/strings/SubString01/SubString01.class rename to regression/jbmc-strings/SubString01/SubString01.class diff --git a/regression/strings/SubString01/SubString01.java b/regression/jbmc-strings/SubString01/SubString01.java similarity index 100% rename from regression/strings/SubString01/SubString01.java rename to regression/jbmc-strings/SubString01/SubString01.java diff --git a/regression/strings/SubString01/test.desc b/regression/jbmc-strings/SubString01/test.desc similarity index 100% rename from regression/strings/SubString01/test.desc rename to regression/jbmc-strings/SubString01/test.desc diff --git a/regression/strings/SubString02/SubString02.class b/regression/jbmc-strings/SubString02/SubString02.class similarity index 100% rename from regression/strings/SubString02/SubString02.class rename to regression/jbmc-strings/SubString02/SubString02.class diff --git a/regression/strings/SubString02/SubString02.java b/regression/jbmc-strings/SubString02/SubString02.java similarity index 100% rename from regression/strings/SubString02/SubString02.java rename to regression/jbmc-strings/SubString02/SubString02.java diff --git a/regression/strings/SubString02/test.desc b/regression/jbmc-strings/SubString02/test.desc similarity index 100% rename from regression/strings/SubString02/test.desc rename to regression/jbmc-strings/SubString02/test.desc diff --git a/regression/strings/SubString03/SubString03.class b/regression/jbmc-strings/SubString03/SubString03.class similarity index 100% rename from regression/strings/SubString03/SubString03.class rename to regression/jbmc-strings/SubString03/SubString03.class diff --git a/regression/strings/SubString03/SubString03.java b/regression/jbmc-strings/SubString03/SubString03.java similarity index 100% rename from regression/strings/SubString03/SubString03.java rename to regression/jbmc-strings/SubString03/SubString03.java diff --git a/regression/strings/SubString03/test.desc b/regression/jbmc-strings/SubString03/test.desc similarity index 100% rename from regression/strings/SubString03/test.desc rename to regression/jbmc-strings/SubString03/test.desc diff --git a/regression/strings/TokenTest01/TokenTest01.class b/regression/jbmc-strings/TokenTest01/TokenTest01.class similarity index 100% rename from regression/strings/TokenTest01/TokenTest01.class rename to regression/jbmc-strings/TokenTest01/TokenTest01.class diff --git a/regression/strings/TokenTest01/TokenTest01.java b/regression/jbmc-strings/TokenTest01/TokenTest01.java similarity index 100% rename from regression/strings/TokenTest01/TokenTest01.java rename to regression/jbmc-strings/TokenTest01/TokenTest01.java diff --git a/regression/strings/TokenTest01/test.desc b/regression/jbmc-strings/TokenTest01/test.desc similarity index 100% rename from regression/strings/TokenTest01/test.desc rename to regression/jbmc-strings/TokenTest01/test.desc diff --git a/regression/strings/TokenTest02/TokenTest02.class b/regression/jbmc-strings/TokenTest02/TokenTest02.class similarity index 100% rename from regression/strings/TokenTest02/TokenTest02.class rename to regression/jbmc-strings/TokenTest02/TokenTest02.class diff --git a/regression/strings/TokenTest02/TokenTest02.java b/regression/jbmc-strings/TokenTest02/TokenTest02.java similarity index 100% rename from regression/strings/TokenTest02/TokenTest02.java rename to regression/jbmc-strings/TokenTest02/TokenTest02.java diff --git a/regression/strings/TokenTest02/test.desc b/regression/jbmc-strings/TokenTest02/test.desc similarity index 100% rename from regression/strings/TokenTest02/test.desc rename to regression/jbmc-strings/TokenTest02/test.desc diff --git a/regression/strings/Validate01/Validate01.class b/regression/jbmc-strings/Validate01/Validate01.class similarity index 100% rename from regression/strings/Validate01/Validate01.class rename to regression/jbmc-strings/Validate01/Validate01.class diff --git a/regression/strings/Validate01/Validate01.java b/regression/jbmc-strings/Validate01/Validate01.java similarity index 100% rename from regression/strings/Validate01/Validate01.java rename to regression/jbmc-strings/Validate01/Validate01.java diff --git a/regression/strings/Validate01/ValidateInput01.class b/regression/jbmc-strings/Validate01/ValidateInput01.class similarity index 100% rename from regression/strings/Validate01/ValidateInput01.class rename to regression/jbmc-strings/Validate01/ValidateInput01.class diff --git a/regression/strings/Validate01/ValidateInput01.java b/regression/jbmc-strings/Validate01/ValidateInput01.java similarity index 100% rename from regression/strings/Validate01/ValidateInput01.java rename to regression/jbmc-strings/Validate01/ValidateInput01.java diff --git a/regression/strings/Validate01/test.desc b/regression/jbmc-strings/Validate01/test.desc similarity index 100% rename from regression/strings/Validate01/test.desc rename to regression/jbmc-strings/Validate01/test.desc diff --git a/regression/strings/Validate02/Validate02.class b/regression/jbmc-strings/Validate02/Validate02.class similarity index 100% rename from regression/strings/Validate02/Validate02.class rename to regression/jbmc-strings/Validate02/Validate02.class diff --git a/regression/strings/Validate02/Validate02.java b/regression/jbmc-strings/Validate02/Validate02.java similarity index 100% rename from regression/strings/Validate02/Validate02.java rename to regression/jbmc-strings/Validate02/Validate02.java diff --git a/regression/strings/Validate02/ValidateInput02.class b/regression/jbmc-strings/Validate02/ValidateInput02.class similarity index 100% rename from regression/strings/Validate02/ValidateInput02.class rename to regression/jbmc-strings/Validate02/ValidateInput02.class diff --git a/regression/strings/Validate02/ValidateInput02.java b/regression/jbmc-strings/Validate02/ValidateInput02.java similarity index 100% rename from regression/strings/Validate02/ValidateInput02.java rename to regression/jbmc-strings/Validate02/ValidateInput02.java diff --git a/regression/strings/Validate02/test.desc b/regression/jbmc-strings/Validate02/test.desc similarity index 100% rename from regression/strings/Validate02/test.desc rename to regression/jbmc-strings/Validate02/test.desc diff --git a/regression/strings/bug-test-gen-095/test.class b/regression/jbmc-strings/bug-test-gen-095/test.class similarity index 100% rename from regression/strings/bug-test-gen-095/test.class rename to regression/jbmc-strings/bug-test-gen-095/test.class diff --git a/regression/strings/bug-test-gen-095/test.desc b/regression/jbmc-strings/bug-test-gen-095/test.desc similarity index 100% rename from regression/strings/bug-test-gen-095/test.desc rename to regression/jbmc-strings/bug-test-gen-095/test.desc diff --git a/regression/strings/bug-test-gen-095/test.java b/regression/jbmc-strings/bug-test-gen-095/test.java similarity index 100% rename from regression/strings/bug-test-gen-095/test.java rename to regression/jbmc-strings/bug-test-gen-095/test.java diff --git a/regression/strings/bug-test-gen-119-2/StringValueOfLong.class b/regression/jbmc-strings/bug-test-gen-119-2/StringValueOfLong.class similarity index 100% rename from regression/strings/bug-test-gen-119-2/StringValueOfLong.class rename to regression/jbmc-strings/bug-test-gen-119-2/StringValueOfLong.class diff --git a/regression/strings/bug-test-gen-119-2/StringValueOfLong.java b/regression/jbmc-strings/bug-test-gen-119-2/StringValueOfLong.java similarity index 100% rename from regression/strings/bug-test-gen-119-2/StringValueOfLong.java rename to regression/jbmc-strings/bug-test-gen-119-2/StringValueOfLong.java diff --git a/regression/strings/bug-test-gen-119-2/test.desc b/regression/jbmc-strings/bug-test-gen-119-2/test.desc similarity index 100% rename from regression/strings/bug-test-gen-119-2/test.desc rename to regression/jbmc-strings/bug-test-gen-119-2/test.desc diff --git a/regression/strings/bug-test-gen-119/StringValueOfBool.class b/regression/jbmc-strings/bug-test-gen-119/StringValueOfBool.class similarity index 100% rename from regression/strings/bug-test-gen-119/StringValueOfBool.class rename to regression/jbmc-strings/bug-test-gen-119/StringValueOfBool.class diff --git a/regression/strings/bug-test-gen-119/StringValueOfBool.java b/regression/jbmc-strings/bug-test-gen-119/StringValueOfBool.java similarity index 100% rename from regression/strings/bug-test-gen-119/StringValueOfBool.java rename to regression/jbmc-strings/bug-test-gen-119/StringValueOfBool.java diff --git a/regression/strings/bug-test-gen-119/test.desc b/regression/jbmc-strings/bug-test-gen-119/test.desc similarity index 100% rename from regression/strings/bug-test-gen-119/test.desc rename to regression/jbmc-strings/bug-test-gen-119/test.desc diff --git a/regression/strings/java_append_char/test.desc b/regression/jbmc-strings/java_append_char/test.desc similarity index 100% rename from regression/strings/java_append_char/test.desc rename to regression/jbmc-strings/java_append_char/test.desc diff --git a/regression/strings/java_append_char/test_append_char.class b/regression/jbmc-strings/java_append_char/test_append_char.class similarity index 100% rename from regression/strings/java_append_char/test_append_char.class rename to regression/jbmc-strings/java_append_char/test_append_char.class diff --git a/regression/strings/java_append_char/test_append_char.java b/regression/jbmc-strings/java_append_char/test_append_char.java similarity index 100% rename from regression/strings/java_append_char/test_append_char.java rename to regression/jbmc-strings/java_append_char/test_append_char.java diff --git a/regression/strings/java_append_int/test.desc b/regression/jbmc-strings/java_append_int/test.desc similarity index 100% rename from regression/strings/java_append_int/test.desc rename to regression/jbmc-strings/java_append_int/test.desc diff --git a/regression/strings/java_append_int/test_append_int.class b/regression/jbmc-strings/java_append_int/test_append_int.class similarity index 100% rename from regression/strings/java_append_int/test_append_int.class rename to regression/jbmc-strings/java_append_int/test_append_int.class diff --git a/regression/strings/java_append_int/test_append_int.java b/regression/jbmc-strings/java_append_int/test_append_int.java similarity index 100% rename from regression/strings/java_append_int/test_append_int.java rename to regression/jbmc-strings/java_append_int/test_append_int.java diff --git a/regression/strings/java_append_object/test.desc b/regression/jbmc-strings/java_append_object/test.desc similarity index 100% rename from regression/strings/java_append_object/test.desc rename to regression/jbmc-strings/java_append_object/test.desc diff --git a/regression/strings/java_append_object/test_append_object.class b/regression/jbmc-strings/java_append_object/test_append_object.class similarity index 100% rename from regression/strings/java_append_object/test_append_object.class rename to regression/jbmc-strings/java_append_object/test_append_object.class diff --git a/regression/strings/java_append_object/test_append_object.java b/regression/jbmc-strings/java_append_object/test_append_object.java similarity index 100% rename from regression/strings/java_append_object/test_append_object.java rename to regression/jbmc-strings/java_append_object/test_append_object.java diff --git a/regression/strings/java_append_string/test.desc b/regression/jbmc-strings/java_append_string/test.desc similarity index 100% rename from regression/strings/java_append_string/test.desc rename to regression/jbmc-strings/java_append_string/test.desc diff --git a/regression/strings/java_append_string/test_append_string.class b/regression/jbmc-strings/java_append_string/test_append_string.class similarity index 100% rename from regression/strings/java_append_string/test_append_string.class rename to regression/jbmc-strings/java_append_string/test_append_string.class diff --git a/regression/strings/java_append_string/test_append_string.java b/regression/jbmc-strings/java_append_string/test_append_string.java similarity index 100% rename from regression/strings/java_append_string/test_append_string.java rename to regression/jbmc-strings/java_append_string/test_append_string.java diff --git a/regression/strings/java_case/test.desc b/regression/jbmc-strings/java_case/test.desc similarity index 100% rename from regression/strings/java_case/test.desc rename to regression/jbmc-strings/java_case/test.desc diff --git a/regression/strings/java_case/test_case.class b/regression/jbmc-strings/java_case/test_case.class similarity index 100% rename from regression/strings/java_case/test_case.class rename to regression/jbmc-strings/java_case/test_case.class diff --git a/regression/strings/java_case/test_case.java b/regression/jbmc-strings/java_case/test_case.java similarity index 100% rename from regression/strings/java_case/test_case.java rename to regression/jbmc-strings/java_case/test_case.java diff --git a/regression/strings/java_char_array/test.desc b/regression/jbmc-strings/java_char_array/test.desc similarity index 100% rename from regression/strings/java_char_array/test.desc rename to regression/jbmc-strings/java_char_array/test.desc diff --git a/regression/strings/java_char_array/test_char_array.class b/regression/jbmc-strings/java_char_array/test_char_array.class similarity index 100% rename from regression/strings/java_char_array/test_char_array.class rename to regression/jbmc-strings/java_char_array/test_char_array.class diff --git a/regression/strings/java_char_array/test_char_array.java b/regression/jbmc-strings/java_char_array/test_char_array.java similarity index 100% rename from regression/strings/java_char_array/test_char_array.java rename to regression/jbmc-strings/java_char_array/test_char_array.java diff --git a/regression/strings/java_char_array_init/test.desc b/regression/jbmc-strings/java_char_array_init/test.desc similarity index 100% rename from regression/strings/java_char_array_init/test.desc rename to regression/jbmc-strings/java_char_array_init/test.desc diff --git a/regression/strings/java_char_array_init/test_init.class b/regression/jbmc-strings/java_char_array_init/test_init.class similarity index 100% rename from regression/strings/java_char_array_init/test_init.class rename to regression/jbmc-strings/java_char_array_init/test_init.class diff --git a/regression/strings/java_char_array_init/test_init.java b/regression/jbmc-strings/java_char_array_init/test_init.java similarity index 100% rename from regression/strings/java_char_array_init/test_init.java rename to regression/jbmc-strings/java_char_array_init/test_init.java diff --git a/regression/strings/java_char_at/test.desc b/regression/jbmc-strings/java_char_at/test.desc similarity index 100% rename from regression/strings/java_char_at/test.desc rename to regression/jbmc-strings/java_char_at/test.desc diff --git a/regression/strings/java_char_at/test_char_at.class b/regression/jbmc-strings/java_char_at/test_char_at.class similarity index 100% rename from regression/strings/java_char_at/test_char_at.class rename to regression/jbmc-strings/java_char_at/test_char_at.class diff --git a/regression/strings/java_char_at/test_char_at.java b/regression/jbmc-strings/java_char_at/test_char_at.java similarity index 100% rename from regression/strings/java_char_at/test_char_at.java rename to regression/jbmc-strings/java_char_at/test_char_at.java diff --git a/regression/strings/java_code_point/test.desc b/regression/jbmc-strings/java_code_point/test.desc similarity index 100% rename from regression/strings/java_code_point/test.desc rename to regression/jbmc-strings/java_code_point/test.desc diff --git a/regression/strings/java_code_point/test_code_point.class b/regression/jbmc-strings/java_code_point/test_code_point.class similarity index 100% rename from regression/strings/java_code_point/test_code_point.class rename to regression/jbmc-strings/java_code_point/test_code_point.class diff --git a/regression/strings/java_code_point/test_code_point.java b/regression/jbmc-strings/java_code_point/test_code_point.java similarity index 100% rename from regression/strings/java_code_point/test_code_point.java rename to regression/jbmc-strings/java_code_point/test_code_point.java diff --git a/regression/strings/java_compare/test.desc b/regression/jbmc-strings/java_compare/test.desc similarity index 100% rename from regression/strings/java_compare/test.desc rename to regression/jbmc-strings/java_compare/test.desc diff --git a/regression/strings/java_compare/test_compare.class b/regression/jbmc-strings/java_compare/test_compare.class similarity index 100% rename from regression/strings/java_compare/test_compare.class rename to regression/jbmc-strings/java_compare/test_compare.class diff --git a/regression/strings/java_compare/test_compare.java b/regression/jbmc-strings/java_compare/test_compare.java similarity index 100% rename from regression/strings/java_compare/test_compare.java rename to regression/jbmc-strings/java_compare/test_compare.java diff --git a/regression/strings/java_concat/test.desc b/regression/jbmc-strings/java_concat/test.desc similarity index 100% rename from regression/strings/java_concat/test.desc rename to regression/jbmc-strings/java_concat/test.desc diff --git a/regression/strings/java_concat/test_concat.class b/regression/jbmc-strings/java_concat/test_concat.class similarity index 100% rename from regression/strings/java_concat/test_concat.class rename to regression/jbmc-strings/java_concat/test_concat.class diff --git a/regression/strings/java_concat/test_concat.java b/regression/jbmc-strings/java_concat/test_concat.java similarity index 100% rename from regression/strings/java_concat/test_concat.java rename to regression/jbmc-strings/java_concat/test_concat.java diff --git a/regression/strings/java_contains/test.desc b/regression/jbmc-strings/java_contains/test.desc similarity index 100% rename from regression/strings/java_contains/test.desc rename to regression/jbmc-strings/java_contains/test.desc diff --git a/regression/strings/java_contains/test_contains.class b/regression/jbmc-strings/java_contains/test_contains.class similarity index 100% rename from regression/strings/java_contains/test_contains.class rename to regression/jbmc-strings/java_contains/test_contains.class diff --git a/regression/strings/java_contains/test_contains.java b/regression/jbmc-strings/java_contains/test_contains.java similarity index 100% rename from regression/strings/java_contains/test_contains.java rename to regression/jbmc-strings/java_contains/test_contains.java diff --git a/regression/strings/java_delete/test.desc b/regression/jbmc-strings/java_delete/test.desc similarity index 100% rename from regression/strings/java_delete/test.desc rename to regression/jbmc-strings/java_delete/test.desc diff --git a/regression/strings/java_delete/test_delete.class b/regression/jbmc-strings/java_delete/test_delete.class similarity index 100% rename from regression/strings/java_delete/test_delete.class rename to regression/jbmc-strings/java_delete/test_delete.class diff --git a/regression/strings/java_delete/test_delete.java b/regression/jbmc-strings/java_delete/test_delete.java similarity index 100% rename from regression/strings/java_delete/test_delete.java rename to regression/jbmc-strings/java_delete/test_delete.java diff --git a/regression/strings/java_delete_char_at/test.desc b/regression/jbmc-strings/java_delete_char_at/test.desc similarity index 100% rename from regression/strings/java_delete_char_at/test.desc rename to regression/jbmc-strings/java_delete_char_at/test.desc diff --git a/regression/strings/java_delete_char_at/test_delete_char_at.class b/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class similarity index 100% rename from regression/strings/java_delete_char_at/test_delete_char_at.class rename to regression/jbmc-strings/java_delete_char_at/test_delete_char_at.class diff --git a/regression/strings/java_delete_char_at/test_delete_char_at.java b/regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java similarity index 100% rename from regression/strings/java_delete_char_at/test_delete_char_at.java rename to regression/jbmc-strings/java_delete_char_at/test_delete_char_at.java diff --git a/regression/strings/java_easychair/easychair.class b/regression/jbmc-strings/java_easychair/easychair.class similarity index 100% rename from regression/strings/java_easychair/easychair.class rename to regression/jbmc-strings/java_easychair/easychair.class diff --git a/regression/strings/java_easychair/easychair.java b/regression/jbmc-strings/java_easychair/easychair.java similarity index 100% rename from regression/strings/java_easychair/easychair.java rename to regression/jbmc-strings/java_easychair/easychair.java diff --git a/regression/strings/java_easychair/test.desc b/regression/jbmc-strings/java_easychair/test.desc similarity index 100% rename from regression/strings/java_easychair/test.desc rename to regression/jbmc-strings/java_easychair/test.desc diff --git a/regression/strings/java_empty/test.desc b/regression/jbmc-strings/java_empty/test.desc similarity index 100% rename from regression/strings/java_empty/test.desc rename to regression/jbmc-strings/java_empty/test.desc diff --git a/regression/strings/java_empty/test_empty.class b/regression/jbmc-strings/java_empty/test_empty.class similarity index 100% rename from regression/strings/java_empty/test_empty.class rename to regression/jbmc-strings/java_empty/test_empty.class diff --git a/regression/strings/java_empty/test_empty.java b/regression/jbmc-strings/java_empty/test_empty.java similarity index 100% rename from regression/strings/java_empty/test_empty.java rename to regression/jbmc-strings/java_empty/test_empty.java diff --git a/regression/strings/java_endswith/test.desc b/regression/jbmc-strings/java_endswith/test.desc similarity index 100% rename from regression/strings/java_endswith/test.desc rename to regression/jbmc-strings/java_endswith/test.desc diff --git a/regression/strings/java_endswith/test_endswith.class b/regression/jbmc-strings/java_endswith/test_endswith.class similarity index 100% rename from regression/strings/java_endswith/test_endswith.class rename to regression/jbmc-strings/java_endswith/test_endswith.class diff --git a/regression/strings/java_endswith/test_endswith.java b/regression/jbmc-strings/java_endswith/test_endswith.java similarity index 100% rename from regression/strings/java_endswith/test_endswith.java rename to regression/jbmc-strings/java_endswith/test_endswith.java diff --git a/regression/strings/java_equal/test.desc b/regression/jbmc-strings/java_equal/test.desc similarity index 100% rename from regression/strings/java_equal/test.desc rename to regression/jbmc-strings/java_equal/test.desc diff --git a/regression/strings/java_equal/test_equal.class b/regression/jbmc-strings/java_equal/test_equal.class similarity index 100% rename from regression/strings/java_equal/test_equal.class rename to regression/jbmc-strings/java_equal/test_equal.class diff --git a/regression/strings/java_equal/test_equal.java b/regression/jbmc-strings/java_equal/test_equal.java similarity index 100% rename from regression/strings/java_equal/test_equal.java rename to regression/jbmc-strings/java_equal/test_equal.java diff --git a/regression/strings/java_float/test.desc b/regression/jbmc-strings/java_float/test.desc similarity index 100% rename from regression/strings/java_float/test.desc rename to regression/jbmc-strings/java_float/test.desc diff --git a/regression/strings/java_float/test_float.class b/regression/jbmc-strings/java_float/test_float.class similarity index 100% rename from regression/strings/java_float/test_float.class rename to regression/jbmc-strings/java_float/test_float.class diff --git a/regression/strings/java_float/test_float.java b/regression/jbmc-strings/java_float/test_float.java similarity index 100% rename from regression/strings/java_float/test_float.java rename to regression/jbmc-strings/java_float/test_float.java diff --git a/regression/strings/java_hash_code/test.desc b/regression/jbmc-strings/java_hash_code/test.desc similarity index 100% rename from regression/strings/java_hash_code/test.desc rename to regression/jbmc-strings/java_hash_code/test.desc diff --git a/regression/strings/java_hash_code/test_hash_code.class b/regression/jbmc-strings/java_hash_code/test_hash_code.class similarity index 100% rename from regression/strings/java_hash_code/test_hash_code.class rename to regression/jbmc-strings/java_hash_code/test_hash_code.class diff --git a/regression/strings/java_hash_code/test_hash_code.java b/regression/jbmc-strings/java_hash_code/test_hash_code.java similarity index 100% rename from regression/strings/java_hash_code/test_hash_code.java rename to regression/jbmc-strings/java_hash_code/test_hash_code.java diff --git a/regression/strings/java_index_of/test.desc b/regression/jbmc-strings/java_index_of/test.desc similarity index 100% rename from regression/strings/java_index_of/test.desc rename to regression/jbmc-strings/java_index_of/test.desc diff --git a/regression/strings/java_index_of/test_index_of.class b/regression/jbmc-strings/java_index_of/test_index_of.class similarity index 100% rename from regression/strings/java_index_of/test_index_of.class rename to regression/jbmc-strings/java_index_of/test_index_of.class diff --git a/regression/strings/java_index_of/test_index_of.java b/regression/jbmc-strings/java_index_of/test_index_of.java similarity index 100% rename from regression/strings/java_index_of/test_index_of.java rename to regression/jbmc-strings/java_index_of/test_index_of.java diff --git a/regression/strings/java_index_of_char/test.desc b/regression/jbmc-strings/java_index_of_char/test.desc similarity index 100% rename from regression/strings/java_index_of_char/test.desc rename to regression/jbmc-strings/java_index_of_char/test.desc diff --git a/regression/strings/java_index_of_char/test_index_of_char.class b/regression/jbmc-strings/java_index_of_char/test_index_of_char.class similarity index 100% rename from regression/strings/java_index_of_char/test_index_of_char.class rename to regression/jbmc-strings/java_index_of_char/test_index_of_char.class diff --git a/regression/strings/java_index_of_char/test_index_of_char.java b/regression/jbmc-strings/java_index_of_char/test_index_of_char.java similarity index 100% rename from regression/strings/java_index_of_char/test_index_of_char.java rename to regression/jbmc-strings/java_index_of_char/test_index_of_char.java diff --git a/regression/strings/java_insert_char/test.desc b/regression/jbmc-strings/java_insert_char/test.desc similarity index 100% rename from regression/strings/java_insert_char/test.desc rename to regression/jbmc-strings/java_insert_char/test.desc diff --git a/regression/strings/java_insert_char/test_insert_char.class b/regression/jbmc-strings/java_insert_char/test_insert_char.class similarity index 100% rename from regression/strings/java_insert_char/test_insert_char.class rename to regression/jbmc-strings/java_insert_char/test_insert_char.class diff --git a/regression/strings/java_insert_char/test_insert_char.java b/regression/jbmc-strings/java_insert_char/test_insert_char.java similarity index 100% rename from regression/strings/java_insert_char/test_insert_char.java rename to regression/jbmc-strings/java_insert_char/test_insert_char.java diff --git a/regression/strings/java_insert_char_array/test.desc b/regression/jbmc-strings/java_insert_char_array/test.desc similarity index 100% rename from regression/strings/java_insert_char_array/test.desc rename to regression/jbmc-strings/java_insert_char_array/test.desc diff --git a/regression/strings/java_insert_char_array/test_insert_char_array.class b/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class similarity index 100% rename from regression/strings/java_insert_char_array/test_insert_char_array.class rename to regression/jbmc-strings/java_insert_char_array/test_insert_char_array.class diff --git a/regression/strings/java_insert_char_array/test_insert_char_array.java b/regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java similarity index 100% rename from regression/strings/java_insert_char_array/test_insert_char_array.java rename to regression/jbmc-strings/java_insert_char_array/test_insert_char_array.java diff --git a/regression/strings/java_insert_int/test.desc b/regression/jbmc-strings/java_insert_int/test.desc similarity index 100% rename from regression/strings/java_insert_int/test.desc rename to regression/jbmc-strings/java_insert_int/test.desc diff --git a/regression/strings/java_insert_int/test_insert_int.class b/regression/jbmc-strings/java_insert_int/test_insert_int.class similarity index 100% rename from regression/strings/java_insert_int/test_insert_int.class rename to regression/jbmc-strings/java_insert_int/test_insert_int.class diff --git a/regression/strings/java_insert_int/test_insert_int.java b/regression/jbmc-strings/java_insert_int/test_insert_int.java similarity index 100% rename from regression/strings/java_insert_int/test_insert_int.java rename to regression/jbmc-strings/java_insert_int/test_insert_int.java diff --git a/regression/strings/java_insert_multiple/test.desc b/regression/jbmc-strings/java_insert_multiple/test.desc similarity index 100% rename from regression/strings/java_insert_multiple/test.desc rename to regression/jbmc-strings/java_insert_multiple/test.desc diff --git a/regression/strings/java_insert_multiple/test_insert_multiple.class b/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class similarity index 100% rename from regression/strings/java_insert_multiple/test_insert_multiple.class rename to regression/jbmc-strings/java_insert_multiple/test_insert_multiple.class diff --git a/regression/strings/java_insert_multiple/test_insert_multiple.java b/regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java similarity index 100% rename from regression/strings/java_insert_multiple/test_insert_multiple.java rename to regression/jbmc-strings/java_insert_multiple/test_insert_multiple.java diff --git a/regression/strings/java_insert_string/test.desc b/regression/jbmc-strings/java_insert_string/test.desc similarity index 100% rename from regression/strings/java_insert_string/test.desc rename to regression/jbmc-strings/java_insert_string/test.desc diff --git a/regression/strings/java_insert_string/test_insert_string.class b/regression/jbmc-strings/java_insert_string/test_insert_string.class similarity index 100% rename from regression/strings/java_insert_string/test_insert_string.class rename to regression/jbmc-strings/java_insert_string/test_insert_string.class diff --git a/regression/strings/java_insert_string/test_insert_string.java b/regression/jbmc-strings/java_insert_string/test_insert_string.java similarity index 100% rename from regression/strings/java_insert_string/test_insert_string.java rename to regression/jbmc-strings/java_insert_string/test_insert_string.java diff --git a/regression/strings-smoke-tests/CMakeLists.txt b/regression/strings-smoke-tests/CMakeLists.txt index 93d5ee716c2..afe0ea5761a 100644 --- a/regression/strings-smoke-tests/CMakeLists.txt +++ b/regression/strings-smoke-tests/CMakeLists.txt @@ -1,3 +1,3 @@ add_test_pl_tests( - "$" + "$" ) diff --git a/regression/strings-smoke-tests/Makefile b/regression/strings-smoke-tests/Makefile index 47653a6bb95..e45465e6130 100644 --- a/regression/strings-smoke-tests/Makefile +++ b/regression/strings-smoke-tests/Makefile @@ -1,25 +1,25 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ ../failed-tests-printer.pl ; \ exit 1 ; \ fi testfuture: - @if ! ../test.pl -c ../../../src/cbmc/cbmc -CF ; then \ + @if ! ../test.pl -c ../../../src/jbmc/jbmc -CF ; then \ ../failed-tests-printer.pl ; \ exit 1 ; \ fi testall: - @if ! ../test.pl -c ../../../src/cbmc/cbmc -CFTK ; then \ + @if ! ../test.pl -c ../../../src/jbmc/jbmc -CFTK ; then \ ../failed-tests-printer.pl ; \ exit 1 ; \ fi tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ + @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ ../failed-tests-printer.pl ; \ exit 1 ; \ fi diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ce01df62dda..c31b786d588 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -108,7 +108,9 @@ add_subdirectory(xmllang) add_subdirectory(java_bytecode) add_subdirectory(miniz) add_subdirectory(clobber) + add_subdirectory(cbmc) +add_subdirectory(jbmc) add_subdirectory(goto-cc) add_subdirectory(goto-instrument) add_subdirectory(goto-analyzer) diff --git a/src/Makefile b/src/Makefile index 191022c8792..447218d3291 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,10 +1,11 @@ -DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \ +DIRS = ansi-c big-int cbmc jbmc cpp goto-cc goto-instrument goto-programs \ goto-symex langapi pointer-analysis solvers util linking xmllang \ assembler analyses java_bytecode \ json goto-analyzer jsil goto-diff clobber \ memory-models miniz -all: cbmc.dir goto-cc.dir goto-instrument.dir goto-analyzer.dir goto-diff.dir +all: cbmc.dir jbmc.dir goto-cc.dir goto-instrument.dir \ + goto-analyzer.dir goto-diff.dir ############################################################################### @@ -18,9 +19,11 @@ $(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir cpp.dir: ansi-c.dir linking.dir +java_bytecode.dir: miniz.dir + languages: util.dir langapi.dir \ cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir \ - jsil.dir miniz.dir + jsil.dir goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \ goto-symex.dir linking.dir analyses.dir solvers.dir \ @@ -30,6 +33,8 @@ cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \ pointer-analysis.dir goto-programs.dir linking.dir \ goto-instrument.dir +jbmc.dir: java_bytecode.dir cbmc.dir + goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \ json.dir goto-instrument.dir diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt index 6777249c8d9..44fbb0170d1 100644 --- a/src/cbmc/CMakeLists.txt +++ b/src/cbmc/CMakeLists.txt @@ -9,31 +9,27 @@ add_library(cbmc-lib ${sources} ${headers}) generic_includes(cbmc-lib) target_link_libraries(cbmc-lib + analyses ansi-c - cpp - linking + assembler big-int + cpp + goto-instrument-lib goto-programs goto-symex - pointer-analysis - goto-instrument-lib - analyses + java_bytecode + json langapi - xml - assembler + linking + pointer-analysis solvers util - json + xml ) add_if_library(cbmc-lib bv_refinement) -add_if_library(cbmc-lib java_bytecode) add_if_library(cbmc-lib jsil) -add_if_library(cbmc-lib specc) -add_if_library(cbmc-lib php) # Executable add_executable(cbmc cbmc_main.cpp) target_link_libraries(cbmc cbmc-lib) - -install(TARGETS cbmc DESTINATION bin) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 4d890b0b5fa..74e73632d96 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -40,7 +40,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../solvers/solvers$(LIBEXT) \ ../util/util$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) \ ../json/json$(LIBEXT) INCLUDES= -I .. diff --git a/src/cbmc/cbmc_languages.cpp b/src/cbmc/cbmc_languages.cpp index 06b919b9cc4..55cc8cda97d 100644 --- a/src/cbmc/cbmc_languages.cpp +++ b/src/cbmc/cbmc_languages.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #ifdef HAVE_JSIL #include @@ -25,7 +24,6 @@ void cbmc_parse_optionst::register_languages() { register_language(new_ansi_c_language); register_language(new_cpp_language); - register_language(new_java_bytecode_language); #ifdef HAVE_JSIL register_language(new_jsil_language); diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b9da1f18c1c..268529ba089 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -35,7 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -45,7 +44,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -64,8 +62,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "java_bytecode/java_bytecode_language.h" - #include "cbmc_solvers.h" #include "bmc.h" #include "version.h" @@ -192,10 +188,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); - // unwind loops in java enum static initialization - if(cmdline.isset("java-unwind-enum-static")) - options.set_option("java-unwind-enum-static", true); - // check assertions if(cmdline.isset("no-assertions")) options.set_option("assertions", false); @@ -545,11 +537,6 @@ int cbmc_parse_optionst::doit() if(set_properties()) return 7; // should contemplate EX_USAGE from sysexits.h - // unwinds loops to number of enum elements - // side effect: add this as explicit unwind to unwind set - if(options.get_bool_option("java-unwind-enum-static")) - remove_static_init_loops(goto_model, options, get_message_handler()); - // get solver cbmc_solverst cbmc_solvers( options, @@ -757,12 +744,8 @@ bool cbmc_parse_optionst::process_goto_program( get_message_handler(), goto_model, cmdline.isset("pointer-check")); - // Java virtual functions -> explicit dispatch tables: - remove_virtual_functions(goto_model); // remove catch and throw (introduces instanceof) remove_exceptions(goto_model); - // Similar removal of RTTI inspection: - remove_instanceof(goto_model); mm_io(goto_model); @@ -775,30 +758,6 @@ bool cbmc_parse_optionst::process_goto_program( remove_complex(goto_model); rewrite_union(goto_model); - // Similar removal of java nondet statements: - // TODO Should really get this from java_bytecode_language somehow, but we - // don't have an instance of that here. - object_factory_parameterst factory_params; - factory_params.max_nondet_array_length= - cmdline.isset("java-max-input-array-length") - ? std::stoul(cmdline.get_value("java-max-input-array-length")) - : MAX_NONDET_ARRAY_LENGTH_DEFAULT; - factory_params.max_nondet_string_length= - cmdline.isset("string-max-input-length") - ? std::stoul(cmdline.get_value("string-max-input-length")) - : MAX_NONDET_STRING_LENGTH; - factory_params.max_nondet_tree_depth= - cmdline.isset("java-max-input-tree-depth") - ? std::stoul(cmdline.get_value("java-max-input-tree-depth")) - : MAX_NONDET_TREE_DEPTH; - - replace_java_nondet(goto_model); - - convert_nondet( - goto_model, - get_message_handler(), - factory_params); - // add generic checks status() << "Generic Property Instrumentation" << eom; goto_check(options, goto_model); @@ -873,7 +832,6 @@ bool cbmc_parse_optionst::process_goto_program( // remove any skips introduced since coverage instrumentation remove_skip(goto_model); - goto_model.goto_functions.update(); } catch(const char *e) @@ -1014,14 +972,6 @@ void cbmc_parse_optionst::help() " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) "\n" - "Java Bytecode frontend options:\n" - " --classpath dir/jar set the classpath\n" - " --main-class class-name set the name of the main class\n" - JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP - // This one is handled by cbmc_parse_options not by the Java frontend, - // hence its presence here: - " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" - "\n" "Semantic transformations:\n" // NOLINTNEXTLINE(whitespace/line_length) " --nondet-static add nondeterministic initialization of variables with static lifetime\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 7ce7e05dc9f..cd837e90d9b 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include "xml_interface.h" class bmct; @@ -34,7 +32,6 @@ class optionst; "(document-subgoals)(outfile):(test-preprocessor)" \ "D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \ "(object-bits):" \ - "(classpath):(cp):(main-class):" \ "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \ OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ @@ -67,8 +64,6 @@ class optionst; "(string-abstraction)(no-arch)(arch):" \ "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ "(graphml-witness):" \ - JAVA_BYTECODE_LANGUAGE_OPTIONS \ - "(java-unwind-enum-static)" \ "(localize-faults)(localize-faults-method):" \ "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp index 231ed117f31..4ce2a74fb04 100644 --- a/src/goto-programs/remove_skip.cpp +++ b/src/goto-programs/remove_skip.cpp @@ -157,6 +157,9 @@ void remove_skip(goto_functionst &goto_functions) { Forall_goto_functions(f_it, goto_functions) remove_skip(f_it->second.body); + + // we may remove targets + goto_functions.update(); } void remove_skip(goto_modelt &goto_model) diff --git a/src/jbmc/CMakeLists.txt b/src/jbmc/CMakeLists.txt new file mode 100644 index 00000000000..062c8f872d9 --- /dev/null +++ b/src/jbmc/CMakeLists.txt @@ -0,0 +1,36 @@ +# Library +file(GLOB_RECURSE sources "*.cpp") +file(GLOB_RECURSE headers "*.h") +list(REMOVE_ITEM sources + ${CMAKE_CURRENT_SOURCE_DIR}/jbmc_main.cpp +) +add_library(jbmc-lib ${sources} ${headers}) + +generic_includes(jbmc-lib) + +target_link_libraries(jbmc-lib + analyses + ansi-c + assembler + big-int + cbmc-lib + cpp + goto-instrument-lib + goto-programs + goto-symex + java_bytecode + json + langapi + linking + pointer-analysis + solvers + util + xml +) + +add_if_library(jbmc-lib bv_refinement) +add_if_library(jbmc-lib jsil) + +# Executable +add_executable(jbmc jbmc_main.cpp) +target_link_libraries(jbmc jbmc-lib) diff --git a/src/jbmc/Makefile b/src/jbmc/Makefile new file mode 100644 index 00000000000..bd6a2b5d962 --- /dev/null +++ b/src/jbmc/Makefile @@ -0,0 +1,63 @@ +SRC = jbmc_main.cpp \ + jbmc_parse_options.cpp \ + # Empty last line + +OBJ += ../ansi-c/ansi-c$(LIBEXT) \ + ../java_bytecode/java_bytecode$(LIBEXT) \ + ../linking/linking$(LIBEXT) \ + ../big-int/big-int$(LIBEXT) \ + ../goto-programs/goto-programs$(LIBEXT) \ + ../goto-symex/goto-symex$(LIBEXT) \ + ../pointer-analysis/value_set$(OBJEXT) \ + ../pointer-analysis/value_set_analysis_fi$(OBJEXT) \ + ../pointer-analysis/value_set_domain_fi$(OBJEXT) \ + ../pointer-analysis/value_set_fi$(OBJEXT) \ + ../pointer-analysis/value_set_dereference$(OBJEXT) \ + ../pointer-analysis/dereference_callback$(OBJEXT) \ + ../pointer-analysis/add_failed_symbols$(OBJEXT) \ + ../pointer-analysis/rewrite_index$(OBJEXT) \ + ../pointer-analysis/goto_program_dereference$(OBJEXT) \ + ../goto-instrument/full_slicer$(OBJEXT) \ + ../goto-instrument/nondet_static$(OBJEXT) \ + ../goto-instrument/cover$(OBJEXT) \ + ../analyses/analyses$(LIBEXT) \ + ../langapi/langapi$(LIBEXT) \ + ../xmllang/xmllang$(LIBEXT) \ + ../assembler/assembler$(LIBEXT) \ + ../solvers/solvers$(LIBEXT) \ + ../util/util$(LIBEXT) \ + ../miniz/miniz$(OBJEXT) \ + ../json/json$(LIBEXT) \ + ../cbmc/all_properties$(OBJEXT) \ + ../cbmc/bmc$(OBJEXT) \ + ../cbmc/bmc_cover$(OBJEXT) \ + ../cbmc/bv_cbmc$(OBJEXT) \ + ../cbmc/cbmc_dimacs$(OBJEXT) \ + ../cbmc/cbmc_solvers$(OBJEXT) \ + ../cbmc/counterexample_beautification$(OBJEXT) \ + ../cbmc/fault_localization$(OBJEXT) \ + ../cbmc/show_vcc$(OBJEXT) \ + ../cbmc/symex_bmc$(OBJEXT) \ + ../cbmc/symex_coverage$(OBJEXT) \ + # Empty last line + +INCLUDES= -I .. + +LIBS = + +include ../config.inc +include ../common + +CLEANFILES = jbmc$(EXEEXT) + +all: jbmc$(EXEEXT) + +############################################################################### + +jbmc$(EXEEXT): $(OBJ) + $(LINKBIN) + +.PHONY: jbmc-mac-signed + +jbmc-mac-signed: jbmc$(EXEEXT) + strip jbmc$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) jbmc$(EXEEXT) diff --git a/src/jbmc/jbmc_main.cpp b/src/jbmc/jbmc_main.cpp new file mode 100644 index 00000000000..eb4c0974830 --- /dev/null +++ b/src/jbmc/jbmc_main.cpp @@ -0,0 +1,55 @@ +/*******************************************************************\ + +Module: CBMC Main Module + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// CBMC Main Module + +/* + + JBMC + Bounded Model Checking for Java + Copyright (C) 2017 Daniel Kroening + +*/ + +#include "jbmc_parse_options.h" + +#include + +#ifdef IREP_HASH_STATS +#include +#endif + +#ifdef IREP_HASH_STATS +extern unsigned long long irep_hash_cnt; +extern unsigned long long irep_cmp_cnt; +extern unsigned long long irep_cmp_ne_cnt; +#endif + +#ifdef _MSC_VER +int wmain(int argc, const wchar_t **argv_wide) +{ + auto vec=narrow_argv(argc, argv_wide); + auto narrow=to_c_str_array(std::begin(vec), std::end(vec)); + auto argv=narrow.data(); +#else +int main(int argc, const char **argv) +{ +#endif + jbmc_parse_optionst parse_options(argc, argv); + + int res=parse_options.main(); + + #ifdef IREP_HASH_STATS + std::cout << "IREP_HASH_CNT=" << irep_hash_cnt << '\n'; + std::cout << "IREP_CMP_CNT=" << irep_cmp_cnt << '\n'; + std::cout << "IREP_CMP_NE_CNT=" << irep_cmp_ne_cnt << '\n'; + #endif + + return res; +} diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp new file mode 100644 index 00000000000..9a0294f0ce7 --- /dev/null +++ b/src/jbmc/jbmc_parse_options.cpp @@ -0,0 +1,919 @@ +/*******************************************************************\ + +Module: JBMC Command Line Option Processing + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// JBMC Command Line Option Processing + +#include "jbmc_parse_options.h" + +#include +#include // exit() +#include +#include + +#include +#include +#include +#include +#include +#include + +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include +#include + +#include +#include +#include + +#include + +#include + +#include + +#include +#include +#include + +jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv): + parse_options_baset(JBMC_OPTIONS, argc, argv), + messaget(ui_message_handler), + ui_message_handler(cmdline, "JBMC " CBMC_VERSION) +{ +} + +::jbmc_parse_optionst::jbmc_parse_optionst( + int argc, + const char **argv, + const std::string &extra_options): + parse_options_baset(JBMC_OPTIONS+extra_options, argc, argv), + messaget(ui_message_handler), + ui_message_handler(cmdline, "JBMC " CBMC_VERSION) +{ +} + +void jbmc_parse_optionst::eval_verbosity() +{ + // this is our default verbosity + unsigned int v=messaget::M_STATISTICS; + + if(cmdline.isset("verbosity")) + { + v=unsafe_string2unsigned(cmdline.get_value("verbosity")); + if(v>10) + v=10; + } + + ui_message_handler.set_verbosity(v); +} + +void jbmc_parse_optionst::get_command_line_options(optionst &options) +{ + if(config.set(cmdline)) + { + usage_error(); + exit(1); // should contemplate EX_USAGE from sysexits.h + } + + if(cmdline.isset("program-only")) + options.set_option("program-only", true); + + if(cmdline.isset("show-vcc")) + options.set_option("show-vcc", true); + + if(cmdline.isset("cover")) + options.set_option("cover", cmdline.get_values("cover")); + + if(cmdline.isset("no-simplify")) + options.set_option("simplify", false); + else + options.set_option("simplify", true); + + if(cmdline.isset("stop-on-fail") || + cmdline.isset("dimacs") || + cmdline.isset("outfile")) + options.set_option("stop-on-fail", true); + else + options.set_option("stop-on-fail", false); + + if(cmdline.isset("trace") || + cmdline.isset("stop-on-fail")) + options.set_option("trace", true); + + if(cmdline.isset("localize-faults")) + options.set_option("localize-faults", true); + if(cmdline.isset("localize-faults-method")) + { + options.set_option( + "localize-faults-method", + cmdline.get_value("localize-faults-method")); + } + + if(cmdline.isset("unwind")) + options.set_option("unwind", cmdline.get_value("unwind")); + + if(cmdline.isset("depth")) + options.set_option("depth", cmdline.get_value("depth")); + + if(cmdline.isset("debug-level")) + options.set_option("debug-level", cmdline.get_value("debug-level")); + + if(cmdline.isset("slice-by-trace")) + options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace")); + + if(cmdline.isset("unwindset")) + options.set_option("unwindset", cmdline.get_value("unwindset")); + + // constant propagation + if(cmdline.isset("no-propagation")) + options.set_option("propagation", false); + else + options.set_option("propagation", true); + + // all checks supported by goto_check + PARSE_OPTIONS_GOTO_CHECK(cmdline, options); + + // unwind loops in java enum static initialization + if(cmdline.isset("java-unwind-enum-static")) + options.set_option("java-unwind-enum-static", true); + + // check assertions + if(cmdline.isset("no-assertions")) + options.set_option("assertions", false); + else + options.set_option("assertions", true); + + // use assumptions + if(cmdline.isset("no-assumptions")) + options.set_option("assumptions", false); + else + options.set_option("assumptions", true); + + // magic error label + if(cmdline.isset("error-label")) + options.set_option("error-label", cmdline.get_values("error-label")); + + // generate unwinding assertions + if(cmdline.isset("cover")) + options.set_option("unwinding-assertions", false); + else + { + options.set_option( + "unwinding-assertions", + cmdline.isset("unwinding-assertions")); + } + + // generate unwinding assumptions otherwise + options.set_option( + "partial-loops", + cmdline.isset("partial-loops")); + + if(options.get_bool_option("partial-loops") && + options.get_bool_option("unwinding-assertions")) + { + error() << "--partial-loops and --unwinding-assertions " + << "must not be given together" << eom; + exit(1); // should contemplate EX_USAGE from sysexits.h + } + + // remove unused equations + options.set_option( + "slice-formula", + cmdline.isset("slice-formula")); + + // simplify if conditions and branches + if(cmdline.isset("no-simplify-if")) + options.set_option("simplify-if", false); + else + options.set_option("simplify-if", true); + + if(cmdline.isset("arrays-uf-always")) + options.set_option("arrays-uf", "always"); + else if(cmdline.isset("arrays-uf-never")) + options.set_option("arrays-uf", "never"); + else + options.set_option("arrays-uf", "auto"); + + if(cmdline.isset("dimacs")) + options.set_option("dimacs", true); + + if(cmdline.isset("refine-arrays")) + { + options.set_option("refine", true); + options.set_option("refine-arrays", true); + } + + if(cmdline.isset("refine-arithmetic")) + { + options.set_option("refine", true); + options.set_option("refine-arithmetic", true); + } + + if(cmdline.isset("refine")) + { + options.set_option("refine", true); + options.set_option("refine-arrays", true); + options.set_option("refine-arithmetic", true); + } + + if(cmdline.isset("refine-strings")) + { + options.set_option("refine-strings", true); + options.set_option("string-non-empty", cmdline.isset("string-non-empty")); + options.set_option("string-printable", cmdline.isset("string-printable")); + if(cmdline.isset("string-max-length")) + options.set_option( + "string-max-length", cmdline.get_value("string-max-length")); + } + + if(cmdline.isset("max-node-refinement")) + options.set_option( + "max-node-refinement", + cmdline.get_value("max-node-refinement")); + + // SMT Options + bool version_set=false; + + if(cmdline.isset("smt1")) + { + options.set_option("smt1", true); + options.set_option("smt2", false); + version_set=true; + } + + if(cmdline.isset("smt2")) + { + // If both are given, smt2 takes precedence + options.set_option("smt1", false); + options.set_option("smt2", true); + version_set=true; + } + + if(cmdline.isset("fpa")) + options.set_option("fpa", true); + + bool solver_set=false; + + if(cmdline.isset("boolector")) + { + options.set_option("boolector", true), solver_set=true; + if(!version_set) + options.set_option("smt2", true), version_set=true; + } + + if(cmdline.isset("mathsat")) + { + options.set_option("mathsat", true), solver_set=true; + if(!version_set) + options.set_option("smt2", true), version_set=true; + } + + if(cmdline.isset("cvc3")) + { + options.set_option("cvc3", true), solver_set=true; + if(!version_set) + options.set_option("smt1", true), version_set=true; + } + + if(cmdline.isset("cvc4")) + { + options.set_option("cvc4", true), solver_set=true; + if(!version_set) + options.set_option("smt2", true), version_set=true; + } + + if(cmdline.isset("yices")) + { + options.set_option("yices", true), solver_set=true; + if(!version_set) + options.set_option("smt2", true), version_set=true; + } + + if(cmdline.isset("z3")) + { + options.set_option("z3", true), solver_set=true; + if(!version_set) + options.set_option("smt2", true), version_set=true; + } + + if(cmdline.isset("opensmt")) + { + options.set_option("opensmt", true), solver_set=true; + if(!version_set) + options.set_option("smt1", true), version_set=true; + } + + if(version_set && !solver_set) + { + if(cmdline.isset("outfile")) + { + // outfile and no solver should give standard compliant SMT-LIB + options.set_option("generic", true), solver_set=true; + } + else + { + if(options.get_bool_option("smt1")) + { + options.set_option("boolector", true), solver_set=true; + } + else + { + INVARIANT(options.get_bool_option("smt2"), "smt2 set"); + options.set_option("z3", true), solver_set=true; + } + } + } + + // Either have solver and standard version set, or neither. + INVARIANT(version_set==solver_set, "solver and version set"); + + if(cmdline.isset("beautify")) + options.set_option("beautify", true); + + if(cmdline.isset("no-sat-preprocessor")) + options.set_option("sat-preprocessor", false); + else + options.set_option("sat-preprocessor", true); + + options.set_option( + "pretty-names", + !cmdline.isset("no-pretty-names")); + + if(cmdline.isset("outfile")) + options.set_option("outfile", cmdline.get_value("outfile")); + + if(cmdline.isset("graphml-witness")) + { + options.set_option("graphml-witness", cmdline.get_value("graphml-witness")); + options.set_option("stop-on-fail", true); + options.set_option("trace", true); + } + + if(cmdline.isset("symex-coverage-report")) + options.set_option( + "symex-coverage-report", + cmdline.get_value("symex-coverage-report")); +} + +/// invoke main modules +int jbmc_parse_optionst::doit() +{ + if(cmdline.isset("version")) + { + std::cout << CBMC_VERSION << '\n'; + return 0; // should contemplate EX_OK from sysexits.h + } + + // + // command line options + // + + optionst options; + try + { + get_command_line_options(options); + } + + catch(const char *error_msg) + { + error() << error_msg << eom; + return 6; // should contemplate EX_SOFTWARE from sysexits.h + } + + catch(const std::string error_msg) + { + error() << error_msg << eom; + return 6; // should contemplate EX_SOFTWARE from sysexits.h + } + + eval_verbosity(); + + // + // Print a banner + // + status() << "JBMC version " CBMC_VERSION " " + << sizeof(void *)*8 << "-bit " + << config.this_architecture() << " " + << config.this_operating_system() << eom; + + register_language(new_ansi_c_language); + register_language(new_java_bytecode_language); + + if(cmdline.isset("show-parse-tree")) + { + if(cmdline.args.size()!=1) + { + error() << "Please give exactly one source file" << eom; + return 6; + } + + std::string filename=cmdline.args[0]; + + #ifdef _MSC_VER + std::ifstream infile(widen(filename)); + #else + std::ifstream infile(filename); + #endif + + if(!infile) + { + error() << "failed to open input file `" + << filename << "'" << eom; + return 6; + } + + std::unique_ptr language= + get_language_from_filename(filename); + + if(language==nullptr) + { + error() << "failed to figure out type of file `" + << filename << "'" << eom; + return 6; + } + + language->get_language_options(cmdline); + language->set_message_handler(get_message_handler()); + + status() << "Parsing " << filename << eom; + + if(language->parse(infile, filename)) + { + error() << "PARSING ERROR" << eom; + return 6; + } + + language->show_parse(std::cout); + return 0; + } + + int get_goto_program_ret=get_goto_program(options); + + if(get_goto_program_ret!=-1) + return get_goto_program_ret; + + if(cmdline.isset("show-properties")) + { + show_properties(goto_model, ui_message_handler.get_ui()); + return 0; // should contemplate EX_OK from sysexits.h + } + + if(set_properties()) + return 7; // should contemplate EX_USAGE from sysexits.h + + // unwinds loops to number of enum elements + // side effect: add this as explicit unwind to unwind set + if(options.get_bool_option("java-unwind-enum-static")) + remove_static_init_loops(goto_model, options, get_message_handler()); + + // get solver + cbmc_solverst jbmc_solvers( + options, + goto_model.symbol_table, + get_message_handler()); + + jbmc_solvers.set_ui(ui_message_handler.get_ui()); + + std::unique_ptr jbmc_solver; + + try + { + jbmc_solver=jbmc_solvers.get_solver(); + } + + catch(const char *error_msg) + { + error() << error_msg << eom; + return 1; // should contemplate EX_SOFTWARE from sysexits.h + } + + prop_convt &prop_conv=jbmc_solver->prop_conv(); + + bmct bmc( + options, + goto_model.symbol_table, + get_message_handler(), + prop_conv); + + // do actual BMC + return do_bmc(bmc); +} + +bool jbmc_parse_optionst::set_properties() +{ + try + { + if(cmdline.isset("property")) + ::set_properties(goto_model, cmdline.get_values("property")); + } + + catch(const char *e) + { + error() << e << eom; + return true; + } + + catch(const std::string e) + { + error() << e << eom; + return true; + } + + catch(int) + { + return true; + } + + return false; +} + +int jbmc_parse_optionst::get_goto_program( + const optionst &options) +{ + if(cmdline.args.empty()) + { + error() << "Please provide a program to verify" << eom; + return 6; + } + + try + { + if(initialize_goto_model(goto_model, cmdline, get_message_handler())) + // Remove all binaries from the command line as they + // are already compiled + return 6; + + if(cmdline.isset("show-symbol-table")) + { + show_symbol_table(goto_model, ui_message_handler.get_ui()); + return 0; + } + + if(process_goto_program(options)) + return 6; + + // show it? + if(cmdline.isset("show-loops")) + { + show_loop_ids(ui_message_handler.get_ui(), goto_model); + return 0; + } + + // show it? + if(cmdline.isset("show-goto-functions")) + { + show_goto_functions(goto_model, ui_message_handler.get_ui()); + return 0; + } + + status() << config.object_bits_info() << eom; + } + + catch(const char *e) + { + error() << e << eom; + return 6; + } + + catch(const std::string e) + { + error() << e << eom; + return 6; + } + + catch(int) + { + return 6; + } + + catch(std::bad_alloc) + { + error() << "Out of memory" << eom; + return 6; + } + + return -1; // no error, continue +} + +bool jbmc_parse_optionst::process_goto_program( + const optionst &options) +{ + try + { + // Remove inline assembler; this needs to happen before + // adding the library. + remove_asm(goto_model); + + // add the library + link_to_library(goto_model, get_message_handler()); + + if(cmdline.isset("string-abstraction")) + string_instrumentation(goto_model, get_message_handler()); + + // remove function pointers + status() << "Removal of function pointers and virtual functions" << eom; + remove_function_pointers( + get_message_handler(), + goto_model, + cmdline.isset("pointer-check")); + // Java virtual functions -> explicit dispatch tables: + remove_virtual_functions(goto_model); + // remove catch and throw (introduces instanceof) + remove_exceptions(goto_model); + // Similar removal of RTTI inspection: + remove_instanceof(goto_model); + + // instrument library preconditions + instrument_preconditions(goto_model); + + // remove returns, gcc vectors, complex + remove_returns(goto_model); + remove_vector(goto_model); + remove_complex(goto_model); + rewrite_union(goto_model); + + // Similar removal of java nondet statements: + // TODO Should really get this from java_bytecode_language somehow, but we + // don't have an instance of that here. + object_factory_parameterst factory_params; + factory_params.max_nondet_array_length= + cmdline.isset("java-max-input-array-length") + ? std::stoul(cmdline.get_value("java-max-input-array-length")) + : MAX_NONDET_ARRAY_LENGTH_DEFAULT; + factory_params.max_nondet_string_length= + cmdline.isset("string-max-input-length") + ? std::stoul(cmdline.get_value("string-max-input-length")) + : MAX_NONDET_STRING_LENGTH; + factory_params.max_nondet_tree_depth= + cmdline.isset("java-max-input-tree-depth") + ? std::stoul(cmdline.get_value("java-max-input-tree-depth")) + : MAX_NONDET_TREE_DEPTH; + + replace_java_nondet(goto_model); + + convert_nondet( + goto_model, + get_message_handler(), + factory_params); + + // add generic checks + status() << "Generic Property Instrumentation" << eom; + goto_check(options, goto_model); + + // checks don't know about adjusted float expressions + adjust_float_expressions(goto_model); + + // ignore default/user-specified initialization + // of variables with static lifetime + if(cmdline.isset("nondet-static")) + { + status() << "Adding nondeterministic initialization " + "of static/global variables" << eom; + nondet_static(goto_model); + } + + if(cmdline.isset("string-abstraction")) + { + status() << "String Abstraction" << eom; + string_abstraction( + goto_model, + get_message_handler()); + } + + // add failed symbols + // needs to be done before pointer analysis + add_failed_symbols(goto_model.symbol_table); + + // recalculate numbers, etc. + goto_model.goto_functions.update(); + + // add loop ids + goto_model.goto_functions.compute_loop_numbers(); + + if(cmdline.isset("drop-unused-functions")) + { + // Entry point will have been set before and function pointers removed + status() << "Removing unused functions" << eom; + remove_unused_functions(goto_model, get_message_handler()); + } + + // remove skips such that trivial GOTOs are deleted and not considered + // for coverage annotation: + remove_skip(goto_model); + + // instrument cover goals + if(cmdline.isset("cover")) + { + if(instrument_cover_goals( + cmdline, + goto_model, + get_message_handler())) + return true; + } + + // label the assertions + // This must be done after adding assertions and + // before using the argument of the "property" option. + // Do not re-label after using the property slicer because + // this would cause the property identifiers to change. + label_properties(goto_model); + + // full slice? + if(cmdline.isset("full-slice")) + { + status() << "Performing a full slice" << eom; + if(cmdline.isset("property")) + property_slicer(goto_model, cmdline.get_values("property")); + else + full_slicer(goto_model); + } + + // remove any skips introduced since coverage instrumentation + remove_skip(goto_model); + goto_model.goto_functions.update(); + } + + catch(const char *e) + { + error() << e << eom; + return true; + } + + catch(const std::string e) + { + error() << e << eom; + return true; + } + + catch(int) + { + return true; + } + + catch(std::bad_alloc) + { + error() << "Out of memory" << eom; + return true; + } + + return false; +} + +/// invoke main modules +int jbmc_parse_optionst::do_bmc(bmct &bmc) +{ + bmc.set_ui(ui_message_handler.get_ui()); + + int result=6; + + // do actual BMC + switch(bmc.run(goto_model.goto_functions)) + { + case safety_checkert::resultt::SAFE: + result=0; + break; + case safety_checkert::resultt::UNSAFE: + result=10; + break; + case safety_checkert::resultt::ERROR: + result=6; + break; + } + + // let's log some more statistics + debug() << "Memory consumption:" << messaget::endl; + memory_info(debug()); + debug() << eom; + + return result; +} + +/// display command line help +void jbmc_parse_optionst::help() +{ + std::cout << + "\n" + "* * JBMC " CBMC_VERSION " - Copyright (C) 2001-2017 "; + + std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; + + std::cout << " * *\n"; + + std::cout << + "* * Daniel Kroening, Edmund Clarke * *\n" + "* * Carnegie Mellon University, Computer Science Department * *\n" + "* * kroening@kroening.com * *\n" + "\n" + "Usage: Purpose:\n" + "\n" + " jbmc [-?] [-h] [--help] show help\n" + " jbmc class name of class to be checked\n" + "\n" + "Analysis options:\n" + " --show-properties show the properties, but don't run analysis\n" // NOLINT(*) + " --symex-coverage-report f generate a Cobertura XML coverage report in f\n" // NOLINT(*) + " --property id only check one specific property\n" + " --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*) + " --trace give a counterexample trace for failed properties\n" //NOLINT(*) + "\n" + " --no-library disable built-in abstract Java library\n" + HELP_FUNCTIONS + "\n" + "Program representations:\n" + " --show-parse-tree show parse tree\n" + " --show-symbol-table show symbol table\n" + HELP_SHOW_GOTO_FUNCTIONS + " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) + "\n" + "Program instrumentation options:\n" + HELP_GOTO_CHECK + " --no-assertions ignore user assertions\n" + " --no-assumptions ignore user assumptions\n" + " --error-label label check that label is unreachable\n" + " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) + " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) + "\n" + "Java Bytecode frontend options:\n" + " --classpath dir/jar set the classpath\n" + " --main-class class-name set the name of the main class\n" + JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP + // This one is handled by jbmc_parse_options not by the Java frontend, + // hence its presence here: + " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" // NOLINT(*) + "\n" + "BMC options:\n" + " --program-only only show program expression\n" + " --show-loops show the loops in the program\n" + " --depth nr limit search depth\n" + " --unwind nr unwind nr times\n" + " --unwindset L:B,... unwind loop L with a bound of B\n" + " (use --show-loops to get the loop IDs)\n" + " --show-vcc show the verification conditions\n" + " --slice-formula remove assignments unrelated to property\n" + " --unwinding-assertions generate unwinding assertions\n" + " --partial-loops permit paths with partial loops\n" + " --no-pretty-names do not simplify identifiers\n" + " --graphml-witness filename write the witness in GraphML format to filename\n" // NOLINT(*) + "\n" + "Backend options:\n" + " --object-bits n number of bits used for object addresses\n" + " --dimacs generate CNF in DIMACS format\n" + " --beautify beautify the counterexample (greedy heuristic)\n" // NOLINT(*) + " --localize-faults localize faults (experimental)\n" + " --smt1 use default SMT1 solver (obsolete)\n" + " --smt2 use default SMT2 solver (Z3)\n" + " --boolector use Boolector\n" + " --mathsat use MathSAT\n" + " --cvc4 use CVC4\n" + " --yices use Yices\n" + " --z3 use Z3\n" + " --refine use refinement procedure (experimental)\n" + " --refine-strings use string refinement (experimental)\n" + " --string-non-empty add constraint that strings are non empty (experimental)\n" // NOLINT(*) + " --string-printable add constraint that strings are printable (experimental)\n" // NOLINT(*) + " --string-max-length add constraint on the length of strings\n" // NOLINT(*) + " --string-max-input-length add constraint on the length of input strings\n" // NOLINT(*) + " --outfile filename output formula to given file\n" + " --arrays-uf-never never turn arrays into uninterpreted functions\n" // NOLINT(*) + " --arrays-uf-always always turn arrays into uninterpreted functions\n" // NOLINT(*) + "\n" + "Other options:\n" + " --version show version and exit\n" + " --xml-ui use XML-formatted output\n" + " --json-ui use JSON-formatted output\n" + " --verbosity # verbosity level\n" + "\n"; +} diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h new file mode 100644 index 00000000000..06916c296a9 --- /dev/null +++ b/src/jbmc/jbmc_parse_options.h @@ -0,0 +1,93 @@ +/*******************************************************************\ + +Module: JBMC Command Line Option Processing + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// JBMC Command Line Option Processing + +#ifndef CPROVER_JBMC_JBMC_PARSE_OPTIONS_H +#define CPROVER_JBMC_JBMC_PARSE_OPTIONS_H + +#include +#include +#include + +#include + +#include + +class bmct; +class goto_functionst; +class optionst; + +#define JBMC_OPTIONS \ + "(program-only)(preprocess)(slice-by-trace):" \ + OPT_FUNCTIONS \ + "(no-simplify)(unwind):(unwindset):(slice-formula)(full-slice)" \ + "(debug-level):(no-propagation)(no-simplify-if)" \ + "(document-subgoals)(outfile):" \ + "(object-bits):" \ + "(classpath):(cp):(main-class):" \ + "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \ + OPT_GOTO_CHECK \ + "(no-assertions)(no-assumptions)" \ + "(no-built-in-assertions)" \ + "(xml-ui)(json-ui)" \ + "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ + "(no-sat-preprocessor)" \ + "(no-pretty-names)(beautify)" \ + "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\ + "(refine-strings)" \ + "(string-non-empty)" \ + "(string-printable)" \ + "(string-max-length):" \ + "(string-max-input-length):" \ + "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ + "(show-goto-functions)(show-loops)" \ + "(show-symbol-table)(show-parse-tree)(show-vcc)" \ + "(show-properties)" \ + "(drop-unused-functions)" \ + "(property):(stop-on-fail)(trace)" \ + "(verbosity):(no-library)" \ + "(version)" \ + "(cover):(symex-coverage-report):" \ + "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \ + "(ppc-macos)" \ + "(arrays-uf-always)(arrays-uf-never)" \ + "(string-abstraction)(no-arch)(arch):" \ + "(graphml-witness):" \ + JAVA_BYTECODE_LANGUAGE_OPTIONS \ + "(java-unwind-enum-static)" \ + "(localize-faults)(localize-faults-method):" + +class jbmc_parse_optionst: + public parse_options_baset, + public messaget +{ +public: + virtual int doit() override; + virtual void help() override; + + jbmc_parse_optionst(int argc, const char **argv); + jbmc_parse_optionst( + int argc, + const char **argv, + const std::string &extra_options); + +protected: + goto_modelt goto_model; + ui_message_handlert ui_message_handler; + + void eval_verbosity(); + void get_command_line_options(optionst &); + int get_goto_program(const optionst &); + bool process_goto_program(const optionst &); + bool set_properties(); + int do_bmc(bmct &); +}; + +#endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 9e9fc93ad09..f2bc127faf8 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -105,6 +105,6 @@ elseif("${sat_impl}" STREQUAL "glucose") target_link_libraries(solvers glucose-condensed) endif() -target_link_libraries(solvers util) +target_link_libraries(solvers java_bytecode util) generic_includes(solvers)