Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Compile Java regression test sources (4/n) #8553

Merged
merged 47 commits into from
Jan 6, 2025
Merged

Compile Java regression test sources (4/n) #8553

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
47 commits
Select commit Hold shift + click to select a range
89e46c8
Compile jbmc/aastore_aaload1 test sources
peterschrammel Dec 31, 2024
8156b37
Compile jbmc/address_space_size_limit1 test sources
peterschrammel Jan 2, 2025
4f2abc5
Compile jbmc/address_space_size_limit2 test sources
peterschrammel Jan 2, 2025
9026b89
Compile jbmc/annotations1 test sources
peterschrammel Jan 2, 2025
32e9d9a
Compile jbmc/annotations2 test sources
peterschrammel Jan 2, 2025
0f323e9
Compile jbmc/ArithmeticException2 test sources
peterschrammel Jan 2, 2025
a319745
Compile jbmc/ArithmeticException3 test sources
peterschrammel Jan 2, 2025
e11c5b9
Compile jbmc/ArithmeticException4 test sources
peterschrammel Jan 2, 2025
06a22ea
Compile jbmc/ArithmeticException5 test sources
peterschrammel Jan 2, 2025
7c18639
Compile jbmc/ArithmeticException6 test sources
peterschrammel Jan 2, 2025
42c3f8d
Compile jbmc/ArithmeticException7 test sources
peterschrammel Jan 2, 2025
b44d1f4
Compile jbmc/array1 test sources
peterschrammel Jan 2, 2025
f657d50
Compile jbmc/array2 test sources
peterschrammel Jan 2, 2025
c321c93
Compile jbmc/array-cell-sensitivity1 test sources
peterschrammel Jan 2, 2025
8a1652e
Compile jbmc/array-cell-sensitivity2 test sources
peterschrammel Jan 2, 2025
753e24c
Compile jbmc/array-cell-sensitivity-negative-size test sources
peterschrammel Jan 2, 2025
bc0df89
Compile jbmc/array-cell-sensitivity-static-fields test sources
peterschrammel Jan 2, 2025
dde14a4
Compile jbmc/array-clone test sources
peterschrammel Jan 2, 2025
fef2fa6
Compile jbmc/array_nonconstsize_nonconstaccess test sources
peterschrammel Jan 2, 2025
c6b5963
Compile jbmc/ArrayIndexOutOfBoundsException1 test sources
peterschrammel Jan 2, 2025
087c1b2
Compile jbmc/ArrayIndexOutOfBoundsException2 test sources
peterschrammel Jan 2, 2025
9067560
Compile jbmc/ArrayIndexOutOfBoundsException3 test sources
peterschrammel Jan 2, 2025
2ed897b
Compile jbmc/arraylength1 test sources
peterschrammel Jan 2, 2025
d5b088d
Compile jbmc/arrayread1 test sources
peterschrammel Jan 2, 2025
14bfce7
Compile jbmc/assert1 test sources
peterschrammel Jan 2, 2025
8b68ff4
Compile jbmc/assert2 test sources
peterschrammel Jan 2, 2025
068d80a
Compile jbmc/assert3 test sources
peterschrammel Jan 2, 2025
46797db
Compile jbmc/assert4 test sources
peterschrammel Jan 2, 2025
40965b0
Compile jbmc/assert5 test sources
peterschrammel Jan 2, 2025
cf4c3e4
Compile jbmc/assert6 test sources
peterschrammel Jan 2, 2025
2811d0e
Compile jbmc/assert7 test sources
peterschrammel Jan 2, 2025
0bac843
Compile jbmc/assert-no-exceptions-thrown test sources
peterschrammel Jan 2, 2025
76ab937
Compile jbmc/assertion_error_constructors test sources
peterschrammel Jan 2, 2025
3de1908
Make Java regression test compilation depend on models-library
peterschrammel Jan 3, 2025
c8fe05c
Compile jbmc/assume1 test sources
peterschrammel Jan 2, 2025
76423e0
Compile jbmc/assume2 test sources
peterschrammel Jan 2, 2025
b4c7470
Compile jbmc/assume3 test sources
peterschrammel Jan 2, 2025
aa4e88f
Compile jbmc/assume-inputs-integral test sources
peterschrammel Jan 2, 2025
b5bc805
Compile jbmc/assume-inputs-interval test sources
peterschrammel Jan 2, 2025
54c4402
Compile jbmc/assume-inputs-non-null test sources
peterschrammel Jan 2, 2025
f69d05f
Compile jbmc/astore_aload1 test sources
peterschrammel Jan 2, 2025
5672a05
Compile jbmc/athrow1 test sources
peterschrammel Jan 2, 2025
173b5b7
Compile jbmc/basic1 test sources
peterschrammel Jan 2, 2025
fb1bed2
Compile jbmc/basic2 test sources
peterschrammel Jan 2, 2025
f73c738
Compile jbmc/bitwise1 test sources
peterschrammel Jan 2, 2025
7ea59f0
Compile jbmc/boolean1 test sources
peterschrammel Jan 2, 2025
7e4897c
Compile jbmc/boolean2 test sources
peterschrammel Jan 2, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions jbmc/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Binary file removed jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/ArithmeticException2/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.ArithmeticException2</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>
0 ...icException2/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/ArithmeticException2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Binary file removed jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/ArithmeticException3/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.ArithmeticException3</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>
0 ...icException3/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/ArithmeticException3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Binary file removed jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/ArithmeticException4/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.ArithmeticException4</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>
0 ...icException4/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/ArithmeticException4/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Binary file removed jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/ArithmeticException5/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.ArithmeticException5</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>
0 ...icException5/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/ArithmeticException5/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
ArithmeticExceptionTest
--throw-runtime-exceptions
--throw-runtime-exceptions -cp target/classes
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL
Expand Down
Binary file removed jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/ArithmeticException6/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.ArithmeticException6</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>
0 ...icException6/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/ArithmeticException6/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Binary file removed jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.class
View file
Open in desktop
Binary file not shown.
Binary file removed jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.class
View file
Open in desktop
Binary file not shown.
Binary file removed jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/ArithmeticException7/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.ArithmeticException7</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>
0 ...icException7/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
View file
Open in desktop
File renamed without changes.
0 ...ption7/java/lang/ArithmeticException.java → ...n/java/java/lang/ArithmeticException.java
View file
Open in desktop
File renamed without changes.
0 ...xception7/java/lang/RuntimeException.java → ...main/java/java/lang/RuntimeException.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/ArithmeticException7/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Binary file removed .../regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.ArrayIndexOutOfBoundsException1</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>
0 ...1/ArrayIndexOutOfBoundsExceptionTest.java → ...a/ArrayIndexOutOfBoundsExceptionTest.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Binary file removed .../regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.ArrayIndexOutOfBoundsException2</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>
0 ...2/ArrayIndexOutOfBoundsExceptionTest.java → ...a/ArrayIndexOutOfBoundsExceptionTest.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Binary file removed .../regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class
View file
Open in desktop
Binary file not shown.
Binary file removed ...ssion/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class
View file
Open in desktop
Binary file not shown.
Binary file removed ...regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class
View file
Open in desktop
Binary file not shown.
Binary file removed jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.ArrayIndexOutOfBoundsException3</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>
0 ...3/ArrayIndexOutOfBoundsExceptionTest.java → ...a/ArrayIndexOutOfBoundsExceptionTest.java
View file
Open in desktop
File renamed without changes.
0 .../lang/ArrayIndexOutOfBoundsException.java → .../lang/ArrayIndexOutOfBoundsException.java
View file
Open in desktop
File renamed without changes.
0 .../java/lang/IndexOutOfBoundsException.java → .../java/lang/IndexOutOfBoundsException.java
View file
Open in desktop
File renamed without changes.
0 ...xception3/java/lang/RuntimeException.java → ...main/java/java/lang/RuntimeException.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
Binary file removed jbmc/regression/jbmc/aastore_aaload1/A.class
View file
Open in desktop
Binary file not shown.
Binary file removed jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.class
View file
Open in desktop
Binary file not shown.
30 changes: 30 additions & 0 deletions jbmc/regression/jbmc/aastore_aaload1/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.aastore_aaload1</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>
0 ...jbmc/aastore_aaload1/aastore_aaload1.java → ...aload1/src/main/java/aastore_aaload1.java
View file
Open in desktop
File renamed without changes.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/aastore_aaload1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
aastore_aaload1

-cp target/classes
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
Binary file removed jbmc/regression/jbmc/address_space_size_limit1/Test.class
View file
Open in desktop
Binary file not shown.
Loading
Loading