mark some KNOWNBUG loop contracts tests as CORE

Author: SaswatPadhi

regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc

@@ -18,4 +18,8 @@ to pass -- we should not mistakenly havoc the allocations, just their values.
 However, the `data[1][2][3] == 0` assertion is expected to fail since `data`
 is havoced.
 
-Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`.
+The assigns clause in this case would have an entire 3D space,
+and some of it must be re-established, to the original objects
+but with different values at certain locations, by the loop invariant.
+However, currently we cannot restrict same_object for pointers
+within loop invariants.

regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c

@@ -17,7 +17,7 @@ void main()
   data[4][5][6] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
-    __CPROVER_loop_invariant(i <= SIZE)
+    __CPROVER_assigns(i, data[4][5][6]) __CPROVER_loop_invariant(i <= SIZE)
     {
       data[4][5][6] = 1;
     }

regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc

@@ -1,12 +1,14 @@
-KNOWNBUG
+CORE
 main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.\d+\] .* Check that data\[(.*)4\]\[(.*)5\]\[(.*)6\] is assignable: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
+^\[main.assertion.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --
@@ -17,5 +19,3 @@ The `data[4][5][6] == 0` assertion is expected to fail since `data[4][5][6]`
 is havoced and the invariant does not reestablish its value.
 However, the `data[1][2][3] == 0` assertion is expected to pass -- we should
 not havoc the entire `data` array, if only a constant index if being modified.
-
-Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`.

regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc

@@ -19,4 +19,8 @@ We _could_ do a more precise analysis in future where we only havoc
 `data[4][5][6]` but not `data[1][2][3]` since the latter clearly cannot be
 modified in the given loop.
 
-Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`.
+The assigns clause in this case would have an entire 2D grid,
+and some of it must be re-established, to the original objects
+but with different values at certain locations, by the loop invariant.
+However, currently we cannot restrict same_object for pointers
+within loop invariants.