File: test.desc

package info (click to toggle)
cbmc 5.12-5
  • links: PTS
  • area: main
  • in suites: bullseye
  • size: 92,512 kB
  • sloc: cpp: 301,761; ansic: 51,699; java: 27,534; python: 5,113; yacc: 4,756; makefile: 3,184; lex: 2,749; sh: 1,347; perl: 555; xml: 404; pascal: 203; ada: 36
file content (13 lines) | stat: -rw-r--r-- 481 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
 
KNOWNBUG
Sync
--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
Note: requires jasmin to compile the bytecode instructions
This checks that an extra monitorexit will always trigger an IllegalMonitorException.

This is currently not working as explicit throws have been removed from the underlying model due to performance considerations.