Skip to content

Commit 5ae1452

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #8553 from peterschrammel/ps/compile-java-regression-test-sources4
Compile Java regression test sources (4/n)
2 parents 1e99418 + 7e4897c commit 5ae1452

File tree

280 files changed

+1554
-93
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

280 files changed

+1554
-93
lines changed

‎jbmc/CMakeLists.txt

+2
Original file line numberDiff line numberDiff line change
@@ -56,3 +56,5 @@ add_custom_command(OUTPUT ${java_regression_compiled_sources}
5656
add_custom_target(java-regression ALL
5757
DEPENDS ${java_regression_compiled_sources}
5858
)
59+
60+
add_dependencies(java-regression java-models-library)

‎jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.class

-646 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArithmeticException2/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.ArithmeticException2</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/ArithmeticException2/ArithmeticExceptionTest.java ‎jbmc/regression/jbmc/ArithmeticException2/src/main/java/ArithmeticExceptionTest.java

File renamed without changes.

‎jbmc/regression/jbmc/ArithmeticException2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
ArithmeticExceptionTest
3-
--throw-runtime-exceptions
3+
--throw-runtime-exceptions -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$

‎jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.class

-629 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArithmeticException3/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.ArithmeticException3</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/ArithmeticException3/ArithmeticExceptionTest.java ‎jbmc/regression/jbmc/ArithmeticException3/src/main/java/ArithmeticExceptionTest.java

File renamed without changes.

‎jbmc/regression/jbmc/ArithmeticException3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
ArithmeticExceptionTest
3-
--throw-runtime-exceptions
3+
--throw-runtime-exceptions -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

‎jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.class

-646 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArithmeticException4/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.ArithmeticException4</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/ArithmeticException4/ArithmeticExceptionTest.java ‎jbmc/regression/jbmc/ArithmeticException4/src/main/java/ArithmeticExceptionTest.java

File renamed without changes.

‎jbmc/regression/jbmc/ArithmeticException4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
ArithmeticExceptionTest
3-
--throw-runtime-exceptions
3+
--throw-runtime-exceptions -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$

‎jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.class

-639 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArithmeticException5/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.ArithmeticException5</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/ArithmeticException5/ArithmeticExceptionTest.java ‎jbmc/regression/jbmc/ArithmeticException5/src/main/java/ArithmeticExceptionTest.java

File renamed without changes.

‎jbmc/regression/jbmc/ArithmeticException5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
ArithmeticExceptionTest
3-
--throw-runtime-exceptions
3+
--throw-runtime-exceptions -cp target/classes
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL

‎jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.class

-605 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArithmeticException6/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.ArithmeticException6</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/ArithmeticException6/ArithmeticExceptionTest.java ‎jbmc/regression/jbmc/ArithmeticException6/src/main/java/ArithmeticExceptionTest.java

File renamed without changes.

‎jbmc/regression/jbmc/ArithmeticException6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
ArithmeticExceptionTest
3-
--throw-runtime-exceptions --function ArithmeticExceptionTest.main
3+
--throw-runtime-exceptions --function ArithmeticExceptionTest.main -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$

‎jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.class

-619 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.class

-232 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.class

-219 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArithmeticException7/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.ArithmeticException7</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/ArithmeticException7/ArithmeticExceptionTest.java ‎jbmc/regression/jbmc/ArithmeticException7/src/main/java/ArithmeticExceptionTest.java

File renamed without changes.

‎jbmc/regression/jbmc/ArithmeticException7/java/lang/ArithmeticException.java ‎jbmc/regression/jbmc/ArithmeticException7/src/main/java/java/lang/ArithmeticException.java

File renamed without changes.

‎jbmc/regression/jbmc/ArithmeticException7/java/lang/RuntimeException.java ‎jbmc/regression/jbmc/ArithmeticException7/src/main/java/java/lang/RuntimeException.java

File renamed without changes.

‎jbmc/regression/jbmc/ArithmeticException7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
ArithmeticExceptionTest
3-
--throw-runtime-exceptions
3+
--throw-runtime-exceptions -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class

-875 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.ArrayIndexOutOfBoundsException1</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java ‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java

File renamed without changes.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
ArrayIndexOutOfBoundsExceptionTest
3-
--throw-runtime-exceptions
3+
--throw-runtime-exceptions -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class

-875 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.ArrayIndexOutOfBoundsException2</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.java ‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java

File renamed without changes.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
ArrayIndexOutOfBoundsExceptionTest
3-
--throw-runtime-exceptions
3+
--throw-runtime-exceptions -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class

-642 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class

-263 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class

-244 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class

-219 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.ArrayIndexOutOfBoundsException3</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java ‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/ArrayIndexOutOfBoundsExceptionTest.java

File renamed without changes.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java ‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/ArrayIndexOutOfBoundsException.java

File renamed without changes.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java ‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/IndexOutOfBoundsException.java

File renamed without changes.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.java ‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/src/main/java/java/lang/RuntimeException.java

File renamed without changes.

‎jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
ArrayIndexOutOfBoundsExceptionTest
3-
--throw-runtime-exceptions
3+
--throw-runtime-exceptions -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

‎jbmc/regression/jbmc/aastore_aaload1/A.class

-229 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.class

-626 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/aastore_aaload1/pom.xml

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression.jbmc.aastore_aaload1</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<parent>
11+
<groupId>org.cprover.regression</groupId>
12+
<artifactId>regression.jbmc</artifactId>
13+
<version>1.0-SNAPSHOT</version>
14+
</parent>
15+
16+
<build>
17+
<plugins>
18+
<plugin>
19+
<artifactId>maven-jar-plugin</artifactId>
20+
<executions>
21+
<execution>
22+
<id>default-jar</id>
23+
<phase>none</phase>
24+
</execution>
25+
</executions>
26+
</plugin>
27+
</plugins>
28+
</build>
29+
30+
</project>

‎jbmc/regression/jbmc/aastore_aaload1/aastore_aaload1.java ‎jbmc/regression/jbmc/aastore_aaload1/src/main/java/aastore_aaload1.java

File renamed without changes.

‎jbmc/regression/jbmc/aastore_aaload1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
aastore_aaload1
3-
3+
-cp target/classes
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎jbmc/regression/jbmc/address_space_size_limit1/Test.class

-640 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)