Skip to content

Commit 75a6311

Browse files
Modified the expected goto-program for cbmc-java/virtual7
The uncaught exceptions analysis is used to reduce the exception handling instrumentation and consequently the number of new labels and GOTOs
1 parent 4a44668 commit 75a6311

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

regression/cbmc-java/virtual7/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ test.class
33
--show-goto-functions
44
^EXIT=0$
55
^SIGNAL=0$
6-
IF "java::E".*THEN GOTO [67]
7-
IF "java::B".*THEN GOTO [67]
8-
IF "java::D".*THEN GOTO [67]
9-
IF "java::C".*THEN GOTO [67]
6+
IF "java::E".*THEN GOTO [12]
7+
IF "java::B".*THEN GOTO [12]
8+
IF "java::D".*THEN GOTO [12]
9+
IF "java::C".*THEN GOTO [12]
1010
--
1111
IF "java::A".*THEN GOTO

0 commit comments

Comments
 (0)