Enable all shadow memory regression tests

NlightNFotis · NlightNFotis · commit 61262eb224d7 · 2023-08-22T17:35:27.000+01:00
diff --git a/regression/cbmc-shadow-memory/char1/test.desc b/regression/cbmc-shadow-memory/char1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/constchar-param1/test.desc b/regression/cbmc-shadow-memory/constchar-param1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --unwind 11
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/constchar-pointers1/test.desc b/regression/cbmc-shadow-memory/constchar-pointers1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --unwind 11
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/errno1/test.desc b/regression/cbmc-shadow-memory/errno1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/float1/test.desc b/regression/cbmc-shadow-memory/float1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/getenv1/test.desc b/regression/cbmc-shadow-memory/getenv1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/global1/test.desc b/regression/cbmc-shadow-memory/global1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/linked-list1/test.desc b/regression/cbmc-shadow-memory/linked-list1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/linked-list2/test.desc b/regression/cbmc-shadow-memory/linked-list2/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/local1/test.desc b/regression/cbmc-shadow-memory/local1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/malloc1/test.desc b/regression/cbmc-shadow-memory/malloc1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/maybe-null1/test.desc b/regression/cbmc-shadow-memory/maybe-null1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/memcpy1/test.desc b/regression/cbmc-shadow-memory/memcpy1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc b/regression/cbmc-shadow-memory/nondet-pointer-into-struct1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc b/regression/cbmc-shadow-memory/nondet-size-arrays1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/param1/test.desc b/regression/cbmc-shadow-memory/param1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/static1/test.desc b/regression/cbmc-shadow-memory/static1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/strdup1/test.desc b/regression/cbmc-shadow-memory/strdup1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --unwind 4
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/struct-get-max1/test.desc b/regression/cbmc-shadow-memory/struct-get-max1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/struct-get-or1/test.desc b/regression/cbmc-shadow-memory/struct-get-or1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/struct-set1/test.desc b/regression/cbmc-shadow-memory/struct-set1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/taint-example1/test.desc b/regression/cbmc-shadow-memory/taint-example1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --unwind 15
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/trace1/test.desc b/regression/cbmc-shadow-memory/trace1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 --stop-on-fail --unwind 5
 ^EXIT=10$
diff --git a/regression/cbmc-shadow-memory/union-get-max1/test.desc b/regression/cbmc-shadow-memory/union-get-max1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/union-get-or1/test.desc b/regression/cbmc-shadow-memory/union-get-or1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/union-set1/test.desc b/regression/cbmc-shadow-memory/union-set1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/var-assign1/test.desc b/regression/cbmc-shadow-memory/var-assign1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc b/regression/cbmc-shadow-memory/void-ptr-param-set1/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=6$
diff --git a/regression/cbmc-shadow-memory/void-ptr-param2/test.desc b/regression/cbmc-shadow-memory/void-ptr-param2/test.desc
@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-FUTURE`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`