forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
13 changed files
with
345 additions
and
0 deletions.
There are no files selected for viewing
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,15 @@ | ||
int a; | ||
|
||
void main(void) | ||
{ | ||
int i = 0; | ||
|
||
if(i < 10) | ||
{ | ||
a = 1; | ||
} | ||
else | ||
{ | ||
a = 2; | ||
} | ||
} |
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,39 @@ | ||
CORE | ||
main.c | ||
--dependence-graph --show | ||
activate-multi-line-match | ||
EXIT=0 | ||
SIGNAL=0 | ||
// First assignment has a control dependency on the if | ||
\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 | ||
// Second assignment has a control dependency on the if | ||
\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 | ||
-- | ||
^warning: ignoring | ||
-- | ||
The first regex above matches output portions like shown below (with <N> being a | ||
location number). The intention is to check whether the assignment has a control | ||
dependency on the goto statement. | ||
|
||
// <N> file main.c line 7 function main | ||
IF !(i < 10) THEN GOTO 1 | ||
|
||
**** 3 file main.c line 9 function main | ||
Control dependencies: <N> | ||
|
||
// 3 file main.c line 9 function main | ||
a = 1; | ||
|
||
The second regex above matches output portions like shown below (with <N> being | ||
a location number). The intention is to check whether the assignment has a | ||
control dependency on the goto statement. | ||
|
||
// <N> file main.c line 7 function main | ||
IF !(i < 10) THEN GOTO 1 | ||
... | ||
**** 5 file main.c line 13 function main | ||
Control dependencies: <N> | ||
|
||
// 5 file main.c line 13 function main | ||
1: a = 2; | ||
|
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,15 @@ | ||
int a; | ||
|
||
void func() | ||
{ | ||
} | ||
|
||
void main(void) | ||
{ | ||
func(); | ||
|
||
if(a < 10) | ||
{ | ||
a = 1; | ||
} | ||
} |
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,23 @@ | ||
CORE | ||
main.c | ||
--dependence-graph --show | ||
activate-multi-line-match | ||
EXIT=0 | ||
SIGNAL=0 | ||
// Assignment has a control dependency on the if | ||
\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 | ||
-- | ||
^warning: ignoring | ||
-- | ||
The regex above match output portions like shown below (with <N> being a | ||
location number). The intention is to check whether the assignment has a control | ||
dependency on the goto statement. | ||
|
||
// <N> file main.c line 7 function main | ||
IF !(i < 10) THEN GOTO 1 | ||
... | ||
**** 3 file main.c line 9 function main | ||
Control dependencies: <N> | ||
|
||
// 3 file main.c line 9 function main | ||
a = 1; |
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,21 @@ | ||
int a; | ||
|
||
void func() | ||
{ | ||
} | ||
|
||
void main(void) | ||
{ | ||
if(a < 7) | ||
{ | ||
goto L; | ||
} | ||
|
||
if(a < 10) | ||
{ | ||
func(); | ||
L: | ||
a = 1; | ||
a = 2; | ||
} | ||
} |
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,38 @@ | ||
CORE | ||
main.c | ||
--dependence-graph --show | ||
activate-multi-line-match | ||
EXIT=0 | ||
SIGNAL=0 | ||
// Assignment has a control dependency on the first if | ||
\/\/ ([0-9]+).*\n.*IF.*a < 7.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2 | ||
// Assignment has a control dependency on the second if | ||
\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2 | ||
-- | ||
^warning: ignoring | ||
-- | ||
The first regex above matches output portions like shown below (with <N> being a | ||
location number). The intention is to check whether the assignment has a control | ||
dependency on the goto statement. | ||
|
||
// <N> file main.c line 9 function main | ||
IF a < 7 THEN GOTO 1 | ||
... | ||
**** 6 file main.c line 19 function main | ||
Control dependencies: (<N>,...)|(...,<N>) | ||
|
||
// 6 file main.c line 19 function main | ||
a = 2; | ||
|
||
The second regex above matches output portions like shown below (with <N> being | ||
a location number). The intention is to check whether the assignment has a | ||
control dependency on the goto statement. | ||
|
||
// <N> file main.c line 14 function main | ||
IF !(a < 10) THEN GOTO 2 | ||
... | ||
**** 6 file main.c line 19 function main | ||
Control dependencies: (<N>,...)|(...,<N>) | ||
|
||
// 6 file main.c line 19 function main | ||
a = 2; |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
int a; | ||
|
||
void main(void) | ||
{ | ||
int i = 0; | ||
while(i < 10) | ||
{ | ||
a = 1; | ||
} | ||
} |
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,50 @@ | ||
CORE | ||
main.c | ||
--dependence-graph --show | ||
activate-multi-line-match | ||
EXIT=0 | ||
SIGNAL=0 | ||
// Assignment has a control dependency on the loop head | ||
\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 | ||
// Backedge has a control dependency on the loop head | ||
\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}\s*GOTO [0-9]+ | ||
// Loop head has a control dependency on itself | ||
Control dependencies: ([0-9]+)\n(.*\n)?\n.*\/\/ \1.*\n.*IF.*i < 10.*THEN | ||
-- | ||
^warning: ignoring | ||
-- | ||
The first regex above match output portions like shown below (with <N> being a | ||
location number). The intention is to check whether the assignment has a control | ||
dependency on the loop head. | ||
|
||
// <N> file main.c line 6 function main | ||
1: IF !(i < 10) THEN GOTO 2 | ||
... | ||
**** 3 file main.c line 8 function main | ||
Control dependencies: <N> | ||
|
||
// 3 file main.c line 8 function main | ||
a = 1; | ||
|
||
The second regex above match output portions like shown below (with <N> being a | ||
location number). The intention is to check whether the backwards goto has a | ||
control dependency on the loop head. | ||
|
||
// <N> file main.c line 6 function main | ||
1: IF !(i < 10) THEN GOTO 2 | ||
... | ||
**** 4 file main.c line 6 function main | ||
Control dependencies: <N> | ||
|
||
// 4 file main.c line 6 function main | ||
GOTO 1 | ||
|
||
The third regex above match output portions like shown below (with <N> being a | ||
location number). The intention is to check whether the loop head has a control | ||
dependency on itself. | ||
|
||
Control dependencies: <N> | ||
Data dependencies: 1 | ||
|
||
// <N> file main.c line 6 function main | ||
1: IF !(i < 10) THEN GOTO 2 |
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 @@ | ||
int a; | ||
|
||
void main(void) | ||
{ | ||
int i = 0; | ||
while(i < 10) | ||
{ | ||
if(i < 7) | ||
{ | ||
a = 1; | ||
} | ||
} | ||
} |
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,54 @@ | ||
CORE | ||
main.c | ||
--dependence-graph --show | ||
activate-multi-line-match | ||
EXIT=0 | ||
SIGNAL=0 | ||
// Assignment has a control dependency on the if | ||
\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 | ||
// If has a control dependency on the loop head | ||
\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*i < 7 | ||
-- | ||
^warning: ignoring | ||
// Assignment does not have a control dependency on the loop head | ||
\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1 | ||
-- | ||
The first regex above matches output portions like shown below (with <N> being a | ||
location number). The intention is to check whether the assignment has a control | ||
dependency on the if. | ||
|
||
// <N> file main.c line 6 function main | ||
1: IF !(i < 7) THEN GOTO 2 | ||
... | ||
**** 3 file main.c line 8 function main | ||
Control dependencies: <N> | ||
|
||
// 3 file main.c line 8 function main | ||
a = 1; | ||
|
||
The second regex above matches output portions like shown below (with <N> being | ||
a location number). The intention is to check whether the if has a control | ||
dependency on the loop head. | ||
|
||
// <N> file main.c line 6 function main | ||
1: IF !(i < 10) THEN GOTO 3 | ||
|
||
**** 3 file main.c line 8 function main | ||
Control dependencies: <N> | ||
Data dependencies: 1 | ||
|
||
// 3 file main.c line 8 function main | ||
IF !(i < 7) THEN GOTO 2 | ||
|
||
The third regex above matches output portions like shown below (with <N> being a | ||
location number). The intention is to check that the assignment does not have a | ||
control dependency on the loop head. | ||
|
||
// <N> file main.c line 6 function main | ||
1: IF !(i < 10) THEN GOTO 3 | ||
... | ||
**** 4 file main.c line 10 function main | ||
Control dependencies: <N> | ||
|
||
// 4 file main.c line 10 function main | ||
a = 1; |
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,16 @@ | ||
int a; | ||
|
||
void main(void) | ||
{ | ||
int i = 0; | ||
|
||
if(i < 10) | ||
{ | ||
if(i < 7) | ||
{ | ||
a = 1; | ||
} | ||
|
||
a = 2; | ||
} | ||
} |
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,38 @@ | ||
CORE | ||
main.c | ||
--dependence-graph --show | ||
activate-multi-line-match | ||
EXIT=0 | ||
SIGNAL=0 | ||
// Second assignment has a control dependency on the outer if | ||
\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 | ||
-- | ||
^warning: ignoring | ||
// Second assignment does not have a control dependency on the inner if | ||
\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2 | ||
-- | ||
The first regex above matches output portions like shown below (with <N> being a | ||
location number). The intention is to check whether the assignment has a control | ||
dependency on the outer if. | ||
|
||
// <N> file main.c line 7 function main | ||
IF !(i < 10) THEN GOTO 2 | ||
... | ||
**** 6 file main.c line 14 function main | ||
Control dependencies: <N> | ||
|
||
// 6 file main.c line 14 function main | ||
a = 2; | ||
|
||
The second regex above matches output portions like shown below (with <N> being | ||
a location number). The intention is to check that the assignment does not have | ||
a control dependency on the inner if. | ||
|
||
// <N> file main.c line 9 function main | ||
IF !(i < 7) THEN GOTO 1 | ||
... | ||
**** 6 file main.c line 14 function main | ||
Control dependencies: <N> | ||
|
||
// 6 file main.c line 14 function main | ||
a = 2; |