Skip to content

Commit 83414be

Browse files
jezhigginsjezhiggins
committed
Correct evaluation of assume in the face of not_exprs
For intervals and value-sets it's possible for, say, (a > b) and !(a > b) to both be true. When evaluationing !(expr) we can't simply flip the result. Instead, where we can, we need to rewrite !(a > b) as (a <= b) and evaluate that instead.
1 parent 8e8eb20 commit 83414be

File tree

59 files changed

+599
-1
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

59 files changed

+599
-1
lines changed

‎regression/goto-analyzer/branching-ge/main-always.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
int unknown();
2+
3+
int main()
4+
{
5+
int i = 0;
6+
int p = 0;
7+
8+
if(unknown())
9+
p = 5;
10+
if(unknown())
11+
p = 10;
12+
13+
if(p >= 0)
14+
i = 5;
15+
else
16+
i = -5;
17+
}

‎regression/goto-analyzer/branching-ge/main-indeterminate.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
int unknown();
2+
3+
int main()
4+
{
5+
int i = 0;
6+
int p = 0;
7+
8+
if(unknown())
9+
p = 5;
10+
if(unknown())
11+
p = 10;
12+
13+
if(p >= 5)
14+
i = 5;
15+
else
16+
i = -5;
17+
}

‎regression/goto-analyzer/branching-ge/main-never.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
int unknown();
2+
3+
int main()
4+
{
5+
int i = 0;
6+
int p = 0;
7+
8+
if(unknown())
9+
p = 5;
10+
if(unknown())
11+
p = 10;
12+
13+
if(p >= 11)
14+
i = 5;
15+
else
16+
i = -5;
17+
}

‎regression/goto-analyzer/branching-ge/test-always-constants.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-always.c
3+
--variable-sensitivity --vsd-values constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* TOP @ \[17, 19\]
7+
^main::1::p .* TOP @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-ge/test-always-intervals.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-always.c
3+
--variable-sensitivity --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* \[5, 5\] @ \[17\]
7+
^main::1::p .* \[0, A\] @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-ge/test-always-value-set.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-always.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\]
7+
^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-ge/test-indeterminate-constants.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-indeterminate.c
3+
--variable-sensitivity --vsd-values constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* TOP @ \[17, 19\]
7+
^main::1::p .* TOP @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-ge/test-indeterminate-intervals.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-indeterminate.c
3+
--variable-sensitivity --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\]
7+
^main::1::p .* \[0, A\] @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-ge/test-indeterminate-value-set.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-indeterminate.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\]
7+
^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-ge/test-never-constants.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-never.c
3+
--variable-sensitivity --vsd-values constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* TOP @ \[17, 19\]
7+
^main::1::p .* TOP @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-ge/test-never-intervals.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-never.c
3+
--variable-sensitivity --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\]
7+
^main::1::p .* \[0, A\] @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-ge/test-never-value-set.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-never.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* value-set-begin: -5 :value-set-end @ \[19\]
7+
^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-gt/main-always.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
int unknown();
2+
3+
int main()
4+
{
5+
int i = 0;
6+
int p = 0;
7+
8+
if(unknown())
9+
p = 5;
10+
if(unknown())
11+
p = 10;
12+
13+
if(p > -1)
14+
i = 5;
15+
else
16+
i = -5;
17+
}

‎regression/goto-analyzer/branching-gt/main-indeterminate.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
int unknown();
2+
3+
int main()
4+
{
5+
int i = 0;
6+
int p = 0;
7+
8+
if(unknown())
9+
p = 5;
10+
if(unknown())
11+
p = 10;
12+
13+
if(p > 5)
14+
i = 5;
15+
else
16+
i = -5;
17+
}

‎regression/goto-analyzer/branching-gt/main-never.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
int unknown();
2+
3+
int main()
4+
{
5+
int i = 0;
6+
int p = 0;
7+
8+
if(unknown())
9+
p = 5;
10+
if(unknown())
11+
p = 10;
12+
13+
if(p > 10)
14+
i = 5;
15+
else
16+
i = -5;
17+
}

‎regression/goto-analyzer/branching-gt/test-always-constants.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-always.c
3+
--variable-sensitivity --vsd-values constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* TOP @ \[17, 19\]
7+
^main::1::p .* TOP @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-gt/test-always-intervals.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-always.c
3+
--variable-sensitivity --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* \[5, 5\] @ \[17\]
7+
^main::1::p .* \[0, A\] @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-gt/test-always-value-set.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-always.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\]
7+
^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-gt/test-indeterminate-constants.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-indeterminate.c
3+
--variable-sensitivity --vsd-values constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* TOP @ \[17, 19\]
7+
^main::1::p .* TOP @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-gt/test-indeterminate-intervals.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-indeterminate.c
3+
--variable-sensitivity --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\]
7+
^main::1::p .* \[0, A\] @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-gt/test-indeterminate-value-set.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-indeterminate.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\]
7+
^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-gt/test-never-constants.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-never.c
3+
--variable-sensitivity --vsd-values constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* TOP @ \[17, 19\]
7+
^main::1::p .* TOP @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-gt/test-never-intervals.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-never.c
3+
--variable-sensitivity --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\]
7+
^main::1::p .* \[0, A\] @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-gt/test-never-value-set.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-never.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* value-set-begin: -5 :value-set-end @ \[19\]
7+
^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-le/main-always.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
int unknown();
2+
3+
int main()
4+
{
5+
int i = 0;
6+
int p = 0;
7+
8+
if(unknown())
9+
p = 5;
10+
if(unknown())
11+
p = 10;
12+
13+
if(p <= 10)
14+
i = 5;
15+
else
16+
i = -5;
17+
}

‎regression/goto-analyzer/branching-le/main-indeterminate.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
int unknown();
2+
3+
int main()
4+
{
5+
int i = 0;
6+
int p = 0;
7+
8+
if(unknown())
9+
p = 5;
10+
if(unknown())
11+
p = 10;
12+
13+
if(p <= 5)
14+
i = 5;
15+
else
16+
i = -5;
17+
}

‎regression/goto-analyzer/branching-le/main-never.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
int unknown();
2+
3+
int main()
4+
{
5+
int i = 0;
6+
int p = 0;
7+
8+
if(unknown())
9+
p = 5;
10+
if(unknown())
11+
p = 10;
12+
13+
if(p <= -1)
14+
i = 5;
15+
else
16+
i = -5;
17+
}

‎regression/goto-analyzer/branching-le/test-always-constants.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-always.c
3+
--variable-sensitivity --vsd-values constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* TOP @ \[17, 19\]
7+
^main::1::p .* TOP @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-le/test-always-intervals.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-always.c
3+
--variable-sensitivity --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* \[5, 5\] @ \[17\]
7+
^main::1::p .* \[0, A\] @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-le/test-always-value-set.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-always.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* value-set-begin: 5 :value-set-end @ \[17\]
7+
^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-le/test-indeterminate-constants.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-indeterminate.c
3+
--variable-sensitivity --vsd-values constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* TOP @ \[17, 19\]
7+
^main::1::p .* TOP @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-le/test-indeterminate-intervals.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-indeterminate.c
3+
--variable-sensitivity --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* \[FFFFFFFB, 5\] @ \[17, 19\]
7+
^main::1::p .* \[0, A\] @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-le/test-indeterminate-value-set.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-indeterminate.c
3+
--variable-sensitivity --vsd-values set-of-constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* value-set-begin: 5, -5 :value-set-end @ \[17, 19\]
7+
^main::1::p .* value-set-begin: 0, 5, 10 :value-set-end @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-le/test-never-constants.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-never.c
3+
--variable-sensitivity --vsd-values constants --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* TOP @ \[17, 19\]
7+
^main::1::p .* TOP @ \[3, 8, 14\]
8+
--

‎regression/goto-analyzer/branching-le/test-never-intervals.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main-never.c
3+
--variable-sensitivity --vsd-values intervals --show
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^main::1::i .* \[FFFFFFFB, FFFFFFFB\] @ \[19\]
7+
^main::1::p .* \[0, A\] @ \[3, 8, 14\]
8+
--

0 commit comments

Comments
 (0)