Compile jbmc/class-literals test sources

Add pom.xml for compilation, move sources, remove obsolete pre-compiled class files.
diffblue · Jan 5, 2025 · 2cd16d8 · 2cd16d8
1 parent 678ee8f
commit 2cd16d8
Show file tree

Hide file tree

Showing 20 changed files with 47 additions and 26 deletions.
diff --git a/jbmc/regression/jbmc/class-literals/ExampleAnnotation.class b/jbmc/regression/jbmc/class-literals/ExampleAnnotation.class
diff --git a/jbmc/regression/jbmc/class-literals/ExampleEnum.class b/jbmc/regression/jbmc/class-literals/ExampleEnum.class
diff --git a/jbmc/regression/jbmc/class-literals/ExampleInterface.class b/jbmc/regression/jbmc/class-literals/ExampleInterface.class
diff --git a/jbmc/regression/jbmc/class-literals/ExampleSynthetic.class b/jbmc/regression/jbmc/class-literals/ExampleSynthetic.class
diff --git a/jbmc/regression/jbmc/class-literals/Test.class b/jbmc/regression/jbmc/class-literals/Test.class
diff --git a/jbmc/regression/jbmc/class-literals/java/lang/Class.class b/jbmc/regression/jbmc/class-literals/java/lang/Class.class
diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/CProver.class b/jbmc/regression/jbmc/class-literals/org/cprover/CProver.class
diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/CProver.java b/jbmc/regression/jbmc/class-literals/org/cprover/CProver.java
diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.class b/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.class
diff --git a/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.java b/jbmc/regression/jbmc/class-literals/org/cprover/MustNotThrow.java
diff --git a/jbmc/regression/jbmc/class-literals/pom.xml b/jbmc/regression/jbmc/class-literals/pom.xml
@@ -0,0 +1,41 @@
+<?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.class-literals</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <dependencies>
+        <dependency>
+            <groupId>org.cprover.util</groupId>
+            <artifactId>cprover-api</artifactId>
+        </dependency>
+    </dependencies>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+            <plugin>
+                <groupId>com.github.abextm</groupId>
+                <artifactId>jasmin-maven-plugin</artifactId>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...bmc/class-literals/ExampleAnnotation.java → ...rals/src/main/java/ExampleAnnotation.java b/...bmc/class-literals/ExampleAnnotation.java → ...rals/src/main/java/ExampleAnnotation.java
diff --git a/...sion/jbmc/class-literals/ExampleEnum.java → ...s-literals/src/main/java/ExampleEnum.java b/...sion/jbmc/class-literals/ExampleEnum.java → ...s-literals/src/main/java/ExampleEnum.java
diff --git a/...jbmc/class-literals/ExampleInterface.java → ...erals/src/main/java/ExampleInterface.java b/...jbmc/class-literals/ExampleInterface.java → ...erals/src/main/java/ExampleInterface.java
diff --git a/...on/jbmc/class-literals/ExampleSynthetic.j → ...literals/src/main/java/ExampleSynthetic.j b/...on/jbmc/class-literals/ExampleSynthetic.j → ...literals/src/main/java/ExampleSynthetic.j
diff --git a/.../regression/jbmc/class-literals/Test.java → ...mc/class-literals/src/main/java/Test.java b/.../regression/jbmc/class-literals/Test.java → ...mc/class-literals/src/main/java/Test.java
diff --git a/.../jbmc/class-literals/java/lang/Class.java → ...terals/src/main/java/java/lang/Class.java b/.../jbmc/class-literals/java/lang/Class.java → ...terals/src/main/java/java/lang/Class.java
@@ -1,6 +1,6 @@
 package java.lang;
 
-public class Class {
+public class Class <T> {
 
   private String name;
 
@@ -43,4 +43,6 @@ public void cproverInitializeClassLiteral(
   public boolean isLocalClass() { return isLocalClass; }
   public boolean isMemberClass() { return isMemberClass; }
   public boolean isEnum() { return isEnum; }
+
+  public boolean desiredAssertionStatus() { return true; }
 }
diff --git a/jbmc/regression/jbmc/class-literals/test.desc b/jbmc/regression/jbmc/class-literals/test.desc
@@ -1,6 +1,6 @@
 CORE bdd-expected-timeout
 Test
---function Test.main
+--function Test.main -cp target/classes
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

diff --git a/jbmc/regression/jbmc/class-literals/test_lazy.desc b/jbmc/regression/jbmc/class-literals/test_lazy.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.main
+--function Test.main -cp target/classes
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml
@@ -68,6 +68,7 @@
         <module>catch1</module>
         <module>char1</module>
         <module>class-fields</module>
+        <module>class-literals</module>
         <module>classpath-jar-load-whole-jar</module>
     </modules>