Skip to content

Commit 0ce8dbc

Browse files
Compile jbmc/class-fields test sources
Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files. Add missing desiredAssertionStatus method to local java.lang.Class model.
1 parent cd70977 commit 0ce8dbc

File tree

11 files changed

+42
-24
lines changed

11 files changed

+42
-24
lines changed

Diff for: jbmc/regression/jbmc/class-fields/Test.class

-598 Bytes
Binary file not shown.
-559 Bytes
Binary file not shown.
-536 Bytes
Binary file not shown.

Diff for: jbmc/regression/jbmc/class-fields/org/cprover/CProver.java

-15
This file was deleted.
-156 Bytes
Binary file not shown.

Diff for: jbmc/regression/jbmc/class-fields/org/cprover/MustNotThrow.java

-8
This file was deleted.

Diff for: jbmc/regression/jbmc/class-fields/pom.xml

+37
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
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.class-fields</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+
<dependencies>
17+
<dependency>
18+
<groupId>org.cprover.util</groupId>
19+
<artifactId>cprover-api</artifactId>
20+
</dependency>
21+
</dependencies>
22+
23+
<build>
24+
<plugins>
25+
<plugin>
26+
<artifactId>maven-jar-plugin</artifactId>
27+
<executions>
28+
<execution>
29+
<id>default-jar</id>
30+
<phase>none</phase>
31+
</execution>
32+
</executions>
33+
</plugin>
34+
</plugins>
35+
</build>
36+
37+
</project>

Diff for: jbmc/regression/jbmc/class-fields/java/lang/Class.java renamed to jbmc/regression/jbmc/class-fields/src/main/java/java/lang/Class.java

+3
Original file line numberDiff line numberDiff line change
@@ -9,4 +9,7 @@ protected void cproverNondetInitialize() {
99
org.cprover.CProver.assume(field == null);
1010
}
1111

12+
public boolean desiredAssertionStatus() {
13+
return true;
14+
}
1215
}

Diff for: jbmc/regression/jbmc/class-fields/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Test
3-
--function Test.main
3+
--function Test.main -cp target/classes
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

Diff for: jbmc/regression/jbmc/pom.xml

+1
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,7 @@
6767
<module>cast_null2</module>
6868
<module>catch1</module>
6969
<module>char1</module>
70+
<module>class-fields</module>
7071
<module>classpath-jar-load-whole-jar</module>
7172
</modules>
7273

0 commit comments

Comments
 (0)