-
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.
CONTRACTS: redirect checks to outer write set for loops that get skipped
A couple of KOWNBUG tests with do-while loops are now working.
- Loading branch information
Remi Delmas
committed
Aug 20, 2024
1 parent
3877e0f
commit c065a20
Showing
9 changed files
with
85 additions
and
10 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
4 changes: 2 additions & 2 deletions
4
regression/contracts-dfcc/loop_contracts_do_while/nested.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 |
---|---|---|
@@ -1,9 +1,9 @@ | ||
KNOWNBUG | ||
CORE | ||
nested.c | ||
--dfcc main --apply-loop-contracts | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- | ||
-- | ||
We spuriously report that x is not assignable. | ||
We properly skip the instrumentation of both 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 | ||
main.c | ||
--dfcc main --apply-loop-contracts | ||
^EXIT=0$ | ||
|
7 changes: 4 additions & 3 deletions
7
regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.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 |
---|---|---|
@@ -1,10 +1,11 @@ | ||
CORE dfcc-only | ||
main.c | ||
--dfcc main --apply-loop-contracts | ||
^EXIT=10$ | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- | ||
^Found loop with more than one latch instruction$ | ||
-- | ||
This test checks that our loop contract instrumentation first transforms loops | ||
so as to only have a single loop latch. | ||
so as to only have a single loop latch, and skips instrumentation if the result | ||
has no contract. |
29 changes: 29 additions & 0 deletions
29
regression/contracts-dfcc/skip_loop_instrumentation/main.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,29 @@ | ||
int global; | ||
|
||
int main() | ||
{ | ||
global = 0; | ||
int argc = 1; | ||
do | ||
{ | ||
int local; | ||
global = 1; | ||
local = 1; | ||
for(int i = 0; i < 1; i++) | ||
{ | ||
local = 1; | ||
global = 2; | ||
int j = 0; | ||
while(j < 1) | ||
{ | ||
local = 1; | ||
global = 3; | ||
j++; | ||
} | ||
__CPROVER_assert(global == 3, "case3"); | ||
} | ||
__CPROVER_assert(global == 3, "case3"); | ||
} while(0); | ||
__CPROVER_assert(global == 3, "case1"); | ||
return 0; | ||
} |
11 changes: 11 additions & 0 deletions
11
regression/contracts-dfcc/skip_loop_instrumentation/test.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,11 @@ | ||
CORE | ||
main.c | ||
--dfcc main --apply-loop-contracts | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- | ||
^warning: ignoring | ||
-- | ||
This test case checks that when the instrumentation of nested loops is skipped, we redirect the write set checks to the | ||
outer write set. |
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