File tree 4 files changed +2
-11
lines changed
jbmc/regression/jbmc/exception-cleanup
nondet_elements_longer_lists
nondet_elements_longer_lists_global
4 files changed +2
-11
lines changed Original file line number Diff line number Diff line change @@ -4,11 +4,8 @@ Test.class
4
4
^EXIT=0$
5
5
^SIGNAL=0$
6
6
^VERIFICATION SUCCESSFUL$
7
- 1 remaining after simplification$
7
+ 0 remaining after simplification$
8
8
--
9
9
^warning: ignoring
10
10
--
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.
Original file line number Diff line number Diff line change @@ -3,8 +3,6 @@ Test.class
3
3
--function Test.main --show-vcc
4
4
^EXIT=0$
5
5
^SIGNAL=0$
6
- file Test\.java line 6 function java::Test.main:\(I\)V
7
- no uncaught exception
8
6
--
9
7
file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5
10
8
assertion at file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5
Original file line number Diff line number Diff line change 1
1
CORE
2
2
main.c
3
3
--harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function
4
- \[test_function.unwind.\d+\] line \d+ unwinding assertion loop 0: SUCCESS
5
- \[test_function.unwind.\d+\] line \d+ unwinding assertion loop 1: SUCCESS
6
4
\[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS
7
5
^EXIT=0$
8
6
^SIGNAL=0$
Original file line number Diff line number Diff line change 1
1
CORE
2
2
main.c
3
3
--harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function --nondet-globals
4
- \[test_function.unwind.\d+\] line \d+ unwinding assertion loop 0: SUCCESS
5
- \[test_function.unwind.\d+\] line \d+ unwinding assertion loop 1: SUCCESS
6
4
\[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS
7
5
^EXIT=0$
8
6
^SIGNAL=0$
You can’t perform that action at this time.
0 commit comments