Skip to content

Commit e52abcb

Browse files
committed
JBMC: Fix failing regression test
A recent modification to https://github.com/diffblue/java-models-library has made the CProver class to lose its class initializer, which resulted in a failing regression test here.
1 parent 1ae3c6b commit e52abcb

File tree

1 file changed

+7
-2
lines changed

1 file changed

+7
-2
lines changed

jbmc/regression/jbmc/coreModels/test.desc

+7-2
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,12 @@ 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.*: java::org.cprover.CProver.assume:\(
7+
^Symbol.*: java::org.cprover.CProver.nondetInt:\(
8+
^Symbol.*: java::org.cprover.CProver.nondetChar:\(
79
--
10+
^failed to load class .org.cprover.CProver.$
811
--
9-
tests that the core models are being loaded by checking if the static initializer for the CProver class was
12+
This checks that the core models are being loaded. We check that methods
13+
assume(), nodetInt(), and nondetChar() are defined in class org.cprover.CProver
14+
and that JBMC does not complain while trying to load the that class.

0 commit comments

Comments
 (0)