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 034e4b9ae1e..374981ad7ee 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -68,6 +68,7 @@ catch1 char1 class-fields + class-literals classpath-jar-load-whole-jar