Compile jbmc/assume-inputs-interval test sources

peterschrammel · peterschrammel · commit b5bc805bef59 · 2025-01-04T19:04:40.000+01:00
Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files.
diff --git a/jbmc/regression/jbmc/assume-inputs-interval/My.class b/jbmc/regression/jbmc/assume-inputs-interval/My.class
diff --git a/jbmc/regression/jbmc/assume-inputs-interval/Other.class b/jbmc/regression/jbmc/assume-inputs-interval/Other.class
diff --git a/jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.class b/jbmc/regression/jbmc/assume-inputs-interval/OtherNoClinit.class
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.assume-inputs-interval</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/My.java b/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/My.java
diff --git a/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/Other.java b/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/Other.java
diff --git a/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/OtherNoClinit.java b/jbmc/regression/jbmc/assume-inputs-interval/src/main/java/OtherNoClinit.java
diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml
@@ -53,6 +53,7 @@
         <module>assume2</module>
         <module>assume3</module>
         <module>assume-inputs-integral</module>
+        <module>assume-inputs-interval</module>
         <module>classpath-jar-load-whole-jar</module>
     </modules>
 
