-
Notifications
You must be signed in to change notification settings - Fork 262
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Maintain loop invariant annotation when converting do .. while
With the changes in bbd9de4 we newly made do .. while converted instructions subject to `optimize_guarded_gotos`, which previously rewrote conditions without retaining annotations related to loop invariants. The included tests now show that the annotations are preserved, but still fail for an unrelated bug in how do .. while loops are instrumented.
- Loading branch information
1 parent
89a0470
commit 2bc9b22
Showing
8 changed files
with
84 additions
and
5 deletions.
There are no files selected for viewing
19 changes: 19 additions & 0 deletions
19
regression/contracts-dfcc/loop_contracts_do_while/assigns.c
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,19 @@ | ||
int global; | ||
|
||
int main() | ||
{ | ||
global = 0; | ||
int argc = 1; | ||
if(argc > 1) | ||
{ | ||
do | ||
__CPROVER_assigns(global) | ||
{ | ||
global = 1; | ||
} | ||
while(0); | ||
} | ||
__CPROVER_assert(global == 0, "should be zero"); | ||
|
||
return 0; | ||
} |
9 changes: 9 additions & 0 deletions
9
regression/contracts-dfcc/loop_contracts_do_while/assigns.desc
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 @@ | ||
KNOWNBUG | ||
assigns.c | ||
--dfcc main --apply-loop-contracts | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- | ||
-- | ||
This test checks that loop contracts work correctly on do/while loops. |
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
24 changes: 24 additions & 0 deletions
24
regression/contracts-dfcc/loop_contracts_do_while/side_effect.c
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,24 @@ | ||
int global; | ||
|
||
int foo() | ||
{ | ||
return 0; | ||
} | ||
|
||
int main() | ||
{ | ||
global = 0; | ||
int argc = 1; | ||
if(argc > 1) | ||
{ | ||
do | ||
__CPROVER_assigns(global) | ||
{ | ||
global = 1; | ||
} | ||
while(foo()); | ||
} | ||
__CPROVER_assert(global == 0, "should be zero"); | ||
|
||
return 0; | ||
} |
9 changes: 9 additions & 0 deletions
9
regression/contracts-dfcc/loop_contracts_do_while/side_effect.desc
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 @@ | ||
KNOWNBUG | ||
side_effect.c | ||
--dfcc main --apply-loop-contracts | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- | ||
-- | ||
This test checks that loop contracts work correctly on do/while loops. |
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 |
---|---|---|
@@ -1,4 +1,4 @@ | ||
KNOWNBUG | ||
CORE dfcc-only | ||
main.c | ||
--dfcc main --apply-loop-contracts | ||
^EXIT=0$ | ||
|
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