Skip to content

Commit de57bb9

Browse files
committed
fix expected outcome of two tests
1 parent cf40a77 commit de57bb9

File tree

2 files changed

+5
-5
lines changed

2 files changed

+5
-5
lines changed

jbmc/regression/jbmc/generic_class_bound1/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ Gn.class
33
--cover location
44
^EXIT=0$
55
^SIGNAL=0$
6-
.*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block 1: FAILED
7-
.*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block 1: FAILED
8-
.*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block 2: FAILED
9-
.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 2: SATISFIED
6+
.*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block .: FAILED
7+
.*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block .: FAILED
8+
.*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block .: FAILED
9+
.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block .: SATISFIED
1010
--
1111
--
1212
This fails under symex-driven lazy loading because the FAILED blocks occur in functions that are unreachable

jbmc/regression/jbmc/reachability-slice/test2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
A.class
3-
--reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
3+
--reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.4' --cover location
44
1001
55
1002
66
1003

0 commit comments

Comments
 (0)