Skip to content

Commit 0e40866

Browse files
author
thk123
committed
Disabling check that writing out of bounds havocs the domain
At the moment, with arrays we assume all writes are in bounds. See issue diffblue#88
1 parent 53e424c commit 0e40866

File tree

2 files changed

+6
-6
lines changed
  • regression/goto-analyzer
    • sensitivity-test-constants-array-of-constants-array
    • sensitivity-test-two-value-array-of-two-value-array

2 files changed

+6
-6
lines changed

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -59,15 +59,15 @@ sensitivity_test_constants_array_of_constants_array.c
5959
^\[main.assertion.54\] .* assertion b\[j\]\[j\]==11: Unknown$
6060
^\[main.assertion.55\] .* assertion a\[100\]\[0\]==0: Unknown$
6161
^\[main.assertion.56\] .* assertion a\[0\]\[100\]==0: Unknown$
62-
^\[main.assertion.57\] .* assertion c==0: Unknown$
63-
^\[main.assertion.58\] .* assertion c==0: Unknown$
64-
^\[main.assertion.66\] .* assertion c==0: Unknown$
62+
^\[main.assertion.57\] .* assertion c==0: Success$
63+
^\[main.assertion.58\] .* assertion c==0: Success$
6564
^\[main.assertion.59\] .* assertion ei\[0\]\[1\]==1: Success$
6665
^\[main.assertion.60\] .* assertion ei\[0\]\[1\]==0: Failure \(if reachable\)$
6766
^\[main.assertion.61\] .* assertion ei\[2\]\[1\]==0: Success$
6867
^\[main.assertion.62\] .* assertion ei\[2\]\[1\]==1: Failure \(if reachable\)$
6968
^\[main.assertion.63\] .* assertion ej\[0\]\[1\]==0: Unknown$
7069
^\[main.assertion.64\] .* assertion ej\[2\]\[1\]==0: Unknown$
7170
^\[main.assertion.65\] .* assertion ek\[0\]\[1\]==0: Unknown$
71+
^\[main.assertion.66\] .* assertion c==0: Success$
7272
--
7373
^warning: ignoring

regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-array/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -59,15 +59,15 @@ sensitivity_test_two_value_array_of_two_value_array.c
5959
^\[main.assertion.54\] .* assertion b\[j\]\[j\]==11: Unknown$
6060
^\[main.assertion.55\] .* assertion a\[100\]\[0\]==0: Unknown$
6161
^\[main.assertion.56\] .* assertion a\[0\]\[100\]==0: Unknown$
62-
^\[main.assertion.57\] .* assertion c==0: Unknown$
63-
^\[main.assertion.58\] .* assertion c==0: Unknown$
64-
^\[main.assertion.66\] .* assertion c==0: Unknown$
62+
^\[main.assertion.57\] .* assertion c==0: Success$
63+
^\[main.assertion.58\] .* assertion c==0: Success$
6564
^\[main.assertion.59\] .* assertion ei\[0\]\[1\]==1: Unknown$
6665
^\[main.assertion.60\] .* assertion ei\[0\]\[1\]==0: Unknown$
6766
^\[main.assertion.61\] .* assertion ei\[2\]\[1\]==0: Unknown$
6867
^\[main.assertion.62\] .* assertion ei\[2\]\[1\]==1: Unknown$
6968
^\[main.assertion.63\] .* assertion ej\[0\]\[1\]==0: Unknown$
7069
^\[main.assertion.64\] .* assertion ej\[2\]\[1\]==0: Unknown$
7170
^\[main.assertion.65\] .* assertion ek\[0\]\[1\]==0: Unknown$
71+
^\[main.assertion.66\] .* assertion c==0: Success$
7272
--
7373
^warning: ignoring

0 commit comments

Comments
 (0)