-
Notifications
You must be signed in to change notification settings - Fork 260
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #7761 from NlightNFotis/simplify_interval_domain
- Loading branch information
Showing
7 changed files
with
198 additions
and
21 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
18 changes: 18 additions & 0 deletions
18
regression/cbmc/simplify_singleton_interval_7690/negative_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,18 @@ | ||
CORE | ||
--trace | ||
singleton_interval_simp_neg.c | ||
^VERIFICATION FAILED$ | ||
^\[main\.assertion\.1\] line \d expected failure: paths where x is unbounded explored: FAILURE$ | ||
^\[main\.assertion\.2\] line \d+ expected failure: paths where 0 \<= x \<= 15 explored: FAILURE$ | ||
^\[main\.assertion\.3\] line \d+ expected success: paths where x \<= 15 explored: SUCCESS$ | ||
y=-6 \(11111111 11111111 11111111 11111010\) | ||
x=14 \(00000000 00000000 00000000 00001110\) | ||
y=34 \(00000000 00000000 00000000 00100010\) | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
-- | ||
-- | ||
This tests the negative case of the simplification of the singleton interval | ||
(i.e when the presented interval *is* the *not* the singleton interval - | ||
the set of possible values that the bounded variable can take has cardinality | ||
> 1). |
14 changes: 14 additions & 0 deletions
14
regression/cbmc/simplify_singleton_interval_7690/positive_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,14 @@ | ||
CORE | ||
--trace | ||
singleton_interval_simp.c | ||
^VERIFICATION FAILED$ | ||
^\[main\.assertion\.1\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$ | ||
^\[main\.assertion\.2\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$ | ||
x=15 \(00000000 00000000 00000000 00001111\) | ||
y=35 \(00000000 00000000 00000000 00100011\) | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
-- | ||
-- | ||
This tests the positive case of the simplification of the singleton interval | ||
(i.e when the presented interval *is* the singleton interval) |
17 changes: 17 additions & 0 deletions
17
regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp.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,17 @@ | ||
// Positive test for singleton interval simplification. | ||
// Notice that the sequence of the inequalities in this | ||
// expression is different to the one in | ||
// `singleton_interval_in_assume_7690.c`. | ||
|
||
int main() | ||
{ | ||
int x; | ||
__CPROVER_assume(x >= 15 && x <= 15); | ||
int y = x + 20; | ||
|
||
__CPROVER_assert( | ||
y != 35, "expected failure: only paths where x == 15 explored"); | ||
__CPROVER_assert( | ||
y == 34, "expected failure: only paths where x == 15 explored"); | ||
return 0; | ||
} |
18 changes: 18 additions & 0 deletions
18
regression/cbmc/simplify_singleton_interval_7690/singleton_interval_simp_neg.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,18 @@ | ||
// Negative test for singleton interval simplification. | ||
|
||
int main() | ||
{ | ||
int x; | ||
int y = x + 20; | ||
|
||
__CPROVER_assert( | ||
y != -6, "expected failure: paths where x is unbounded explored"); | ||
|
||
__CPROVER_assume(x >= 0 && x <= 15); | ||
__CPROVER_assert( | ||
y != 34, "expected failure: paths where 0 <= x <= 15 explored"); | ||
|
||
int z = x + 20; | ||
__CPROVER_assert(z != 36, "expected success: paths where x <= 15 explored"); | ||
return 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