Skip to content

Commit 3308bff

Browse files
Compile jbmc/class-literals test sources
Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files.
1 parent 9687748 commit 3308bff

20 files changed

+47
-26
lines changed
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
-1.61 KB
Binary file not shown.
Binary file not shown.
Binary file not shown.

jbmc/regression/jbmc/class-literals/org/cprover/CProver.java

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

jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.java

-8
This file was deleted.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
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-literals</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+
<plugin>
35+
<groupId>com.github.abextm</groupId>
36+
<artifactId>jasmin-maven-plugin</artifactId>
37+
</plugin>
38+
</plugins>
39+
</build>
40+
41+
</project>

jbmc/regression/jbmc/class-literals/java/lang/Class.java jbmc/regression/jbmc/class-literals/src/main/java/java/lang/Class.java

+3-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
package java.lang;
22

3-
public class Class {
3+
public class Class <T> {
44

55
private String name;
66

@@ -43,4 +43,6 @@ public void cproverInitializeClassLiteral(
4343
public boolean isLocalClass() { return isLocalClass; }
4444
public boolean isMemberClass() { return isMemberClass; }
4545
public boolean isEnum() { return isEnum; }
46+
47+
public boolean desiredAssertionStatus() { return true; }
4648
}

jbmc/regression/jbmc/class-literals/test.desc

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

jbmc/regression/jbmc/class-literals/test_lazy.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--function Test.main
3+
--function Test.main -cp target/classes
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc/pom.xml

+1
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,7 @@
6868
<module>catch1</module>
6969
<module>char1</module>
7070
<module>class-fields</module>
71+
<module>class-literals</module>
7172
<module>classpath-jar-load-whole-jar</module>
7273
</modules>
7374

0 commit comments

Comments
 (0)