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
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.
You can’t perform that action at this time.
0 commit comments