forked from diffblue/cbmc
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Add forwards reachability to the slicer, in addition to the backwards reachability currently implemented. * Add command-line options for the slicer in jbmc and cbmc. * Refactor the way reachability is computed in the slicer, using grapht rather than own implementation
- Loading branch information
Vojtech Forejt
committed
Mar 22, 2018
1 parent
7161f17
commit 6120c17
Showing
19 changed files
with
299 additions
and
38 deletions.
There are no files selected for viewing
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
public class A { | ||
|
||
public void foo(int i ) { | ||
// We use integer constants that we grep for later in a goto program. | ||
int x = 1001 + i; | ||
if (i > 0) { | ||
x = 1002 + i; // property "java::A.foo:(I)V.coverage.3", see https://github.com/diffblue/cbmc/pull/1943#discussion_r175367063 for a discusison. | ||
x = 1003 + i; | ||
} | ||
else | ||
x = 1004 + i; | ||
x = 1005 + i; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
CORE | ||
A.class | ||
--reachability-slice --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location | ||
1001 | ||
-- | ||
1003 | ||
1004 | ||
1005 | ||
-- | ||
Note: 1002 might and might not be removed, based on where the assertion for coverage resides. | ||
At the time of writing of this test, 1002 is removed. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
CORE | ||
A.class | ||
--reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location | ||
1001 | ||
1002 | ||
1003 | ||
1005 | ||
-- | ||
1004 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
CORE | ||
A.class | ||
--reachability-slice --show-goto-functions --cover location | ||
1001 | ||
1002 | ||
1003 | ||
1004 | ||
1005 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
void foo(int i) | ||
{ | ||
// We use integer constants that we grep for later in a goto program. | ||
int x = 1001 + i; | ||
if(i > 0) | ||
{ //foo.coverage.2 | ||
x = 1002 + i; | ||
x = 1003 + i; | ||
} | ||
else | ||
x = 1004 + i; | ||
x = 1005 + i; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
CORE | ||
test.c | ||
--reachability-slice --show-goto-functions --cover location --property foo.coverage.2 | ||
1001 | ||
-- | ||
1004 | ||
1005 | ||
-- | ||
We do not include 1002 and 1003, whether this is hit depends on where assertion is put |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
CORE | ||
test.c | ||
--reachability-slice-fb --show-goto-functions --cover location --property foo.coverage.2 | ||
1001 | ||
1002 | ||
1003 | ||
1005 | ||
-- | ||
1004 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE | ||
test.c | ||
--reachability-slice --show-goto-functions --cover location | ||
1001 | ||
1002 | ||
1003 | ||
1004 | ||
-- | ||
-- | ||
We do not include 1005 since it might or might not be present based on where the assertion is in the block. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.