File tree Expand file tree Collapse file tree 1 file changed +7
-2
lines changed
jbmc/regression/jbmc/coreModels Expand file tree Collapse file tree 1 file changed +7
-2
lines changed Original file line number Diff line number Diff line change @@ -3,7 +3,12 @@ test.class
3
3
--show-symbol-table --cp ../../../src/java_bytecode/library/core-models.jar:.
4
4
^EXIT=0$
5
5
^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:\(
7
9
--
10
+ ^failed to load class .org.cprover.CProver.$
8
11
--
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.
You can’t perform that action at this time.
0 commit comments