Skip to content

Commit 6120ca2

Browse files
author
thk123
committed
Enabling some of these assertions in tests related to arrays
We have to turn on pointer sensitivity or otherwise when evaluating these expressions we won't get the correct write stack.
1 parent db48f03 commit 6120ca2

File tree

2 files changed

+8
-8
lines changed
  • regression/goto-analyzer
    • sensitivity-test-constants-array
    • sensitivity-test-constants-array-of-constants-array

2 files changed

+8
-8
lines changed

regression/goto-analyzer/sensitivity-test-constants-array-of-constants-array/test.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
sensitivity_test_constants_array_of_constants_array.c
3-
--variable --arrays --verify
3+
--variable --arrays --verify --pointers
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.assertion.1\] .* a\[1\]\[2\]==0: Success$
@@ -17,10 +17,10 @@ sensitivity_test_constants_array_of_constants_array.c
1717
^\[main.assertion.12\] .* 1\[b\]\[2\]==0: Failure \(if reachable\)$
1818
^\[main.assertion.13\] .* \*\(1\[b\]\+2\)==5: Success$
1919
^\[main.assertion.14\] .* \*\(1\[b\]\+2\)==0: Failure \(if reachable\)$
20-
^\[main.assertion.15\] .* \(\*\(1\+b\)\)\[2\]==5: Unknown$
21-
^\[main.assertion.16\] .* \(\*\(1\+b\)\)\[2\]==0: Unknown$
22-
^\[main.assertion.17\] .* \*\(\*\(1\+b\)\+2\)==5: Unknown$
23-
^\[main.assertion.18\] .* \*\(\*\(1\+b\)\+2\)==0: Unknown$
20+
^\[main.assertion.15\] .* \(\*\(1\+b\)\)\[2\]==5: Success$
21+
^\[main.assertion.16\] .* \(\*\(1\+b\)\)\[2\]==0: Failure \(if reachable\)$
22+
^\[main.assertion.17\] .* \*\(\*\(1\+b\)\+2\)==5: Success$
23+
^\[main.assertion.18\] .* \*\(\*\(1\+b\)\+2\)==0: Failure \(if reachable\)$
2424
^\[main.assertion.19\] .* 2\[1\[b\]\]==5: Success$
2525
^\[main.assertion.20\] .* 2\[1\[b\]\]==0: Failure \(if reachable\)$
2626
^\[main.assertion.21\] .* \*\(2\+1\[b\]\)==5: Unknown$

regression/goto-analyzer/sensitivity-test-constants-array/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
sensitivity_test_constants_array.c
3-
--variable --arrays --verify
3+
--variable --arrays --verify --pointers
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.assertion.1\] .* a\[1\]==0: Success$
@@ -9,8 +9,8 @@ sensitivity_test_constants_array.c
99
^\[main.assertion.4\] .* b\[1\]==1: Failure \(if reachable\)$
1010
^\[main.assertion.5\] .* \*\(b\+1\)==0: Success$
1111
^\[main.assertion.6\] .* \*\(b\+1\)==1: Failure \(if reachable\)$
12-
^\[main.assertion.7\] .* \*\(1\+b\)==0: Unknown$
13-
^\[main.assertion.8\] .* \*\(1\+b\)==1: Unknown$
12+
^\[main.assertion.7\] .* \*\(1\+b\)==0: Success$
13+
^\[main.assertion.8\] .* \*\(1\+b\)==1: Failure \(if reachable\)$
1414
^\[main.assertion.9\] .* 1\[b\]==0: Success$
1515
^\[main.assertion.10\] .* 1\[b\]==1: Failure \(if reachable\)$
1616
^\[main.assertion.11\] .* c\[0\]==0: Success$

0 commit comments

Comments
 (0)