Skip to content

Commit f10618f

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 42afd18 commit f10618f

File tree

2 files changed

+8
-8
lines changed
  • regression/goto-analyzer
    • sensitivity-test-constants-array-of-constants-array
    • sensitivity-test-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)