Updated array test to test exactly what we want

Author: thk123

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-array/main.c

@@ -1,56 +1,27 @@
-int a[10];
-
-int c[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
-
-void param_test(int array[])
-{
-    array[1] = 5;
-    // TODO: This is marked as "unknown" when running analysis of param_test and global_test. Doesn't seem correct
-    // as array[1] is being assigned one line above?
-    __CPROVER_assert(array[1]==5,  "array[1]==5");
-}
-
 void param_test_val(int array[], int x)
 {
     array[1] = x;
-    // TODO: This is marked as "unknown" when running analysis of param_test and global_test. Doesn't seem correct
-    // as array[1] is being assigned one line above?
-    //__CPROVER_assert(array[1]==5,  "array[1]==5");
-}
-
-void global_test()
-{
-    a[2] = 6;
-    __CPROVER_assert(a[2]==6,  "a[2]==6");
-    c[8] = 15;
-    __CPROVER_assert(c[8]==15,  "c[8]==15");
-    // TODO: This is marked as "unknown" when running analysis of global_test. CORRECT?
-    __CPROVER_assert(c[9]==9,  "c[9]==9");
 }
 
 void pass_param()
 {
     int b[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
-    
-    __CPROVER_assert(b[0]==0,  "b[0]==0");
-    __CPROVER_assert(b[4]==4,  "b[4]==4");
-    __CPROVER_assert(b[8]==8,  "b[8]==8");
-    // TODO: This is marked as "unknown" when running analysis of pass_param. CORRECT?
-    // The theme here is that global array initialisation assertions are marked as "unknown". Why?
-    __CPROVER_assert(c[8]==8,  "c[8]==8");
-    
-    param_test_val(b, 5);
 
-    __CPROVER_assert(b[1]==5,  "b[1]==5");
+    param_test_val(b, 5);
 
+    // This assertion should be true since b[0] is unmodified
     __CPROVER_assert(b[0]==0,  "b[0]==0");
-    __CPROVER_assert(b[4]==4,  "b[4]==4");
-    __CPROVER_assert(b[8]==8,  "b[8]==8");
 
-    __CPROVER_assert(b[1]==1,  "b[1]==1");
+    // This assertion should be true since b[1] can only have one value
+    __CPROVER_assert(b[1]==5,  "b[1]==5");
+
     param_test_val(b, 6);
+
+    // Both these assertions shoul be unknown since the domain for
+    // param_test_val, x is TOP so we don't know what is written
      __CPROVER_assert(b[1]==5,  "b[1]==5");
      __CPROVER_assert(b[1]==6,  "b[1]==6");
+
+     // b[0] is still not modified so this assertion should still be true
      __CPROVER_assert(b[0]==0,  "b[0]==0");
-     __CPROVER_assert(b[8]==8,  "b[8]==8");
 }

regression/goto-analyzer/variable-sensitivity-assign-aware-merge-array/test.desc

@@ -3,17 +3,9 @@ main.c
 --function pass_param --variable --pointers --arrays --structs --verify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[pass_param.assertion.1\] file main.c line 35 function pass_param, b\[0\]==0: Success$
-^\[pass_param.assertion.2\] file main.c line 36 function pass_param, b\[4\]==4: Success$
-^\[pass_param.assertion.3\] file main.c line 37 function pass_param, b\[8\]==8: Success$
-^\[pass_param.assertion.4\] file main.c line 40 function pass_param, c\[8\]==8: Unknown$
-^\[pass_param.assertion.5\] file main.c line 44 function pass_param, b\[1\]==5: Success$
-^\[pass_param.assertion.6\] file main.c line 46 function pass_param, b\[0\]==0: Success$
-^\[pass_param.assertion.7\] file main.c line 47 function pass_param, b\[4\]==4: Success$
-^\[pass_param.assertion.8\] file main.c line 48 function pass_param, b\[8\]==8: Success$
-^\[pass_param.assertion.9\] file main.c line 50 function pass_param, b\[1\]==1: Failure \(if reachable\)$
-^\[pass_param.assertion.10\] file main.c line 52 function pass_param, b\[1\]==5: Unknown$
-^\[pass_param.assertion.11\] file main.c line 53 function pass_param, b\[1\]==6: Unknown$
-^\[pass_param.assertion.12\] file main.c line 54 function pass_param, b\[0\]==0: Success$
-^\[pass_param.assertion.13\] file main.c line 55 function pass_param, b\[8\]==8: Success$
+\[pass_param\.assertion\.1\] .* b\[0\]==0: Success
+\[pass_param\.assertion\.2\] .* b\[1\]==5: Success
+\[pass_param\.assertion\.3\] .* b\[1\]==5: Unknown
+\[pass_param\.assertion\.4\] .* b\[1\]==6: Unknown
+\[pass_param\.assertion\.5\] .* b\[0\]==0: Success
 --