pointer encoding: tests changed

kroening · kroening · commit 6d8e6461dca3 · 2022-04-27T21:05:51.000+01:00
diff --git a/regression/cbmc-primitives/r_w_ok_bug/test.desc b/regression/cbmc-primitives/r_w_ok_bug/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --no-simplify --no-propagation
 ^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$
diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test-no-cp.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$
diff --git a/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc b/regression/cbmc-primitives/r_w_ok_inconsistent_invalid/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc-primitives/same-object-01/test-no-cp.desc b/regression/cbmc-primitives/same-object-01/test-no-cp.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --no-simplify --no-propagation
 ^EXIT=0$
diff --git a/regression/cbmc-primitives/same-object-01/test.desc b/regression/cbmc-primitives/same-object-01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+KNOWNBUG`
`2`	`2`	`main.c`
`3`	`3`	`--pointer-check --no-simplify --no-propagation`
`4`	`4`	`^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$`