Bigger array in variable-sensitivity-array-nondet-access tests

Author: jezhiggins

regression/goto-analyzer/variable-sensitivity-array-nondet-access/main.c

@@ -1,6 +1,6 @@
 int main(void)
 {
-  int arr[] = {1, 2, 3};
+  int arr[] = {1, 2, 3, 4, 5};
   int ix;
   if(ix)
   {
@@ -10,24 +10,25 @@ int main(void)
   {
     ix = 2;
   }
-  // ix is between 0 and 2
-  // so this is between 1 and 3
+
+  // ix is between 0 and 4
+  // so this is between 1 and 5
   int arr_at_ix = arr[ix];
+
   int write_ix;
   if(write_ix)
   {
     write_ix = 0;
   }
   else
   {
-    write_ix = 1;
+    write_ix = 4;
   }
-  arr[write_ix] = 4;
+  arr[write_ix] = 99;
   int arr_0_after_write = arr[0];
   int arr_1_after_write = arr[1];
-  // We can't write to arr[2]
-  // because write_ix is between 0 and 1
-  // so this should be unchanged
   int arr_2_after_write = arr[2];
+  int arr_3_after_write = arr[3];
+  int arr_4_after_write = arr[4];
   return 0;
 }

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc

@@ -7,3 +7,5 @@ main::1::arr_at_ix \(\) -> TOP @ \[9\]
 main::1::arr_0_after_write \(\) -> TOP @ \[18\]
 main::1::arr_1_after_write \(\) -> TOP @ \[20\]
 main::1::arr_2_after_write \(\) -> TOP @ \[22\]
+main::1::arr_3_after_write \(\) -> TOP @ \[24\]
+main::1::arr_4_after_write \(\) -> TOP @ \[26\]

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc

@@ -4,6 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 main::1::arr_at_ix \(\) -> TOP @ \[9\]
-main::1::arr_0_after_write \(\) -> TOP @ \[18\]
-main::1::arr_1_after_write \(\) -> TOP @ \[20\]
-main::1::arr_2_after_write \(\) -> TOP @ \[22\]
+main::1::arr_0_after_write \(\) -> TOP
+main::1::arr_1_after_write \(\) -> TOP
+main::1::arr_2_after_write \(\) -> TOP
+main::1::arr_3_after_write \(\) -> TOP
+main::1::arr_4_after_write \(\) -> TOP

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc

@@ -4,6 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 main::1::arr_at_ix \(\) -> \[1, 3\] @ \[9\]
-main::1::arr_0_after_write \(\) -> \[1, 4\] @ \[18\]
-main::1::arr_1_after_write \(\) -> \[2, 4\] @ \[20\]
-main::1::arr_2_after_write \(\) -> \[3, 3\] @ \[22\]
+main::1::arr_0_after_write \(\) -> \[1, 63\] @ \[18\]
+main::1::arr_1_after_write \(\) -> \[2, 63\] @ \[20\]
+main::1::arr_2_after_write \(\) -> \[3, 63\] @ \[22\]
+main::1::arr_3_after_write \(\) -> \[4, 63\] @ \[24\]
+main::1::arr_4_after_write \(\) -> \[5, 63\] @ \[26\]

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc

@@ -3,7 +3,9 @@ main.c
 --show --variable-sensitivity --vsd-values intervals --vsd-arrays smash
 ^EXIT=0$
 ^SIGNAL=0$
-main::1::arr_at_ix \(\) -> \[1, 3\] @ \[9\]
-main::1::arr_0_after_write \(\) -> \[1, 4\] @ \[18\]
-main::1::arr_1_after_write \(\) -> \[1, 4\] @ \[20\]
-main::1::arr_2_after_write \(\) -> \[1, 4\] @ \[22\]
+main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\]
+main::1::arr_0_after_write \(\) -> \[1, 63\]
+main::1::arr_1_after_write \(\) -> \[1, 63\]
+main::1::arr_2_after_write \(\) -> \[1, 63\]
+main::1::arr_3_after_write \(\) -> \[1, 63\]
+main::1::arr_4_after_write \(\) -> \[1, 63\]

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-every-element.desc

@@ -4,6 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 main::1::arr_at_ix \(\) -> value-set-begin: 1, 3 :value-set-end
-main::1::arr_0_after_write \(\) -> value-set-begin: 1, 4 :value-set-end
-main::1::arr_1_after_write \(\) -> value-set-begin: 2, 4 :value-set-end
+main::1::arr_0_after_write \(\) -> value-set-begin: 1, 99 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
 main::1::arr_2_after_write \(\) -> value-set-begin: 3 :value-set-end
+main::1::arr_3_after_write \(\) -> value-set-begin: 4 :value-set-end
+main::1::arr_4_after_write \(\) -> value-set-begin: 5, 99 :value-set-end

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-smash.desc

@@ -3,7 +3,9 @@ main.c
 --show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays smash
 ^EXIT=0$
 ^SIGNAL=0$
-main::1::arr_at_ix \(\) -> value-set-begin: 1, 2, 3 :value-set-end
-main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4 :value-set-end
-main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4 :value-set-end
-main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4 :value-set-end
+main::1::arr_at_ix \(\) -> value-set-begin: 1, 2, 3, 4, 5 :value-set-end
+main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_3_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_4_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end