Skip to content

Commit 13b6290

Browse files
Owensmowton
Owen
authored andcommitted
Update existing tests so they pass
1 parent e12d4ab commit 13b6290

File tree

2 files changed

+2
-7
lines changed

2 files changed

+2
-7
lines changed

jbmc/regression/jbmc/exception-cleanup/test.desc

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,8 @@ Test.class
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
7-
1 remaining after simplification$
7+
0 remaining after simplification$
88
--
99
^warning: ignoring
1010
--
11-
The function "unreachable" should be successfully noted as unreachable by symex,
12-
but the final uncaught-exception test in __CPROVER__start is not yet decidable
13-
in symex, as it requires symex to note that within a catch block
14-
@inflight_exception is definitely *not* null, which it can't just yet.
11+
The function "unreachable" should be successfully noted as unreachable by symex.

jbmc/regression/jbmc/exception-cleanup/vccs.desc

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@ Test.class
33
--function Test.main --show-vcc
44
^EXIT=0$
55
^SIGNAL=0$
6-
file Test\.java line 6 function java::Test.main:\(I\)V
7-
no uncaught exception
86
--
97
file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5
108
assertion at file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5

0 commit comments

Comments
 (0)