File tree 6 files changed +26
-26
lines changed
jbmc/regression/jbmc/reachability-slice
regression/cbmc/reachability-slice
6 files changed +26
-26
lines changed Original file line number Diff line number Diff line change 1
1
CORE symex-driven-lazy-loading-expected-failure
2
2
A.class
3
3
--reachability-slice --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
4
- 1001
4
+ = \(int\)\(short\) 1001
5
5
--
6
- 1003
7
- 1004
8
- 1005
6
+ = \(int\)\(short\) 1003
7
+ = \(int\)\(short\) 1004
8
+ = \(int\)\(short\) 1005
9
9
--
10
10
Note: 1002 might and might not be removed, based on where the assertion for coverage resides.
11
11
At the time of writing of this test, 1002 is removed.
Original file line number Diff line number Diff line change 1
1
CORE symex-driven-lazy-loading-expected-failure
2
2
A.class
3
3
--reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.4' --cover location
4
- 1001
5
- 1002
6
- 1003
7
- 1005
4
+ = \(int\)\(short\) 1001
5
+ = \(int\)\(short\) 1002
6
+ = \(int\)\(short\) 1003
7
+ = \(int\)\(short\) 1005
8
8
--
9
- 1004
9
+ = \(int\)\(short\) 1004
10
10
--
11
11
Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
Original file line number Diff line number Diff line change 1
1
CORE symex-driven-lazy-loading-expected-failure
2
2
A.class
3
3
--reachability-slice --show-goto-functions --cover location
4
- 1001
5
- 1002
6
- 1003
7
- 1004
8
- 1005
4
+ = \(int\)\(short\) 1001
5
+ = \(int\)\(short\) 1002
6
+ = \(int\)\(short\) 1003
7
+ = \(int\)\(short\) 1004
8
+ = \(int\)\(short\) 1005
9
9
--
10
10
--
11
11
Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
Original file line number Diff line number Diff line change 1
1
CORE
2
2
test.c
3
3
--reachability-slice --show-goto-functions --cover location --property foo.coverage.2
4
- 1001
4
+ = 1001
5
5
--
6
- 1004
7
- 1005
6
+ = 1004
7
+ = 1005
8
8
--
9
9
We do not include 1002 and 1003, whether this is hit depends on where assertion is put
Original file line number Diff line number Diff line change 1
1
CORE
2
2
test.c
3
3
--reachability-slice-fb --show-goto-functions --cover location --property foo.coverage.2
4
- 1001
5
- 1002
6
- 1003
7
- 1005
4
+ = 1001
5
+ = 1002
6
+ = 1003
7
+ = 1005
8
8
--
9
- 1004
9
+ = 1004
Original file line number Diff line number Diff line change 1
1
CORE
2
2
test.c
3
3
--reachability-slice --show-goto-functions --cover location
4
- 1001
5
- 1002
6
- 1003
7
- 1004
4
+ = 1001
5
+ = 1002
6
+ = 1003
7
+ = 1004
8
8
--
9
9
--
10
10
We do not include 1005 since it might or might not be present based on where the assertion is in the block.
You can’t perform that action at this time.
0 commit comments