Merge pull request #6438 from NlightNFotis/flip_cbmc_primitives_tests_core

Flip passing FUTURE tests to CORE in `regression/cbmc-primitives`

Author: NlightNFotis

regression/cbmc-primitives/dynamic-object-02/test-no-cp.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --no-simplify --no-propagation
 ^EXIT=10$
@@ -10,5 +10,6 @@ main.c
 --
 Check that the dynamic object property is nondet for uninitialized pointers. We
 use --no-simplify and --no-propagation to ensure that the case is not solved by
-the constant propagation and thus tests the constraint encoding. Recorded as
-ADA-526.
+the constant propagation and thus tests the constraint encoding. We expect
+that `__CPROVER_DYNAMIC_OBJECT` should be nondet for pointers that are neither
+null nor valid.

regression/cbmc-primitives/dynamic-object-02/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=10$
@@ -9,4 +9,3 @@ main.c
 ^warning: ignoring
 --
 Check that the dynamic object property is nondet for uninitialized pointers.
-Recorded as ADA-526.

regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --no-simplify --no-propagation
 ^EXIT=10$
@@ -11,4 +11,3 @@ main.c
 Check that both positive and negative offsets can be chosen for uninitialized
 pointers. We use --no-simplify and --no-propagation to ensure that the case is
 not solved by the constant propagation and thus tests the constraint encoding.
-Recorded as ADA-528.

regression/cbmc-primitives/pointer-offset-01/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=10$
@@ -8,5 +8,10 @@ main.c
 --
 ^warning: ignoring
 --
-Check that both positive and negative offsets can be chosen for uninitialized
-pointers. Recorded as ADA-528.
+For uninitialised pointers, CBMC chooses a nondeterministic value (though no memory
+is allocated). Since the offset of pointers is signed, negative offsets should be
+able to be chosen (along with positive ones) non-deterministically.
+`__CPROVER_POINTER_OFFSET` is the CBMC primitive that gets the pointer offset
+from the base address of the object. This test guards this, and especially
+against the case where we could only observe some cases where offsets were only
+positive (in some CI configurations, for instance).