Skip to content

Commit 0cf8fbf

Browse files
Fix core models test
org.cprover.* methods are not part of the core models and are therefore not necessarily on the classpath. Therefore the test should test for the presence of another class that will always be part of the core models.
1 parent d3a2d2d commit 0cf8fbf

File tree

3 files changed

+4
-6
lines changed

3 files changed

+4
-6
lines changed
-269 Bytes
Binary file not shown.

jbmc/regression/jbmc/coreModels/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--show-symbol-table --cp ../../../src/java_bytecode/library/core-models.jar:.
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\<clinit\>\:\(\)V$
6+
^Symbol\s*\.*\: java\:\:java.lang.Throwable\.\<clinit\>\:\(\)V$
77
--
88
--
9-
tests that the core models are being loaded by checking if the static initializer for the CProver class was
9+
tests that the core models are being loaded by checking if the static initializer for the Throwable class was loaded
+2-4
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,8 @@
1-
import org.cprover.CProver;
21
class test
32
{
4-
public static void main(String[] args)
3+
public static void main(String[] args) throws Exception
54
{
6-
int i=CProver.nondetInt();
7-
assert(i!=0);
5+
throw new Exception();
86
}
97
}
108

0 commit comments

Comments
 (0)