diff --git a/jbmc/CMakeLists.txt b/jbmc/CMakeLists.txt index 561f89a5799..e5e05070c50 100644 --- a/jbmc/CMakeLists.txt +++ b/jbmc/CMakeLists.txt @@ -56,3 +56,5 @@ add_custom_command(OUTPUT ${java_regression_compiled_sources} add_custom_target(java-regression ALL DEPENDS ${java_regression_compiled_sources} ) + +add_dependencies(java-regression java-models-library) diff --git a/jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.class deleted file mode 100644 index 3ac62d1ede5..00000000000 Binary files a/jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArithmeticException2/pom.xml b/jbmc/regression/jbmc/ArithmeticException2/pom.xml new file mode 100644 index 00000000000..65a12534b47 --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException2/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException2/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException2/test.desc b/jbmc/regression/jbmc/ArithmeticException2/test.desc index 1341d843ccb..2142ad4c6f4 100644 --- a/jbmc/regression/jbmc/ArithmeticException2/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException2/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.class deleted file mode 100644 index 21c451e02f3..00000000000 Binary files a/jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArithmeticException3/pom.xml b/jbmc/regression/jbmc/ArithmeticException3/pom.xml new file mode 100644 index 00000000000..69c6eea5eaf --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException3/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException3 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException3/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException3/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException3/test.desc b/jbmc/regression/jbmc/ArithmeticException3/test.desc index 0577e08a51b..a07a8ddb801 100644 --- a/jbmc/regression/jbmc/ArithmeticException3/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException3/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.class deleted file mode 100644 index a4723d1d652..00000000000 Binary files a/jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArithmeticException4/pom.xml b/jbmc/regression/jbmc/ArithmeticException4/pom.xml new file mode 100644 index 00000000000..4da8cbe1011 --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException4/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException4 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException4/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException4/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException4/test.desc b/jbmc/regression/jbmc/ArithmeticException4/test.desc index 1341d843ccb..2142ad4c6f4 100644 --- a/jbmc/regression/jbmc/ArithmeticException4/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException4/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.class deleted file mode 100644 index 813391d04af..00000000000 Binary files a/jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArithmeticException5/pom.xml b/jbmc/regression/jbmc/ArithmeticException5/pom.xml new file mode 100644 index 00000000000..48d152a576e --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException5/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException5 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException5/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException5/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException5/test.desc b/jbmc/regression/jbmc/ArithmeticException5/test.desc index 3df41a2390a..a5d9fe7cac6 100644 --- a/jbmc/regression/jbmc/ArithmeticException5/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException5/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.class deleted file mode 100644 index fdcb29ad252..00000000000 Binary files a/jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArithmeticException6/pom.xml b/jbmc/regression/jbmc/ArithmeticException6/pom.xml new file mode 100644 index 00000000000..f22db55b6c9 --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException6/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException6 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException6/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException6/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException6/test.desc b/jbmc/regression/jbmc/ArithmeticException6/test.desc index 438f1f346da..6782f32d8d9 100644 --- a/jbmc/regression/jbmc/ArithmeticException6/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException6/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions --function ArithmeticExceptionTest.main +--throw-runtime-exceptions --function ArithmeticExceptionTest.main -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.class deleted file mode 100644 index 621ed3729b0..00000000000 Binary files a/jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.class b/jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.class deleted file mode 100644 index a85ed965b94..00000000000 Binary files a/jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.class b/jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.class deleted file mode 100644 index 2f0ac26544c..00000000000 Binary files a/jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArithmeticException7/pom.xml b/jbmc/regression/jbmc/ArithmeticException7/pom.xml new file mode 100644 index 00000000000..6b3c9765c17 --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException7/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException7 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException7/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException7/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.java b/jbmc/regression/jbmc/ArithmeticException7/src/main/java/java/lang/ArithmeticException.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.java rename to jbmc/regression/jbmc/ArithmeticException7/src/main/java/java/lang/ArithmeticException.java diff --git a/jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.java b/jbmc/regression/jbmc/ArithmeticException7/src/main/java/java/lang/RuntimeException.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.java rename to jbmc/regression/jbmc/ArithmeticException7/src/main/java/java/lang/RuntimeException.java diff --git a/jbmc/regression/jbmc/ArithmeticException7/test.desc b/jbmc/regression/jbmc/ArithmeticException7/test.desc index 0577e08a51b..a07a8ddb801 100644 --- a/jbmc/regression/jbmc/ArithmeticException7/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException7/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class deleted file mode 100644 index ca15fe999ec..00000000000 Binary files a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/pom.xml b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/pom.xml new file mode 100644 index 00000000000..e9a6514c61f --- /dev/null +++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArrayIndexOutOfBoundsException1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc index c6cca9da7d7..e41f46b73a0 100644 --- a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc +++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc @@ -1,6 +1,6 @@ CORE ArrayIndexOutOfBoundsExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class deleted file mode 100644 index 3de63e25a0f..00000000000 Binary files a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/pom.xml b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/pom.xml new file mode 100644 index 00000000000..084b1c6ee4f --- /dev/null +++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArrayIndexOutOfBoundsException2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc index c6cca9da7d7..e41f46b73a0 100644 --- a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc +++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc @@ -1,6 +1,6 @@ CORE ArrayIndexOutOfBoundsExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class deleted file mode 100644 index b500a095ac4..00000000000 Binary files a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class deleted file mode 100644 index 90434074df6..00000000000 Binary files a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class deleted file mode 100644 index 07ac2ac49f6..00000000000 Binary files a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class deleted file mode 100644 index 2f0ac26544c..00000000000 Binary files a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml new file mode 100644 index 00000000000..4b7162373f1 --- /dev/null +++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArrayIndexOutOfBoundsException3 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/ArrayIndexOutOfBoundsException.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/ArrayIndexOutOfBoundsException.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/IndexOutOfBoundsException.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/IndexOutOfBoundsException.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.java b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/RuntimeException.java similarity index 100% rename from jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.java rename to jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/RuntimeException.java diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc index c6cca9da7d7..e41f46b73a0 100644 --- a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc +++ b/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc @@ -1,6 +1,6 @@ CORE ArrayIndexOutOfBoundsExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/aastore_aaload1/A.class b/jbmc/regression/jbmc/aastore_aaload1/A.class deleted file mode 100644 index 058d5ef9984..00000000000 Binary files a/jbmc/regression/jbmc/aastore_aaload1/A.class and /dev/null differ diff --git a/jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.class b/jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.class deleted file mode 100644 index 748e45b414b..00000000000 Binary files a/jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/aastore_aaload1/pom.xml b/jbmc/regression/jbmc/aastore_aaload1/pom.xml new file mode 100644 index 00000000000..ec4f700c59d --- /dev/null +++ b/jbmc/regression/jbmc/aastore_aaload1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.aastore_aaload1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.java b/jbmc/regression/jbmc/aastore_aaload1/src/main/java/aastore_aaload1.java similarity index 100% rename from jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.java rename to jbmc/regression/jbmc/aastore_aaload1/src/main/java/aastore_aaload1.java diff --git a/jbmc/regression/jbmc/aastore_aaload1/test.desc b/jbmc/regression/jbmc/aastore_aaload1/test.desc index a5c1145917e..f5ce48e69f5 100644 --- a/jbmc/regression/jbmc/aastore_aaload1/test.desc +++ b/jbmc/regression/jbmc/aastore_aaload1/test.desc @@ -1,6 +1,6 @@ CORE aastore_aaload1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/address_space_size_limit1/Test.class b/jbmc/regression/jbmc/address_space_size_limit1/Test.class deleted file mode 100644 index 5f81fc826ff..00000000000 Binary files a/jbmc/regression/jbmc/address_space_size_limit1/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/address_space_size_limit1/pom.xml b/jbmc/regression/jbmc/address_space_size_limit1/pom.xml new file mode 100644 index 00000000000..0ad08f62a67 --- /dev/null +++ b/jbmc/regression/jbmc/address_space_size_limit1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.address_space_size_limit1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/address_space_size_limit1/Test.java b/jbmc/regression/jbmc/address_space_size_limit1/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/address_space_size_limit1/Test.java rename to jbmc/regression/jbmc/address_space_size_limit1/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/address_space_size_limit1/test.desc b/jbmc/regression/jbmc/address_space_size_limit1/test.desc index a9bb6c1ed0a..88299880103 100644 --- a/jbmc/regression/jbmc/address_space_size_limit1/test.desc +++ b/jbmc/regression/jbmc/address_space_size_limit1/test.desc @@ -1,6 +1,6 @@ CORE Test ---object-bits 4 +--object-bits 4 --cp target/classes too many addressed objects ^EXIT=6$ ^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/address_space_size_limit2/Test.class b/jbmc/regression/jbmc/address_space_size_limit2/Test.class deleted file mode 100644 index 5f81fc826ff..00000000000 Binary files a/jbmc/regression/jbmc/address_space_size_limit2/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/address_space_size_limit2/pom.xml b/jbmc/regression/jbmc/address_space_size_limit2/pom.xml new file mode 100644 index 00000000000..41309e373ea --- /dev/null +++ b/jbmc/regression/jbmc/address_space_size_limit2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.address_space_size_limit2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/address_space_size_limit2/Test.java b/jbmc/regression/jbmc/address_space_size_limit2/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/address_space_size_limit2/Test.java rename to jbmc/regression/jbmc/address_space_size_limit2/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/address_space_size_limit2/test.desc b/jbmc/regression/jbmc/address_space_size_limit2/test.desc index 87f368c70f9..600e3c82179 100644 --- a/jbmc/regression/jbmc/address_space_size_limit2/test.desc +++ b/jbmc/regression/jbmc/address_space_size_limit2/test.desc @@ -1,6 +1,6 @@ CORE Test ---object-bits 8 +--object-bits 8 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/annotations1/ClassAnnotation.class b/jbmc/regression/jbmc/annotations1/ClassAnnotation.class deleted file mode 100644 index c5dbfca92fd..00000000000 Binary files a/jbmc/regression/jbmc/annotations1/ClassAnnotation.class and /dev/null differ diff --git a/jbmc/regression/jbmc/annotations1/FieldAnnotation.class b/jbmc/regression/jbmc/annotations1/FieldAnnotation.class deleted file mode 100644 index 423bddd6062..00000000000 Binary files a/jbmc/regression/jbmc/annotations1/FieldAnnotation.class and /dev/null differ diff --git a/jbmc/regression/jbmc/annotations1/MethodAnnotation.class b/jbmc/regression/jbmc/annotations1/MethodAnnotation.class deleted file mode 100644 index 471b9576871..00000000000 Binary files a/jbmc/regression/jbmc/annotations1/MethodAnnotation.class and /dev/null differ diff --git a/jbmc/regression/jbmc/annotations1/annotations.class b/jbmc/regression/jbmc/annotations1/annotations.class deleted file mode 100644 index 6c6cb308255..00000000000 Binary files a/jbmc/regression/jbmc/annotations1/annotations.class and /dev/null differ diff --git a/jbmc/regression/jbmc/annotations1/pom.xml b/jbmc/regression/jbmc/annotations1/pom.xml new file mode 100644 index 00000000000..edffa69b55e --- /dev/null +++ b/jbmc/regression/jbmc/annotations1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.annotations1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc index a1f601974e1..879ce4fb9ff 100644 --- a/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc +++ b/jbmc/regression/jbmc/annotations1/show_annotation_symbol.desc @@ -1,6 +1,6 @@ CORE annotations ---no-lazy-methods --show-symbol-table --function annotations.main +--no-lazy-methods --show-symbol-table --function annotations.main -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^Type\.\.\.\.\.\.\.\.: @java::ClassAnnotation struct annotations diff --git a/jbmc/regression/jbmc/annotations1/annotations.java b/jbmc/regression/jbmc/annotations1/src/main/java/annotations.java similarity index 100% rename from jbmc/regression/jbmc/annotations1/annotations.java rename to jbmc/regression/jbmc/annotations1/src/main/java/annotations.java diff --git a/jbmc/regression/jbmc/annotations2/FieldAnnotation.class b/jbmc/regression/jbmc/annotations2/FieldAnnotation.class deleted file mode 100644 index 7be3db544bd..00000000000 Binary files a/jbmc/regression/jbmc/annotations2/FieldAnnotation.class and /dev/null differ diff --git a/jbmc/regression/jbmc/annotations2/Test.class b/jbmc/regression/jbmc/annotations2/Test.class deleted file mode 100644 index c0260839fe3..00000000000 Binary files a/jbmc/regression/jbmc/annotations2/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/annotations2/pom.xml b/jbmc/regression/jbmc/annotations2/pom.xml new file mode 100644 index 00000000000..ff39b676792 --- /dev/null +++ b/jbmc/regression/jbmc/annotations2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.annotations2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/annotations2/Test.java b/jbmc/regression/jbmc/annotations2/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/annotations2/Test.java rename to jbmc/regression/jbmc/annotations2/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/annotations2/test.desc b/jbmc/regression/jbmc/annotations2/test.desc index 28b08e36284..1f87fc5bbf8 100644 --- a/jbmc/regression/jbmc/annotations2/test.desc +++ b/jbmc/regression/jbmc/annotations2/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.check +--function Test.check -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file Test.java line 10 .* SUCCESS diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.class deleted file mode 100644 index 1811bee9941..00000000000 Binary files a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/pom.xml b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/pom.xml new file mode 100644 index 00000000000..37b3521a42e --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array-cell-sensitivity-negative-size + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.java rename to jbmc/regression/jbmc/array-cell-sensitivity-negative-size/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc index 605cd7040d4..2e1d8af1f57 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.check +--function Test.check -cp target/classes line 5 Array size should be >= 0: FAILURE ^EXIT=10$ ^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.class deleted file mode 100644 index a41151d6a03..00000000000 Binary files a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Util.class b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Util.class deleted file mode 100644 index 4eeec110121..00000000000 Binary files a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Util.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/pom.xml b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/pom.xml new file mode 100644 index 00000000000..a39539c7970 --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array-cell-sensitivity-static-fields + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.java rename to jbmc/regression/jbmc/array-cell-sensitivity-static-fields/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc index 6cb0a122f1e..51515b0e110 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure Test ---function Test.charArrayRef --property 'java::Test.charArrayRef:()[C.assertion.2' --static-values static-values.json +--function Test.charArrayRef --property 'java::Test.charArrayRef:()[C.assertion.2' --static-values static-values.json -cp target/classes Generated 0 VCC[(]s[)], 0 remaining after simplification assertion at file Test.java line 31 .*: SUCCESS ^EXIT=0$ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc index 4598fef0877..2dacde1593d 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure Test ---function Test.charArrayRef --property 'java::Test.charArrayRef:()[C.assertion.1' +--function Test.charArrayRef --property 'java::Test.charArrayRef:()[C.assertion.1' -cp target/classes Generated 0 VCC[(]s[)], 0 remaining after simplification assertion at file Test.java line 29 .*: SUCCESS ^EXIT=0$ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc index a31e295710f..cf6668f17fd 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure Test ---function Test.charArray --property 'java::Test.charArray:()[C.assertion.2' --static-values static-values.json +--function Test.charArray --property 'java::Test.charArray:()[C.assertion.2' --static-values static-values.json -cp target/classes Generated 0 VCC[(]s[)], 0 remaining after simplification assertion at file Test.java line 21 .*: SUCCESS ^EXIT=0$ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc index e70aaf0604e..7a28f184269 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure Test ---function Test.charArray --property 'java::Test.charArray:()[C.assertion.1' +--function Test.charArray --property 'java::Test.charArray:()[C.assertion.1' -cp target/classes Generated 0 VCC[(]s[)], 0 remaining after simplification assertion at file Test.java line 20 .*: SUCCESS ^EXIT=0$ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity1/Test.class deleted file mode 100644 index 57c9912d571..00000000000 Binary files a/jbmc/regression/jbmc/array-cell-sensitivity1/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/pom.xml b/jbmc/regression/jbmc/array-cell-sensitivity1/pom.xml new file mode 100644 index 00000000000..8148be54c60 --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array-cell-sensitivity1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity1/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/array-cell-sensitivity1/Test.java rename to jbmc/regression/jbmc/array-cell-sensitivity1/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc index 34336440f7a..ea0b6b1ce36 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main --show-vcc --max-field-sensitivity-array-size 10 +--function Test.main --show-vcc --max-field-sensitivity-array-size 10 -cp target/classes symex_dynamic::dynamic_array#2\[\[0\]\] = symex_dynamic::dynamic_array#2\[\[1\]\] = symex_dynamic::dynamic_array#2\[\[2\]\] = diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc index db0ec927037..dfb2ea1b7e0 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main --show-vcc --max-field-sensitivity-array-size 9 +--function Test.main --show-vcc --max-field-sensitivity-array-size 9 -cp target/classes ^EXIT=0$ ^SIGNAL=0$ symex_dynamic::dynamic_array#[0-9]\[1\] diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc index 2fbb2dd7dc3..6cc50795e6c 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main --show-vcc --no-array-field-sensitivity +--function Test.main --show-vcc --no-array-field-sensitivity -cp target/classes ^EXIT=0$ ^SIGNAL=0$ symex_dynamic::dynamic_array#[0-9]\[1\] diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc index 5061f9230e4..165a8c26b67 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main --show-vcc +--function Test.main --show-vcc -cp target/classes symex_dynamic::dynamic_array#2\[\[0\]\] = symex_dynamic::dynamic_array#2\[\[1\]\] = symex_dynamic::dynamic_array#2\[\[2\]\] = diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity2/Test.class deleted file mode 100644 index ae3d24793dc..00000000000 Binary files a/jbmc/regression/jbmc/array-cell-sensitivity2/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/pom.xml b/jbmc/regression/jbmc/array-cell-sensitivity2/pom.xml new file mode 100644 index 00000000000..10c5aab568d --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array-cell-sensitivity2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity2/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/array-cell-sensitivity2/Test.java rename to jbmc/regression/jbmc/array-cell-sensitivity2/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc b/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc index ce987c5326b..57597c18830 100644 --- a/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc +++ b/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main --show-vcc +--function Test.main --show-vcc -cp target/classes symex_dynamic::dynamic_object\$3#3\.\.data = symex_dynamic::dynamic_object\$1#3\.\.data = ^EXIT=0$ diff --git a/jbmc/regression/jbmc/array-clone/ArrayClone.class b/jbmc/regression/jbmc/array-clone/ArrayClone.class deleted file mode 100644 index 2e985bf8761..00000000000 Binary files a/jbmc/regression/jbmc/array-clone/ArrayClone.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array-clone/pom.xml b/jbmc/regression/jbmc/array-clone/pom.xml new file mode 100644 index 00000000000..66609764d94 --- /dev/null +++ b/jbmc/regression/jbmc/array-clone/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array-clone + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array-clone/ArrayClone.java b/jbmc/regression/jbmc/array-clone/src/main/java/ArrayClone.java similarity index 100% rename from jbmc/regression/jbmc/array-clone/ArrayClone.java rename to jbmc/regression/jbmc/array-clone/src/main/java/ArrayClone.java diff --git a/jbmc/regression/jbmc/array-clone/testBoolean.desc b/jbmc/regression/jbmc/array-clone/testBoolean.desc index 14819080eb0..724c42bf5d1 100644 --- a/jbmc/regression/jbmc/array-clone/testBoolean.desc +++ b/jbmc/regression/jbmc/array-clone/testBoolean.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneBooleanArray +--function ArrayClone.cloneBooleanArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testByte.desc b/jbmc/regression/jbmc/array-clone/testByte.desc index 2e0d2012dd4..0df7b22c221 100644 --- a/jbmc/regression/jbmc/array-clone/testByte.desc +++ b/jbmc/regression/jbmc/array-clone/testByte.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneByteArray +--function ArrayClone.cloneByteArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testDouble.desc b/jbmc/regression/jbmc/array-clone/testDouble.desc index 58d52f46a4f..3a49658300f 100644 --- a/jbmc/regression/jbmc/array-clone/testDouble.desc +++ b/jbmc/regression/jbmc/array-clone/testDouble.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneDoubleArray +--function ArrayClone.cloneDoubleArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testFloat.desc b/jbmc/regression/jbmc/array-clone/testFloat.desc index 73117b32e43..23188c99cb6 100644 --- a/jbmc/regression/jbmc/array-clone/testFloat.desc +++ b/jbmc/regression/jbmc/array-clone/testFloat.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneFloatArray +--function ArrayClone.cloneFloatArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testInt.desc b/jbmc/regression/jbmc/array-clone/testInt.desc index ea0b0552131..c091b6f5778 100644 --- a/jbmc/regression/jbmc/array-clone/testInt.desc +++ b/jbmc/regression/jbmc/array-clone/testInt.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneIntArray +--function ArrayClone.cloneIntArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testLong.desc b/jbmc/regression/jbmc/array-clone/testLong.desc index e1904c51acf..7f242d279c6 100644 --- a/jbmc/regression/jbmc/array-clone/testLong.desc +++ b/jbmc/regression/jbmc/array-clone/testLong.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneLongArray +--function ArrayClone.cloneLongArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testObject.desc b/jbmc/regression/jbmc/array-clone/testObject.desc index ae7d25c7587..d0dcc481b5b 100644 --- a/jbmc/regression/jbmc/array-clone/testObject.desc +++ b/jbmc/regression/jbmc/array-clone/testObject.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneObjectArray +--function ArrayClone.cloneObjectArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testReference.desc b/jbmc/regression/jbmc/array-clone/testReference.desc index bd1ed3407d3..0d258793c34 100644 --- a/jbmc/regression/jbmc/array-clone/testReference.desc +++ b/jbmc/regression/jbmc/array-clone/testReference.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneReferenceArray +--function ArrayClone.cloneReferenceArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array-clone/testShort.desc b/jbmc/regression/jbmc/array-clone/testShort.desc index 18341d3f9b3..5d7e0d7e937 100644 --- a/jbmc/regression/jbmc/array-clone/testShort.desc +++ b/jbmc/regression/jbmc/array-clone/testShort.desc @@ -1,6 +1,6 @@ CORE ArrayClone ---function ArrayClone.cloneShortArray +--function ArrayClone.cloneShortArray -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array1/array1.class b/jbmc/regression/jbmc/array1/array1.class deleted file mode 100644 index 6cc7d0164b6..00000000000 Binary files a/jbmc/regression/jbmc/array1/array1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array1/pom.xml b/jbmc/regression/jbmc/array1/pom.xml new file mode 100644 index 00000000000..f53f1d4c392 --- /dev/null +++ b/jbmc/regression/jbmc/array1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array1/array1.java b/jbmc/regression/jbmc/array1/src/main/java/array1.java similarity index 100% rename from jbmc/regression/jbmc/array1/array1.java rename to jbmc/regression/jbmc/array1/src/main/java/array1.java diff --git a/jbmc/regression/jbmc/array1/what_not.java b/jbmc/regression/jbmc/array1/src/main/java/what_not.java similarity index 100% rename from jbmc/regression/jbmc/array1/what_not.java rename to jbmc/regression/jbmc/array1/src/main/java/what_not.java diff --git a/jbmc/regression/jbmc/array1/test.desc b/jbmc/regression/jbmc/array1/test.desc index da6eeb929fe..315e1390053 100644 --- a/jbmc/regression/jbmc/array1/test.desc +++ b/jbmc/regression/jbmc/array1/test.desc @@ -1,6 +1,6 @@ CORE array1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/array1/what_not.class b/jbmc/regression/jbmc/array1/what_not.class deleted file mode 100644 index 752b97aa8b3..00000000000 Binary files a/jbmc/regression/jbmc/array1/what_not.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array2/pom.xml b/jbmc/regression/jbmc/array2/pom.xml new file mode 100644 index 00000000000..611d48a56f7 --- /dev/null +++ b/jbmc/regression/jbmc/array2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array2/test.java b/jbmc/regression/jbmc/array2/src/main/java/test.java similarity index 100% rename from jbmc/regression/jbmc/array2/test.java rename to jbmc/regression/jbmc/array2/src/main/java/test.java diff --git a/jbmc/regression/jbmc/array2/test.class b/jbmc/regression/jbmc/array2/test.class deleted file mode 100644 index 10fc89c0a68..00000000000 Binary files a/jbmc/regression/jbmc/array2/test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array2/test.desc b/jbmc/regression/jbmc/array2/test.desc index 452845047bb..2b2bb8c0ee6 100644 --- a/jbmc/regression/jbmc/array2/test.desc +++ b/jbmc/regression/jbmc/array2/test.desc @@ -1,6 +1,6 @@ CORE test ---function test.f +--function test.f -cp target/classes ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class deleted file mode 100644 index 14f1d91ebe7..00000000000 Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class deleted file mode 100644 index ba36f3ebae8..00000000000 Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class deleted file mode 100644 index a2ca10913d1..00000000000 Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.class deleted file mode 100644 index 38ea3340b0c..00000000000 Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.class deleted file mode 100644 index f55c4cdf726..00000000000 Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class deleted file mode 100644 index 1287e3d6ba6..00000000000 Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.class b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.class deleted file mode 100644 index e3a1a32b818..00000000000 Binary files a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.class and /dev/null differ diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/pom.xml b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/pom.xml new file mode 100644 index 00000000000..425ace656cc --- /dev/null +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.array_nonconstsize_nonconstaccess + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/A.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/A.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/A.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/FloatMultidim1.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim1.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/FloatMultidim1.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/FloatMultidim2.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/FloatMultidim2.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/FloatMultidim2.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidim1.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim1.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidim1.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidim2.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidim2.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidim2.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidimConstsize.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefMultidimConstsize.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefSingledim.java similarity index 100% rename from jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/RefSingledim.java rename to jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/src/main/java/RefSingledim.java diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc index 47ea2e8dc8e..05a7550ab70 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc @@ -1,6 +1,6 @@ CORE FloatMultidim1 ---function FloatMultidim1.f --unwind 3 +--function FloatMultidim1.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file FloatMultidim1.java line 14 .*: FAILURE diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc index 3fa0879cae4..fae3a56bf8c 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc @@ -1,6 +1,6 @@ CORE FloatMultidim2 ---function FloatMultidim2.f --unwind 3 +--function FloatMultidim2.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file FloatMultidim2.java line 14 .*: FAILURE diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc index 1c4932e2ea8..4df4bd346fa 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc @@ -1,6 +1,6 @@ CORE RefMultidim1 ---function RefMultidim1.f --unwind 3 +--function RefMultidim1.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file RefMultidim1.java line 15 .*: FAILURE diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc index da2111478eb..04c798bab59 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc @@ -1,6 +1,6 @@ CORE RefMultidim2 ---function RefMultidim2.f --unwind 3 +--function RefMultidim2.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file RefMultidim2.java line 15 .*: FAILURE diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc index fc471ccf70c..0339e784649 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc @@ -1,6 +1,6 @@ CORE RefMultidimConstsize ---function RefMultidimConstsize.f --unwind 3 +--function RefMultidimConstsize.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file RefMultidimConstsize.java line 7 .*: FAILURE diff --git a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc index 023b53a65ca..bb308b4445f 100644 --- a/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc +++ b/jbmc/regression/jbmc/array_nonconstsize_nonconstaccess/test_ref_singledim.desc @@ -1,6 +1,6 @@ CORE RefSingledim ---function RefSingledim.f --unwind 3 +--function RefSingledim.f --unwind 3 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ assertion at file RefSingledim.java line 15 .*: FAILURE diff --git a/jbmc/regression/jbmc/arraylength1/arraylength1.class b/jbmc/regression/jbmc/arraylength1/arraylength1.class deleted file mode 100644 index 5bf22d010d3..00000000000 Binary files a/jbmc/regression/jbmc/arraylength1/arraylength1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/arraylength1/pom.xml b/jbmc/regression/jbmc/arraylength1/pom.xml new file mode 100644 index 00000000000..2888b268307 --- /dev/null +++ b/jbmc/regression/jbmc/arraylength1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.arraylength1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/arraylength1/arraylength1.java b/jbmc/regression/jbmc/arraylength1/src/main/java/arraylength1.java similarity index 100% rename from jbmc/regression/jbmc/arraylength1/arraylength1.java rename to jbmc/regression/jbmc/arraylength1/src/main/java/arraylength1.java diff --git a/jbmc/regression/jbmc/arraylength1/test.desc b/jbmc/regression/jbmc/arraylength1/test.desc index 4d7c9a21f30..7d896f47bc4 100644 --- a/jbmc/regression/jbmc/arraylength1/test.desc +++ b/jbmc/regression/jbmc/arraylength1/test.desc @@ -1,6 +1,6 @@ CORE arraylength1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/arrayread1/arrayread1.class b/jbmc/regression/jbmc/arrayread1/arrayread1.class deleted file mode 100644 index 66779a1478b..00000000000 Binary files a/jbmc/regression/jbmc/arrayread1/arrayread1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/arrayread1/pom.xml b/jbmc/regression/jbmc/arrayread1/pom.xml new file mode 100644 index 00000000000..49a97ed7dfa --- /dev/null +++ b/jbmc/regression/jbmc/arrayread1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.arrayread1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/arrayread1/arrayread1.java b/jbmc/regression/jbmc/arrayread1/src/main/java/arrayread1.java similarity index 100% rename from jbmc/regression/jbmc/arrayread1/arrayread1.java rename to jbmc/regression/jbmc/arrayread1/src/main/java/arrayread1.java diff --git a/jbmc/regression/jbmc/arrayread1/test.desc b/jbmc/regression/jbmc/arrayread1/test.desc index 147a0556846..bb36a860d0a 100644 --- a/jbmc/regression/jbmc/arrayread1/test.desc +++ b/jbmc/regression/jbmc/arrayread1/test.desc @@ -1,6 +1,6 @@ CORE arrayread1 ---unwind 3 --no-propagation --function arrayread1.main +--unwind 3 --no-propagation --function arrayread1.main -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class deleted file mode 100644 index 5578fa11a8f..00000000000 Binary files a/jbmc/regression/jbmc/assert-no-exceptions-thrown/MyException.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class deleted file mode 100644 index 9b30d4d418e..00000000000 Binary files a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class b/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class deleted file mode 100644 index ed6f21fd4e3..00000000000 Binary files a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/pom.xml b/jbmc/regression/jbmc/assert-no-exceptions-thrown/pom.xml new file mode 100644 index 00000000000..ac82dea6dcd --- /dev/null +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert-no-exceptions-thrown + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java b/jbmc/regression/jbmc/assert-no-exceptions-thrown/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/assert-no-exceptions-thrown/Test.java rename to jbmc/regression/jbmc/assert-no-exceptions-thrown/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.java b/jbmc/regression/jbmc/assert-no-exceptions-thrown/src/main/java/Thrower.java similarity index 100% rename from jbmc/regression/jbmc/assert-no-exceptions-thrown/Thrower.java rename to jbmc/regression/jbmc/assert-no-exceptions-thrown/src/main/java/Thrower.java diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc index bae55e9bae2..322add66010 100644 --- a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-thrower.desc @@ -1,6 +1,6 @@ CORE Thrower ---function Thrower.test --assert-no-exceptions-thrown --throw-runtime-exceptions +--function Thrower.test --assert-no-exceptions-thrown --throw-runtime-exceptions -cp target/classes line 39 assertion at file Thrower.java line 39 .*: FAILURE line 42 assertion at file Thrower.java line 42 .*: FAILURE line 45 assertion at file Thrower.java line 45 .*: FAILURE diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc index 55fc3ff7220..a62f286ec54 100644 --- a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test-with-throw.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.check +--function Test.check -cp target/classes line 22 assertion at file Test.java line 22 .*: FAILURE line 24 assertion at file Test.java line 24 .*: FAILURE line 26 assertion at file Test.java line 26 .*: FAILURE diff --git a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc index e1536ea9097..c893a47825f 100644 --- a/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc +++ b/jbmc/regression/jbmc/assert-no-exceptions-thrown/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.check --assert-no-exceptions-thrown +--function Test.check --assert-no-exceptions-thrown -cp target/classes line 6 assertion at file Test.java line 6 .*: FAILURE line 8 assertion at file Test.java line 8 .*: FAILURE line 10 assertion at file Test.java line 10 .*: FAILURE diff --git a/jbmc/regression/jbmc/assert1/assert1.class b/jbmc/regression/jbmc/assert1/assert1.class deleted file mode 100644 index eb6fad5bf34..00000000000 Binary files a/jbmc/regression/jbmc/assert1/assert1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assert1/pom.xml b/jbmc/regression/jbmc/assert1/pom.xml new file mode 100644 index 00000000000..65489ced2c9 --- /dev/null +++ b/jbmc/regression/jbmc/assert1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert1/assert1.java b/jbmc/regression/jbmc/assert1/src/main/java/assert1.java similarity index 100% rename from jbmc/regression/jbmc/assert1/assert1.java rename to jbmc/regression/jbmc/assert1/src/main/java/assert1.java diff --git a/jbmc/regression/jbmc/assert1/test.desc b/jbmc/regression/jbmc/assert1/test.desc index 45ce9e12416..4be9690f6e5 100644 --- a/jbmc/regression/jbmc/assert1/test.desc +++ b/jbmc/regression/jbmc/assert1/test.desc @@ -1,6 +1,6 @@ CORE assert1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/assert2/assert2.class b/jbmc/regression/jbmc/assert2/assert2.class deleted file mode 100644 index 80fbe0c0be1..00000000000 Binary files a/jbmc/regression/jbmc/assert2/assert2.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assert2/pom.xml b/jbmc/regression/jbmc/assert2/pom.xml new file mode 100644 index 00000000000..329a0df9730 --- /dev/null +++ b/jbmc/regression/jbmc/assert2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert2/assert2.java b/jbmc/regression/jbmc/assert2/src/main/java/assert2.java similarity index 100% rename from jbmc/regression/jbmc/assert2/assert2.java rename to jbmc/regression/jbmc/assert2/src/main/java/assert2.java diff --git a/jbmc/regression/jbmc/assert2/test.desc b/jbmc/regression/jbmc/assert2/test.desc index 9a000461b72..a3981bdefdf 100644 --- a/jbmc/regression/jbmc/assert2/test.desc +++ b/jbmc/regression/jbmc/assert2/test.desc @@ -1,6 +1,6 @@ CORE assert2 - +-cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assert3/assert3.class b/jbmc/regression/jbmc/assert3/assert3.class deleted file mode 100644 index d3f15d76521..00000000000 Binary files a/jbmc/regression/jbmc/assert3/assert3.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assert3/pom.xml b/jbmc/regression/jbmc/assert3/pom.xml new file mode 100644 index 00000000000..35755aae8e2 --- /dev/null +++ b/jbmc/regression/jbmc/assert3/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert3 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert3/assert3.java b/jbmc/regression/jbmc/assert3/src/main/java/assert3.java similarity index 100% rename from jbmc/regression/jbmc/assert3/assert3.java rename to jbmc/regression/jbmc/assert3/src/main/java/assert3.java diff --git a/jbmc/regression/jbmc/assert3/test.desc b/jbmc/regression/jbmc/assert3/test.desc index 19d5157d04b..16a01c15b58 100644 --- a/jbmc/regression/jbmc/assert3/test.desc +++ b/jbmc/regression/jbmc/assert3/test.desc @@ -1,6 +1,6 @@ CORE assert3 - +-cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc b/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc index 8e320065b11..2f106df135e 100644 --- a/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc +++ b/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc @@ -1,6 +1,6 @@ CORE assert3 ---throw-assertion-error --disable-uncaught-exception-check +--throw-assertion-error --disable-uncaught-exception-check -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/assert4/assert4.class b/jbmc/regression/jbmc/assert4/assert4.class deleted file mode 100644 index cfefa40fc19..00000000000 Binary files a/jbmc/regression/jbmc/assert4/assert4.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assert4/pom.xml b/jbmc/regression/jbmc/assert4/pom.xml new file mode 100644 index 00000000000..1df6fd6987a --- /dev/null +++ b/jbmc/regression/jbmc/assert4/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert4 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert4/assert4.java b/jbmc/regression/jbmc/assert4/src/main/java/assert4.java similarity index 100% rename from jbmc/regression/jbmc/assert4/assert4.java rename to jbmc/regression/jbmc/assert4/src/main/java/assert4.java diff --git a/jbmc/regression/jbmc/assert4/test.desc b/jbmc/regression/jbmc/assert4/test.desc index 461bde7c38a..31a59524f20 100644 --- a/jbmc/regression/jbmc/assert4/test.desc +++ b/jbmc/regression/jbmc/assert4/test.desc @@ -1,6 +1,6 @@ CORE assert4 - +-cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assert5/assert5.class b/jbmc/regression/jbmc/assert5/assert5.class deleted file mode 100644 index cd56f3a62d6..00000000000 Binary files a/jbmc/regression/jbmc/assert5/assert5.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assert5/pom.xml b/jbmc/regression/jbmc/assert5/pom.xml new file mode 100644 index 00000000000..ef1c69e552e --- /dev/null +++ b/jbmc/regression/jbmc/assert5/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert5 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert5/assert5.java b/jbmc/regression/jbmc/assert5/src/main/java/assert5.java similarity index 100% rename from jbmc/regression/jbmc/assert5/assert5.java rename to jbmc/regression/jbmc/assert5/src/main/java/assert5.java diff --git a/jbmc/regression/jbmc/assert5/test.desc b/jbmc/regression/jbmc/assert5/test.desc index 02dc9fa50a1..a7e4a6f48d5 100644 --- a/jbmc/regression/jbmc/assert5/test.desc +++ b/jbmc/regression/jbmc/assert5/test.desc @@ -1,6 +1,6 @@ CORE assert5 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/assert6/assert6.class b/jbmc/regression/jbmc/assert6/assert6.class deleted file mode 100644 index 82ff1d37483..00000000000 Binary files a/jbmc/regression/jbmc/assert6/assert6.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assert6/pom.xml b/jbmc/regression/jbmc/assert6/pom.xml new file mode 100644 index 00000000000..204345594ad --- /dev/null +++ b/jbmc/regression/jbmc/assert6/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert6 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert6/assert6.java b/jbmc/regression/jbmc/assert6/src/main/java/assert6.java similarity index 100% rename from jbmc/regression/jbmc/assert6/assert6.java rename to jbmc/regression/jbmc/assert6/src/main/java/assert6.java diff --git a/jbmc/regression/jbmc/assert6/test.desc b/jbmc/regression/jbmc/assert6/test.desc index fc3a3f08b34..459b70ed04c 100644 --- a/jbmc/regression/jbmc/assert6/test.desc +++ b/jbmc/regression/jbmc/assert6/test.desc @@ -1,6 +1,6 @@ CORE assert6 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/assert7/Test.class b/jbmc/regression/jbmc/assert7/Test.class deleted file mode 100644 index fbf9949d0e6..00000000000 Binary files a/jbmc/regression/jbmc/assert7/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assert7/pom.xml b/jbmc/regression/jbmc/assert7/pom.xml new file mode 100644 index 00000000000..acb58d24590 --- /dev/null +++ b/jbmc/regression/jbmc/assert7/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assert7 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assert7/Test.java b/jbmc/regression/jbmc/assert7/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/assert7/Test.java rename to jbmc/regression/jbmc/assert7/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/assert7/test.desc b/jbmc/regression/jbmc/assert7/test.desc index dfca31f92d2..a7844ed0c9d 100644 --- a/jbmc/regression/jbmc/assert7/test.desc +++ b/jbmc/regression/jbmc/assert7/test.desc @@ -1,6 +1,6 @@ CORE Test - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/assertion_error_constructors/AssertionIssue.class b/jbmc/regression/jbmc/assertion_error_constructors/AssertionIssue.class deleted file mode 100644 index a9312303951..00000000000 Binary files a/jbmc/regression/jbmc/assertion_error_constructors/AssertionIssue.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assertion_error_constructors/pom.xml b/jbmc/regression/jbmc/assertion_error_constructors/pom.xml new file mode 100644 index 00000000000..358f3d00a3f --- /dev/null +++ b/jbmc/regression/jbmc/assertion_error_constructors/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assertion_error_constructors + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assertion_error_constructors/AssertionIssue.java b/jbmc/regression/jbmc/assertion_error_constructors/src/main/java/AssertionIssue.java similarity index 100% rename from jbmc/regression/jbmc/assertion_error_constructors/AssertionIssue.java rename to jbmc/regression/jbmc/assertion_error_constructors/src/main/java/AssertionIssue.java diff --git a/jbmc/regression/jbmc/assertion_error_constructors/test.desc b/jbmc/regression/jbmc/assertion_error_constructors/test.desc index f138c827612..9c70224212b 100644 --- a/jbmc/regression/jbmc/assertion_error_constructors/test.desc +++ b/jbmc/regression/jbmc/assertion_error_constructors/test.desc @@ -1,6 +1,6 @@ CORE AssertionIssue ---function AssertionIssue.throwAssertion +--function AssertionIssue.throwAssertion -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-integral/My.class b/jbmc/regression/jbmc/assume-inputs-integral/My.class deleted file mode 100644 index e508f3a323b..00000000000 Binary files a/jbmc/regression/jbmc/assume-inputs-integral/My.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume-inputs-integral/Other.class b/jbmc/regression/jbmc/assume-inputs-integral/Other.class deleted file mode 100644 index f9446d51619..00000000000 Binary files a/jbmc/regression/jbmc/assume-inputs-integral/Other.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume-inputs-integral/OtherNoClinit.class b/jbmc/regression/jbmc/assume-inputs-integral/OtherNoClinit.class deleted file mode 100644 index 95a3408e1db..00000000000 Binary files a/jbmc/regression/jbmc/assume-inputs-integral/OtherNoClinit.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume-inputs-integral/arg_assume.desc b/jbmc/regression/jbmc/assume-inputs-integral/arg_assume.desc index 6bac42a905b..d5cc962e8e2 100644 --- a/jbmc/regression/jbmc/assume-inputs-integral/arg_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-integral/arg_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-integral +--function My.numericalArg --java-assume-inputs-integral -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-integral/class_arr_assume.desc b/jbmc/regression/jbmc/assume-inputs-integral/class_arr_assume.desc index df77ba55b85..8997b66c73a 100644 --- a/jbmc/regression/jbmc/assume-inputs-integral/class_arr_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-integral/class_arr_assume.desc @@ -1,6 +1,6 @@ KNOWNBUG My ---function My.arrayArg --java-assume-inputs-integral +--function My.arrayArg --java-assume-inputs-integral -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-integral/class_assume.desc b/jbmc/regression/jbmc/assume-inputs-integral/class_assume.desc index 09bddf0ead6..545afd02d4a 100644 --- a/jbmc/regression/jbmc/assume-inputs-integral/class_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-integral/class_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.classArg --java-assume-inputs-integral +--function My.classArg --java-assume-inputs-integral -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-integral/field_assume.desc b/jbmc/regression/jbmc/assume-inputs-integral/field_assume.desc index a13ea805b48..f9a267e823a 100644 --- a/jbmc/regression/jbmc/assume-inputs-integral/field_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-integral/field_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.field --java-assume-inputs-integral +--function My.field --java-assume-inputs-integral -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-integral/field_assume_static.desc b/jbmc/regression/jbmc/assume-inputs-integral/field_assume_static.desc index 2c36605bb93..0417a35ed45 100644 --- a/jbmc/regression/jbmc/assume-inputs-integral/field_assume_static.desc +++ b/jbmc/regression/jbmc/assume-inputs-integral/field_assume_static.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure My ---function My.fieldStatic --java-assume-inputs-integral --nondet-static +--function My.fieldStatic --java-assume-inputs-integral --nondet-static -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-integral/field_assume_static_no_clinit.desc b/jbmc/regression/jbmc/assume-inputs-integral/field_assume_static_no_clinit.desc index b2dbd3f15dd..a8f6d9a3c11 100644 --- a/jbmc/regression/jbmc/assume-inputs-integral/field_assume_static_no_clinit.desc +++ b/jbmc/regression/jbmc/assume-inputs-integral/field_assume_static_no_clinit.desc @@ -1,6 +1,6 @@ KNOWNBUG symex-driven-lazy-loading-expected-failure My ---function My.fieldStaticNoClinit --java-assume-inputs-integral --nondet-static +--function My.fieldStaticNoClinit --java-assume-inputs-integral --nondet-static -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-integral/pom.xml b/jbmc/regression/jbmc/assume-inputs-integral/pom.xml new file mode 100644 index 00000000000..4c7625f86ec --- /dev/null +++ b/jbmc/regression/jbmc/assume-inputs-integral/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assume-inputs-integral + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume-inputs-integral/My.java b/jbmc/regression/jbmc/assume-inputs-integral/src/main/java/My.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-integral/My.java rename to jbmc/regression/jbmc/assume-inputs-integral/src/main/java/My.java diff --git a/jbmc/regression/jbmc/assume-inputs-integral/Other.java b/jbmc/regression/jbmc/assume-inputs-integral/src/main/java/Other.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-integral/Other.java rename to jbmc/regression/jbmc/assume-inputs-integral/src/main/java/Other.java diff --git a/jbmc/regression/jbmc/assume-inputs-integral/OtherNoClinit.java b/jbmc/regression/jbmc/assume-inputs-integral/src/main/java/OtherNoClinit.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-integral/OtherNoClinit.java rename to jbmc/regression/jbmc/assume-inputs-integral/src/main/java/OtherNoClinit.java diff --git a/jbmc/regression/jbmc/assume-inputs-interval/My.class b/jbmc/regression/jbmc/assume-inputs-interval/My.class deleted file mode 100644 index 006b62236c4..00000000000 Binary files a/jbmc/regression/jbmc/assume-inputs-interval/My.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/Other.class b/jbmc/regression/jbmc/assume-inputs-interval/Other.class deleted file mode 100644 index a9003bedf42..00000000000 Binary files a/jbmc/regression/jbmc/assume-inputs-interval/Other.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.class b/jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.class deleted file mode 100644 index d3324086474..00000000000 Binary files a/jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume.desc index 3175712d29b..89d2682b2e6 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval [1:3] +--function My.numericalArg --java-assume-inputs-interval [1:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid2.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid2.desc index 6d535889918..3d93fb3ed9c 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid2.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid2.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval 2:] +--function My.numericalArg --java-assume-inputs-interval 2:] -cp target/classes ^EXIT=1$ ^SIGNAL=0$ ^Invalid User Input diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid3.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid3.desc index 7e8b719fe8e..b106f88ed35 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid3.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid3.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval [-:1] +--function My.numericalArg --java-assume-inputs-interval [-:1] -cp target/classes ^EXIT=1$ ^SIGNAL=0$ ^Invalid User Input diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid4.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid4.desc index 0d1f6789e55..bd24489455b 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid4.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid4.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval [3:1] +--function My.numericalArg --java-assume-inputs-interval [3:1] -cp target/classes ^EXIT=1$ ^SIGNAL=0$ ^Invalid User Input diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid5.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid5.desc index 11bbef4ed31..0a1d71fa082 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid5.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_invalid5.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval [1.5:3] +--function My.numericalArg --java-assume-inputs-interval [1.5:3] -cp target/classes ^EXIT=1$ ^SIGNAL=0$ ^Invalid User Input diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_neg.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_neg.desc index 7528bab4114..9abcafe0abe 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_neg.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_neg.desc @@ -1,6 +1,6 @@ CORE My ---function My.numericalArg --java-assume-inputs-interval [-1:3] +--function My.numericalArg --java-assume-inputs-interval [-1:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc index cac3205ebdf..5ec0e07c630 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure My ---function My.intervalUnion --java-assume-inputs-interval [3:3] --property 'java::My.intervalUnion:(I)V.assertion.1' --property 'java::My.intervalUnion:(I)V.assertion.2' --property 'java::My.intervalUnion:(I)V.assertion.3' --property 'java::My.intervalUnion:(I)V.assertion.4' --property 'java::My.intervalUnion:(I)V.assertion.6' +--function My.intervalUnion --java-assume-inputs-interval [3:3] --property 'java::My.intervalUnion:(I)V.assertion.1' --property 'java::My.intervalUnion:(I)V.assertion.2' --property 'java::My.intervalUnion:(I)V.assertion.3' --property 'java::My.intervalUnion:(I)V.assertion.4' --property 'java::My.intervalUnion:(I)V.assertion.6' -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_union.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_union.desc index a1916f7e5bb..d3057b0d697 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_union.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_union.desc @@ -1,6 +1,6 @@ CORE My ---function My.intervalUnion --java-assume-inputs-interval [-3:-2],[5:],[1:2] +--function My.intervalUnion --java-assume-inputs-interval [-3:-2],[5:],[1:2] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/class_arr_assume.desc b/jbmc/regression/jbmc/assume-inputs-interval/class_arr_assume.desc index c36f416a1ba..0e2f82284c8 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/class_arr_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/class_arr_assume.desc @@ -1,6 +1,6 @@ KNOWNBUG My ---function My.classArrArg --java-assume-inputs-interval [1:3] +--function My.classArrArg --java-assume-inputs-interval [1:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/class_assume.desc b/jbmc/regression/jbmc/assume-inputs-interval/class_assume.desc index abb58e1710e..04b0347b1d6 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/class_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/class_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.classArg --java-assume-inputs-interval [1:3] +--function My.classArg --java-assume-inputs-interval [1:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/class_assume_lower.desc b/jbmc/regression/jbmc/assume-inputs-interval/class_assume_lower.desc index 0e3c694a653..92267d2bada 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/class_assume_lower.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/class_assume_lower.desc @@ -1,6 +1,6 @@ CORE My ---function My.classArg --java-assume-inputs-interval [1:] +--function My.classArg --java-assume-inputs-interval [1:] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/class_assume_upper.desc b/jbmc/regression/jbmc/assume-inputs-interval/class_assume_upper.desc index 28c8c382d00..23617a1003f 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/class_assume_upper.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/class_assume_upper.desc @@ -1,6 +1,6 @@ CORE My ---function My.classArg --java-assume-inputs-interval [:3] +--function My.classArg --java-assume-inputs-interval [:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/field_assume.desc b/jbmc/regression/jbmc/assume-inputs-interval/field_assume.desc index 103a5364b33..9664d049594 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/field_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/field_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.field --java-assume-inputs-interval [1:3] +--function My.field --java-assume-inputs-interval [1:3] -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static.desc b/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static.desc index 9e1bb28a314..3e1d770d7ca 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure My ---function My.fieldStatic --java-assume-inputs-interval [1:3] --nondet-static +--function My.fieldStatic --java-assume-inputs-interval [1:3] --nondet-static -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static_no_clinit.desc b/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static_no_clinit.desc index a214a8afed8..84d918b5b50 100644 --- a/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static_no_clinit.desc +++ b/jbmc/regression/jbmc/assume-inputs-interval/field_assume_static_no_clinit.desc @@ -1,6 +1,6 @@ KNOWNBUG symex-driven-lazy-loading-expected-failure My ---function My.fieldStaticNoClinit --java-assume-inputs-interval [1:3] --nondet-static +--function My.fieldStaticNoClinit --java-assume-inputs-interval [1:3] --nondet-static -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-interval/pom.xml b/jbmc/regression/jbmc/assume-inputs-interval/pom.xml new file mode 100644 index 00000000000..c1a0ffc5ab4 --- /dev/null +++ b/jbmc/regression/jbmc/assume-inputs-interval/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assume-inputs-interval + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume-inputs-interval/My.java b/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/My.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-interval/My.java rename to jbmc/regression/jbmc/assume-inputs-interval/src/main/java/My.java diff --git a/jbmc/regression/jbmc/assume-inputs-interval/Other.java b/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/Other.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-interval/Other.java rename to jbmc/regression/jbmc/assume-inputs-interval/src/main/java/Other.java diff --git a/jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.java b/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/OtherNoClinit.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.java rename to jbmc/regression/jbmc/assume-inputs-interval/src/main/java/OtherNoClinit.java diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/My.class b/jbmc/regression/jbmc/assume-inputs-non-null/My.class deleted file mode 100644 index ee262398832..00000000000 Binary files a/jbmc/regression/jbmc/assume-inputs-non-null/My.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other.class b/jbmc/regression/jbmc/assume-inputs-non-null/Other.class deleted file mode 100644 index 5e090a36a8e..00000000000 Binary files a/jbmc/regression/jbmc/assume-inputs-non-null/Other.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other2.class b/jbmc/regression/jbmc/assume-inputs-non-null/Other2.class deleted file mode 100644 index 29d7b35b2b8..00000000000 Binary files a/jbmc/regression/jbmc/assume-inputs-non-null/Other2.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc index 7ad022e0f81..4c5932cfd3a 100644 --- a/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.classArg --java-assume-inputs-non-null --max-nondet-string-length 1000 +--function My.classArg --java-assume-inputs-non-null --max-nondet-string-length 1000 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc index be46491c673..8bc4782c4df 100644 --- a/jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.field --java-assume-inputs-non-null +--function My.field --java-assume-inputs-non-null -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/pom.xml b/jbmc/regression/jbmc/assume-inputs-non-null/pom.xml new file mode 100644 index 00000000000..f7f466989fb --- /dev/null +++ b/jbmc/regression/jbmc/assume-inputs-non-null/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assume-inputs-non-null + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/My.java b/jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/My.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-non-null/My.java rename to jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/My.java diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other.java b/jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/Other.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-non-null/Other.java rename to jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/Other.java diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other2.java b/jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/Other2.java similarity index 100% rename from jbmc/regression/jbmc/assume-inputs-non-null/Other2.java rename to jbmc/regression/jbmc/assume-inputs-non-null/src/main/java/Other2.java diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc index a8bae456601..4e3651ee069 100644 --- a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.stringArrayArg --java-assume-inputs-non-null +--function My.stringArrayArg --java-assume-inputs-non-null -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc index dbad249bce4..5737a812498 100644 --- a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.stringArrayArg +--function My.stringArrayArg -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc index bdfb938fb45..fc37e0b71e5 100644 --- a/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc +++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc @@ -1,6 +1,6 @@ CORE My ---function My.stringArg --java-assume-inputs-non-null --max-nondet-string-length 10 +--function My.stringArg --java-assume-inputs-non-null --max-nondet-string-length 10 -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume1/Assume1.class b/jbmc/regression/jbmc/assume1/Assume1.class deleted file mode 100644 index b9a49bc9971..00000000000 Binary files a/jbmc/regression/jbmc/assume1/Assume1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume1/pom.xml b/jbmc/regression/jbmc/assume1/pom.xml new file mode 100644 index 00000000000..f42ba273954 --- /dev/null +++ b/jbmc/regression/jbmc/assume1/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assume1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume1/Assume1.java b/jbmc/regression/jbmc/assume1/src/main/java/Assume1.java similarity index 100% rename from jbmc/regression/jbmc/assume1/Assume1.java rename to jbmc/regression/jbmc/assume1/src/main/java/Assume1.java diff --git a/jbmc/regression/jbmc/assume1/test.desc b/jbmc/regression/jbmc/assume1/test.desc index 5cfc6ec2841..9078c1ab3da 100644 --- a/jbmc/regression/jbmc/assume1/test.desc +++ b/jbmc/regression/jbmc/assume1/test.desc @@ -1,6 +1,6 @@ CORE Assume1 ---function Assume1.foo +--function Assume1.foo -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/assume2/Assume2.class b/jbmc/regression/jbmc/assume2/Assume2.class deleted file mode 100644 index 36e09875d7d..00000000000 Binary files a/jbmc/regression/jbmc/assume2/Assume2.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume2/pom.xml b/jbmc/regression/jbmc/assume2/pom.xml new file mode 100644 index 00000000000..7bddbf26f38 --- /dev/null +++ b/jbmc/regression/jbmc/assume2/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assume2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume2/Assume2.java b/jbmc/regression/jbmc/assume2/src/main/java/Assume2.java similarity index 100% rename from jbmc/regression/jbmc/assume2/Assume2.java rename to jbmc/regression/jbmc/assume2/src/main/java/Assume2.java diff --git a/jbmc/regression/jbmc/assume2/test.desc b/jbmc/regression/jbmc/assume2/test.desc index 10be6fca773..1efbe6bdef5 100644 --- a/jbmc/regression/jbmc/assume2/test.desc +++ b/jbmc/regression/jbmc/assume2/test.desc @@ -1,6 +1,6 @@ CORE Assume2 ---function Assume2.foo +--function Assume2.foo -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/assume3/Assume3.class b/jbmc/regression/jbmc/assume3/Assume3.class deleted file mode 100644 index 916ad4065fb..00000000000 Binary files a/jbmc/regression/jbmc/assume3/Assume3.class and /dev/null differ diff --git a/jbmc/regression/jbmc/assume3/pom.xml b/jbmc/regression/jbmc/assume3/pom.xml new file mode 100644 index 00000000000..0e6f183f5b2 --- /dev/null +++ b/jbmc/regression/jbmc/assume3/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.assume3 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/assume3/Assume3.java b/jbmc/regression/jbmc/assume3/src/main/java/Assume3.java similarity index 100% rename from jbmc/regression/jbmc/assume3/Assume3.java rename to jbmc/regression/jbmc/assume3/src/main/java/Assume3.java diff --git a/jbmc/regression/jbmc/assume3/test.desc b/jbmc/regression/jbmc/assume3/test.desc index 04509cf4cbc..e3d7203f32e 100644 --- a/jbmc/regression/jbmc/assume3/test.desc +++ b/jbmc/regression/jbmc/assume3/test.desc @@ -1,6 +1,6 @@ CORE Assume3 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/astore_aload1/astore_aload1.class b/jbmc/regression/jbmc/astore_aload1/astore_aload1.class deleted file mode 100644 index 730c243fb52..00000000000 Binary files a/jbmc/regression/jbmc/astore_aload1/astore_aload1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/astore_aload1/pom.xml b/jbmc/regression/jbmc/astore_aload1/pom.xml new file mode 100644 index 00000000000..dc7ebf16d41 --- /dev/null +++ b/jbmc/regression/jbmc/astore_aload1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.astore_aload1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/astore_aload1/astore_aload1.java b/jbmc/regression/jbmc/astore_aload1/src/main/java/astore_aload1.java similarity index 100% rename from jbmc/regression/jbmc/astore_aload1/astore_aload1.java rename to jbmc/regression/jbmc/astore_aload1/src/main/java/astore_aload1.java diff --git a/jbmc/regression/jbmc/astore_aload1/test.desc b/jbmc/regression/jbmc/astore_aload1/test.desc index c12fa6d0767..7b9d0fc934e 100644 --- a/jbmc/regression/jbmc/astore_aload1/test.desc +++ b/jbmc/regression/jbmc/astore_aload1/test.desc @@ -1,6 +1,6 @@ CORE astore_aload1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/athrow1/A.class b/jbmc/regression/jbmc/athrow1/A.class deleted file mode 100644 index a5f1be16970..00000000000 Binary files a/jbmc/regression/jbmc/athrow1/A.class and /dev/null differ diff --git a/jbmc/regression/jbmc/athrow1/athrow1.class b/jbmc/regression/jbmc/athrow1/athrow1.class deleted file mode 100644 index 9a5e577142b..00000000000 Binary files a/jbmc/regression/jbmc/athrow1/athrow1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/athrow1/pom.xml b/jbmc/regression/jbmc/athrow1/pom.xml new file mode 100644 index 00000000000..5d45507caa9 --- /dev/null +++ b/jbmc/regression/jbmc/athrow1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.athrow1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/athrow1/athrow1.java b/jbmc/regression/jbmc/athrow1/src/main/java/athrow1.java similarity index 100% rename from jbmc/regression/jbmc/athrow1/athrow1.java rename to jbmc/regression/jbmc/athrow1/src/main/java/athrow1.java diff --git a/jbmc/regression/jbmc/athrow1/test.desc b/jbmc/regression/jbmc/athrow1/test.desc index d5e77f68299..d70f94bc7e5 100644 --- a/jbmc/regression/jbmc/athrow1/test.desc +++ b/jbmc/regression/jbmc/athrow1/test.desc @@ -1,6 +1,6 @@ CORE athrow1 - +-cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/basic1/helloworld.class b/jbmc/regression/jbmc/basic1/helloworld.class deleted file mode 100644 index 244d721feaa..00000000000 Binary files a/jbmc/regression/jbmc/basic1/helloworld.class and /dev/null differ diff --git a/jbmc/regression/jbmc/basic1/pom.xml b/jbmc/regression/jbmc/basic1/pom.xml new file mode 100644 index 00000000000..bd1a129332c --- /dev/null +++ b/jbmc/regression/jbmc/basic1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.basic1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/basic1/helloworld.java b/jbmc/regression/jbmc/basic1/src/main/java/helloworld.java similarity index 100% rename from jbmc/regression/jbmc/basic1/helloworld.java rename to jbmc/regression/jbmc/basic1/src/main/java/helloworld.java diff --git a/jbmc/regression/jbmc/basic1/test.desc b/jbmc/regression/jbmc/basic1/test.desc index 4c355e7c702..0a54dedeb3c 100644 --- a/jbmc/regression/jbmc/basic1/test.desc +++ b/jbmc/regression/jbmc/basic1/test.desc @@ -1,6 +1,6 @@ CORE helloworld - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/basic2/basic.class b/jbmc/regression/jbmc/basic2/basic.class deleted file mode 100644 index cfaa6ef986e..00000000000 Binary files a/jbmc/regression/jbmc/basic2/basic.class and /dev/null differ diff --git a/jbmc/regression/jbmc/basic2/basic2.class b/jbmc/regression/jbmc/basic2/basic2.class deleted file mode 100644 index c75dafa2bee..00000000000 Binary files a/jbmc/regression/jbmc/basic2/basic2.class and /dev/null differ diff --git a/jbmc/regression/jbmc/basic2/pom.xml b/jbmc/regression/jbmc/basic2/pom.xml new file mode 100644 index 00000000000..8a7197539ed --- /dev/null +++ b/jbmc/regression/jbmc/basic2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.basic2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/basic2/basic.java b/jbmc/regression/jbmc/basic2/src/main/java/basic.java similarity index 100% rename from jbmc/regression/jbmc/basic2/basic.java rename to jbmc/regression/jbmc/basic2/src/main/java/basic.java diff --git a/jbmc/regression/jbmc/basic2/test.desc b/jbmc/regression/jbmc/basic2/test.desc index 260f047024f..fe3693b2412 100644 --- a/jbmc/regression/jbmc/basic2/test.desc +++ b/jbmc/regression/jbmc/basic2/test.desc @@ -1,6 +1,6 @@ CORE basic - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/bitwise1/bitwise1.class b/jbmc/regression/jbmc/bitwise1/bitwise1.class deleted file mode 100644 index ae41460ca8a..00000000000 Binary files a/jbmc/regression/jbmc/bitwise1/bitwise1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/bitwise1/pom.xml b/jbmc/regression/jbmc/bitwise1/pom.xml new file mode 100644 index 00000000000..94147b570b0 --- /dev/null +++ b/jbmc/regression/jbmc/bitwise1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.bitwise1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/bitwise1/bitwise1.java b/jbmc/regression/jbmc/bitwise1/src/main/java/bitwise1.java similarity index 100% rename from jbmc/regression/jbmc/bitwise1/bitwise1.java rename to jbmc/regression/jbmc/bitwise1/src/main/java/bitwise1.java diff --git a/jbmc/regression/jbmc/bitwise1/test.desc b/jbmc/regression/jbmc/bitwise1/test.desc index c72bb47d6d5..0271dbaab5c 100644 --- a/jbmc/regression/jbmc/bitwise1/test.desc +++ b/jbmc/regression/jbmc/bitwise1/test.desc @@ -1,6 +1,6 @@ CORE bitwise1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/boolean1/boolean1.class b/jbmc/regression/jbmc/boolean1/boolean1.class deleted file mode 100644 index 06838038368..00000000000 Binary files a/jbmc/regression/jbmc/boolean1/boolean1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/boolean1/pom.xml b/jbmc/regression/jbmc/boolean1/pom.xml new file mode 100644 index 00000000000..12e6ee31b9e --- /dev/null +++ b/jbmc/regression/jbmc/boolean1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.boolean1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/boolean1/boolean1.java b/jbmc/regression/jbmc/boolean1/src/main/java/boolean1.java similarity index 100% rename from jbmc/regression/jbmc/boolean1/boolean1.java rename to jbmc/regression/jbmc/boolean1/src/main/java/boolean1.java diff --git a/jbmc/regression/jbmc/boolean1/test.desc b/jbmc/regression/jbmc/boolean1/test.desc index 808347e008b..bc15c092cef 100644 --- a/jbmc/regression/jbmc/boolean1/test.desc +++ b/jbmc/regression/jbmc/boolean1/test.desc @@ -1,6 +1,6 @@ CORE boolean1 ---function boolean1.doit +--function boolean1.doit -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/boolean2/boolean2.class b/jbmc/regression/jbmc/boolean2/boolean2.class deleted file mode 100644 index 86c6fdf0ffa..00000000000 Binary files a/jbmc/regression/jbmc/boolean2/boolean2.class and /dev/null differ diff --git a/jbmc/regression/jbmc/boolean2/pom.xml b/jbmc/regression/jbmc/boolean2/pom.xml new file mode 100644 index 00000000000..4fbb0b87e87 --- /dev/null +++ b/jbmc/regression/jbmc/boolean2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.boolean2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/boolean2/boolean2.java b/jbmc/regression/jbmc/boolean2/src/main/java/boolean2.java similarity index 100% rename from jbmc/regression/jbmc/boolean2/boolean2.java rename to jbmc/regression/jbmc/boolean2/src/main/java/boolean2.java diff --git a/jbmc/regression/jbmc/boolean2/test.desc b/jbmc/regression/jbmc/boolean2/test.desc index e457b40c62b..93e69f9d0dd 100644 --- a/jbmc/regression/jbmc/boolean2/test.desc +++ b/jbmc/regression/jbmc/boolean2/test.desc @@ -1,6 +1,6 @@ CORE boolean2 ---function boolean2.entry +--function boolean2.entry -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/cast1/cast1.class b/jbmc/regression/jbmc/cast1/cast1.class deleted file mode 100644 index 5b163e52559..00000000000 Binary files a/jbmc/regression/jbmc/cast1/cast1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/cast1/pom.xml b/jbmc/regression/jbmc/cast1/pom.xml new file mode 100644 index 00000000000..5b0d5af7058 --- /dev/null +++ b/jbmc/regression/jbmc/cast1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.cast1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/cast1/cast1.java b/jbmc/regression/jbmc/cast1/src/main/java/cast1.java similarity index 100% rename from jbmc/regression/jbmc/cast1/cast1.java rename to jbmc/regression/jbmc/cast1/src/main/java/cast1.java diff --git a/jbmc/regression/jbmc/cast1/test.desc b/jbmc/regression/jbmc/cast1/test.desc index e7393a374a8..72f8ef0639e 100644 --- a/jbmc/regression/jbmc/cast1/test.desc +++ b/jbmc/regression/jbmc/cast1/test.desc @@ -1,6 +1,6 @@ CORE cast1 - +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/cast_null1/pom.xml b/jbmc/regression/jbmc/cast_null1/pom.xml new file mode 100644 index 00000000000..5993228a356 --- /dev/null +++ b/jbmc/regression/jbmc/cast_null1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.cast_null1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/cast_null1/test.java b/jbmc/regression/jbmc/cast_null1/src/main/java/test.java similarity index 100% rename from jbmc/regression/jbmc/cast_null1/test.java rename to jbmc/regression/jbmc/cast_null1/src/main/java/test.java diff --git a/jbmc/regression/jbmc/cast_null1/test.class b/jbmc/regression/jbmc/cast_null1/test.class deleted file mode 100644 index efced7cc257..00000000000 Binary files a/jbmc/regression/jbmc/cast_null1/test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/cast_null1/test.desc b/jbmc/regression/jbmc/cast_null1/test.desc index 4f9c1abf9f9..0da520e5d42 100644 --- a/jbmc/regression/jbmc/cast_null1/test.desc +++ b/jbmc/regression/jbmc/cast_null1/test.desc @@ -1,6 +1,6 @@ CORE test ---function test.main +--function test.main -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/cast_null2/pom.xml b/jbmc/regression/jbmc/cast_null2/pom.xml new file mode 100644 index 00000000000..4091bd8afab --- /dev/null +++ b/jbmc/regression/jbmc/cast_null2/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.cast_null2 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/cast_null2/test.java b/jbmc/regression/jbmc/cast_null2/src/main/java/test.java similarity index 100% rename from jbmc/regression/jbmc/cast_null2/test.java rename to jbmc/regression/jbmc/cast_null2/src/main/java/test.java diff --git a/jbmc/regression/jbmc/cast_null2/test.class b/jbmc/regression/jbmc/cast_null2/test.class deleted file mode 100644 index efced7cc257..00000000000 Binary files a/jbmc/regression/jbmc/cast_null2/test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/cast_null2/test.desc b/jbmc/regression/jbmc/cast_null2/test.desc index c7a3dcfa352..9b0a7fe4352 100644 --- a/jbmc/regression/jbmc/cast_null2/test.desc +++ b/jbmc/regression/jbmc/cast_null2/test.desc @@ -1,6 +1,6 @@ CORE test ---throw-runtime-exceptions --function test.main +--throw-runtime-exceptions --function test.main -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/catch1/catch1.class b/jbmc/regression/jbmc/catch1/catch1.class deleted file mode 100644 index 7af4da2e97f..00000000000 Binary files a/jbmc/regression/jbmc/catch1/catch1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/catch1/pom.xml b/jbmc/regression/jbmc/catch1/pom.xml new file mode 100644 index 00000000000..0e2a1c2b704 --- /dev/null +++ b/jbmc/regression/jbmc/catch1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.catch1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/catch1/catch1.java b/jbmc/regression/jbmc/catch1/src/main/java/catch1.java similarity index 52% rename from jbmc/regression/jbmc/catch1/catch1.java rename to jbmc/regression/jbmc/catch1/src/main/java/catch1.java index 1fb128a8593..78beb3c1050 100644 --- a/jbmc/regression/jbmc/catch1/catch1.java +++ b/jbmc/regression/jbmc/catch1/src/main/java/catch1.java @@ -8,7 +8,7 @@ class some_exception2 extends some_exception1 class catch1 { - public static void main(String[] args) + public static void catchSuper() throws Throwable { try { @@ -19,5 +19,17 @@ public static void main(String[] args) { } } + + public static void catchSub() throws Throwable + { + try + { + throw new some_exception1(); + } + + catch(some_exception2 e) + { + } + } } diff --git a/jbmc/regression/jbmc/catch1/test.desc b/jbmc/regression/jbmc/catch1/test.desc deleted file mode 100644 index fa539538486..00000000000 --- a/jbmc/regression/jbmc/catch1/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -catch1 - -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ -^\[.*\] line 15 no uncaught exception: FAILURE$ --- -^warning: ignoring diff --git a/jbmc/regression/jbmc/catch1/test_catch_sub.desc b/jbmc/regression/jbmc/catch1/test_catch_sub.desc new file mode 100644 index 00000000000..0dbd07fa628 --- /dev/null +++ b/jbmc/regression/jbmc/catch1/test_catch_sub.desc @@ -0,0 +1,9 @@ +CORE +catch1.catchSub +-cp target/classes +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +^\[.*\] line 27 no uncaught exception: FAILURE$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc b/jbmc/regression/jbmc/catch1/test_catch_super.desc similarity index 63% rename from jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc rename to jbmc/regression/jbmc/catch1/test_catch_super.desc index 73abd712abc..766bb46003a 100644 --- a/jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc +++ b/jbmc/regression/jbmc/catch1/test_catch_super.desc @@ -1,6 +1,6 @@ CORE -catch1 ---disable-uncaught-exception-check +catch1.catchSuper +-cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/char1/char1.class b/jbmc/regression/jbmc/char1/char1.class deleted file mode 100644 index 67e32dd1403..00000000000 Binary files a/jbmc/regression/jbmc/char1/char1.class and /dev/null differ diff --git a/jbmc/regression/jbmc/char1/pom.xml b/jbmc/regression/jbmc/char1/pom.xml new file mode 100644 index 00000000000..9b6c013ddfb --- /dev/null +++ b/jbmc/regression/jbmc/char1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.char1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/char1/char1.java b/jbmc/regression/jbmc/char1/src/main/java/char1.java similarity index 100% rename from jbmc/regression/jbmc/char1/char1.java rename to jbmc/regression/jbmc/char1/src/main/java/char1.java diff --git a/jbmc/regression/jbmc/char1/test.desc b/jbmc/regression/jbmc/char1/test.desc index c2c964cc359..39a14ae6b10 100644 --- a/jbmc/regression/jbmc/char1/test.desc +++ b/jbmc/regression/jbmc/char1/test.desc @@ -1,6 +1,6 @@ CORE char1 ---function char1.doit +--function char1.doit -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/class-fields/Test.class b/jbmc/regression/jbmc/class-fields/Test.class deleted file mode 100644 index a69b61691fe..00000000000 Binary files a/jbmc/regression/jbmc/class-fields/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-fields/java/lang/Class.class b/jbmc/regression/jbmc/class-fields/java/lang/Class.class deleted file mode 100644 index e788df0f4ce..00000000000 Binary files a/jbmc/regression/jbmc/class-fields/java/lang/Class.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-fields/org/cprover/CProver.class b/jbmc/regression/jbmc/class-fields/org/cprover/CProver.class deleted file mode 100644 index cd291032b8d..00000000000 Binary files a/jbmc/regression/jbmc/class-fields/org/cprover/CProver.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-fields/org/cprover/CProver.java b/jbmc/regression/jbmc/class-fields/org/cprover/CProver.java deleted file mode 100644 index fe21dd16ad4..00000000000 --- a/jbmc/regression/jbmc/class-fields/org/cprover/CProver.java +++ /dev/null @@ -1,15 +0,0 @@ -package org.cprover; - -public final class CProver -{ - public static final boolean enableAssume=true; - - public static void assume(boolean condition) - { - if(enableAssume) - { - throw new RuntimeException( - "Cannot execute program with CProver.assume()"); - } - } -} diff --git a/jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.class b/jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.class deleted file mode 100644 index ca862caecb9..00000000000 Binary files a/jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.java b/jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.java deleted file mode 100644 index 7be14b181d7..00000000000 --- a/jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.java +++ /dev/null @@ -1,8 +0,0 @@ -package org.cprover; - -/** - * This can be added to methods to indicate they aren't allowed to throw - * exceptions. JBMC and related tools will truncate any execution path on which - * they do with an ASSUME FALSE instruction. - */ -public @interface MustNotThrow { } diff --git a/jbmc/regression/jbmc/class-fields/pom.xml b/jbmc/regression/jbmc/class-fields/pom.xml new file mode 100644 index 00000000000..35a288f250b --- /dev/null +++ b/jbmc/regression/jbmc/class-fields/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.class-fields + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/class-fields/Test.java b/jbmc/regression/jbmc/class-fields/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/class-fields/Test.java rename to jbmc/regression/jbmc/class-fields/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/class-fields/java/lang/Class.java b/jbmc/regression/jbmc/class-fields/src/main/java/java/lang/Class.java similarity index 74% rename from jbmc/regression/jbmc/class-fields/java/lang/Class.java rename to jbmc/regression/jbmc/class-fields/src/main/java/java/lang/Class.java index eba32beb0a2..dcf22323ddd 100644 --- a/jbmc/regression/jbmc/class-fields/java/lang/Class.java +++ b/jbmc/regression/jbmc/class-fields/src/main/java/java/lang/Class.java @@ -9,4 +9,7 @@ protected void cproverNondetInitialize() { org.cprover.CProver.assume(field == null); } + public boolean desiredAssertionStatus() { + return true; + } } diff --git a/jbmc/regression/jbmc/class-fields/test.desc b/jbmc/regression/jbmc/class-fields/test.desc index 7d5b6849915..637fdb3d2ee 100644 --- a/jbmc/regression/jbmc/class-fields/test.desc +++ b/jbmc/regression/jbmc/class-fields/test.desc @@ -1,6 +1,6 @@ CORE Test ---function Test.main +--function Test.main -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/class-literals/ExampleAnnotation.class b/jbmc/regression/jbmc/class-literals/ExampleAnnotation.class deleted file mode 100644 index ab1a9793533..00000000000 Binary files a/jbmc/regression/jbmc/class-literals/ExampleAnnotation.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-literals/ExampleEnum.class b/jbmc/regression/jbmc/class-literals/ExampleEnum.class deleted file mode 100644 index 17ed2db3139..00000000000 Binary files a/jbmc/regression/jbmc/class-literals/ExampleEnum.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-literals/ExampleInterface.class b/jbmc/regression/jbmc/class-literals/ExampleInterface.class deleted file mode 100644 index 3669f3afa5c..00000000000 Binary files a/jbmc/regression/jbmc/class-literals/ExampleInterface.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-literals/ExampleSynthetic.class b/jbmc/regression/jbmc/class-literals/ExampleSynthetic.class deleted file mode 100644 index 3be8707e65e..00000000000 Binary files a/jbmc/regression/jbmc/class-literals/ExampleSynthetic.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-literals/Test.class b/jbmc/regression/jbmc/class-literals/Test.class deleted file mode 100644 index c6ca2351f0d..00000000000 Binary files a/jbmc/regression/jbmc/class-literals/Test.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-literals/java/lang/Class.class b/jbmc/regression/jbmc/class-literals/java/lang/Class.class deleted file mode 100644 index e81318158e0..00000000000 Binary files a/jbmc/regression/jbmc/class-literals/java/lang/Class.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/CProver.class b/jbmc/regression/jbmc/class-literals/org/cprover/CProver.class deleted file mode 100644 index cd291032b8d..00000000000 Binary files a/jbmc/regression/jbmc/class-literals/org/cprover/CProver.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/CProver.java b/jbmc/regression/jbmc/class-literals/org/cprover/CProver.java deleted file mode 100644 index fe21dd16ad4..00000000000 --- a/jbmc/regression/jbmc/class-literals/org/cprover/CProver.java +++ /dev/null @@ -1,15 +0,0 @@ -package org.cprover; - -public final class CProver -{ - public static final boolean enableAssume=true; - - public static void assume(boolean condition) - { - if(enableAssume) - { - throw new RuntimeException( - "Cannot execute program with CProver.assume()"); - } - } -} diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.class b/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.class deleted file mode 100644 index ca862caecb9..00000000000 Binary files a/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.class and /dev/null differ diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.java b/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.java deleted file mode 100644 index 7be14b181d7..00000000000 --- a/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.java +++ /dev/null @@ -1,8 +0,0 @@ -package org.cprover; - -/** - * This can be added to methods to indicate they aren't allowed to throw - * exceptions. JBMC and related tools will truncate any execution path on which - * they do with an ASSUME FALSE instruction. - */ -public @interface MustNotThrow { } diff --git a/jbmc/regression/jbmc/class-literals/pom.xml b/jbmc/regression/jbmc/class-literals/pom.xml new file mode 100644 index 00000000000..7398a7121cb --- /dev/null +++ b/jbmc/regression/jbmc/class-literals/pom.xml @@ -0,0 +1,41 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.class-literals + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + com.github.abextm + jasmin-maven-plugin + + + + + diff --git a/jbmc/regression/jbmc/class-literals/ExampleAnnotation.java b/jbmc/regression/jbmc/class-literals/src/main/java/ExampleAnnotation.java similarity index 100% rename from jbmc/regression/jbmc/class-literals/ExampleAnnotation.java rename to jbmc/regression/jbmc/class-literals/src/main/java/ExampleAnnotation.java diff --git a/jbmc/regression/jbmc/class-literals/ExampleEnum.java b/jbmc/regression/jbmc/class-literals/src/main/java/ExampleEnum.java similarity index 100% rename from jbmc/regression/jbmc/class-literals/ExampleEnum.java rename to jbmc/regression/jbmc/class-literals/src/main/java/ExampleEnum.java diff --git a/jbmc/regression/jbmc/class-literals/ExampleInterface.java b/jbmc/regression/jbmc/class-literals/src/main/java/ExampleInterface.java similarity index 100% rename from jbmc/regression/jbmc/class-literals/ExampleInterface.java rename to jbmc/regression/jbmc/class-literals/src/main/java/ExampleInterface.java diff --git a/jbmc/regression/jbmc/class-literals/ExampleSynthetic.j b/jbmc/regression/jbmc/class-literals/src/main/java/ExampleSynthetic.j similarity index 100% rename from jbmc/regression/jbmc/class-literals/ExampleSynthetic.j rename to jbmc/regression/jbmc/class-literals/src/main/java/ExampleSynthetic.j diff --git a/jbmc/regression/jbmc/class-literals/Test.java b/jbmc/regression/jbmc/class-literals/src/main/java/Test.java similarity index 100% rename from jbmc/regression/jbmc/class-literals/Test.java rename to jbmc/regression/jbmc/class-literals/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/class-literals/java/lang/Class.java b/jbmc/regression/jbmc/class-literals/src/main/java/java/lang/Class.java similarity index 93% rename from jbmc/regression/jbmc/class-literals/java/lang/Class.java rename to jbmc/regression/jbmc/class-literals/src/main/java/java/lang/Class.java index c39aedf97cb..162a8b70515 100644 --- a/jbmc/regression/jbmc/class-literals/java/lang/Class.java +++ b/jbmc/regression/jbmc/class-literals/src/main/java/java/lang/Class.java @@ -1,6 +1,6 @@ package java.lang; -public class Class { +public class Class { private String name; @@ -43,4 +43,6 @@ public void cproverInitializeClassLiteral( public boolean isLocalClass() { return isLocalClass; } public boolean isMemberClass() { return isMemberClass; } public boolean isEnum() { return isEnum; } + + public boolean desiredAssertionStatus() { return true; } } diff --git a/jbmc/regression/jbmc/class-literals/test.desc b/jbmc/regression/jbmc/class-literals/test.desc index 513924f665e..3ac8b38eb62 100644 --- a/jbmc/regression/jbmc/class-literals/test.desc +++ b/jbmc/regression/jbmc/class-literals/test.desc @@ -1,6 +1,6 @@ CORE bdd-expected-timeout Test ---function Test.main +--function Test.main -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/class-literals/test_lazy.desc b/jbmc/regression/jbmc/class-literals/test_lazy.desc index 76b0dd8b13e..e0bd3dcc723 100644 --- a/jbmc/regression/jbmc/class-literals/test_lazy.desc +++ b/jbmc/regression/jbmc/class-literals/test_lazy.desc @@ -1,6 +1,6 @@ CORE symex-driven-lazy-loading-expected-failure Test ---function Test.main +--function Test.main -cp target/classes ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 9452e36ad45..374981ad7ee 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -15,7 +15,60 @@ + aastore_aaload1 + address_space_size_limit1 + address_space_size_limit2 + annotations1 + annotations2 ArithmeticException1 + ArithmeticException2 + ArithmeticException3 + ArithmeticException4 + ArithmeticException5 + ArithmeticException6 + ArithmeticException7 + array1 + array2 + array-cell-sensitivity1 + array-cell-sensitivity2 + array-cell-sensitivity-negative-size + array-cell-sensitivity-static-fields + array-clone + array_nonconstsize_nonconstaccess + ArrayIndexOutOfBoundsException1 + ArrayIndexOutOfBoundsException2 + ArrayIndexOutOfBoundsException3 + arraylength1 + arrayread1 + assert1 + assert2 + assert3 + assert4 + assert5 + assert6 + assert7 + assert-no-exceptions-thrown + assertion_error_constructors + assume1 + assume2 + assume3 + assume-inputs-integral + assume-inputs-interval + assume-inputs-non-null + astore_aload1 + athrow1 + basic1 + basic2 + bitwise1 + boolean1 + boolean2 + cast1 + cast_null1 + cast_null2 + catch1 + char1 + class-fields + class-literals classpath-jar-load-whole-jar diff --git a/jbmc/regression/pom.xml b/jbmc/regression/pom.xml index 16dab954a94..443265182f5 100644 --- a/jbmc/regression/pom.xml +++ b/jbmc/regression/pom.xml @@ -20,9 +20,42 @@ book-examples + + + + jitpack.io + https://jitpack.io + + + + + + + org.cprover.util + cprover-api + 1.0.0 + system + ${maven.multiModuleProjectDirectory}/../lib/java-models-library/target/cprover-api.jar + + + + + + com.github.abextm + jasmin-maven-plugin + 1.0 + + + generate-sources + + compile-jasmin + + + + org.apache.maven.plugins maven-jar-plugin diff --git a/jbmc/src/jbmc/CMakeLists.txt b/jbmc/src/jbmc/CMakeLists.txt index c1735e3ed94..3772687126a 100644 --- a/jbmc/src/jbmc/CMakeLists.txt +++ b/jbmc/src/jbmc/CMakeLists.txt @@ -32,8 +32,8 @@ add_executable(jbmc jbmc_main.cpp) target_link_libraries(jbmc jbmc-lib) install(TARGETS jbmc DESTINATION ${CMAKE_INSTALL_BINDIR}) -# make sure java-models-library and java-regression is built at least once -add_dependencies(jbmc java-models-library java-regression) +# make sure java-models-library (on which java-regression depends) is built at least once +add_dependencies(jbmc java-regression) # Man page if(NOT WIN32)