fx

Author: kroening

regression/cbmc/Pointer29/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.i
 --bounds-check --32 --no-simplify
 ^EXIT=10$

regression/cbmc/Typecast3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=10$

regression/cbmc/memory_allocation1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$

regression/cbmc/memory_allocation2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --bounds-check
 ^EXIT=10$

regression/cbmc/mm_io1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$

regression/cbmc/pointer-overflow3/no-simplify.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 --pointer-overflow-check --no-simplify
 ^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE

regression/cbmc/union12/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$

regression/cbmc/va_list3/windows-preprocessed.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+KNOWNBUG broken-smt-backend
 windows-preprocessed.i
 --winx64
 ^EXIT=0$