Merge pull request #6910 from NlightNFotis/pointer_support_new_smt_backend_qa

NlightNFotis · web-flow · commit 136c6f552e5c · 2022-06-10T15:04:04.000+01:00
Enable pointer tests from `regression/cbmc` to run using new SMT backend.
diff --git a/regression/cbmc/Pointer1/test.desc b/regression/cbmc/Pointer1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer10/test.desc b/regression/cbmc/Pointer10/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer11/test.desc b/regression/cbmc/Pointer11/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer12/test.desc b/regression/cbmc/Pointer12/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer14/test.desc b/regression/cbmc/Pointer14/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Pointer15/test.desc b/regression/cbmc/Pointer15/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer17/test.desc b/regression/cbmc/Pointer17/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer18/full-slice.desc b/regression/cbmc/Pointer18/full-slice.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --unwind 1 --no-unwinding-assertions --pointer-check --full-slice
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer18/test.desc b/regression/cbmc/Pointer18/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --unwind 1 --no-unwinding-assertions --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer25/test.desc b/regression/cbmc/Pointer25/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer26/test.desc b/regression/cbmc/Pointer26/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer27/test.desc b/regression/cbmc/Pointer27/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^SIGNAL=0$
diff --git a/regression/cbmc/Pointer29/test.desc b/regression/cbmc/Pointer29/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer30/test.desc b/regression/cbmc/Pointer30/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer6/test.desc b/regression/cbmc/Pointer6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer7/test.desc b/regression/cbmc/Pointer7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer8/test.desc b/regression/cbmc/Pointer8/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer9/test.desc b/regression/cbmc/Pointer9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic10/test.desc b/regression/cbmc/Pointer_Arithmetic10/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic12/test.desc b/regression/cbmc/Pointer_Arithmetic12/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.i
 --32 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic14/test.desc b/regression/cbmc/Pointer_Arithmetic14/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic15/test.desc b/regression/cbmc/Pointer_Arithmetic15/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_Arithmetic17/test.desc b/regression/cbmc/Pointer_Arithmetic17/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic19/test.desc b/regression/cbmc/Pointer_Arithmetic19/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --program-only
 ASSERT\(\{ 42, 43 \}\[POINTER_OFFSET\(p!0@1#2\) / \d+l*\] == 43\)$
diff --git a/regression/cbmc/Pointer_Arithmetic2/test.desc b/regression/cbmc/Pointer_Arithmetic2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic3/test.desc b/regression/cbmc/Pointer_Arithmetic3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic4/test.desc b/regression/cbmc/Pointer_Arithmetic4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic5/test.desc b/regression/cbmc/Pointer_Arithmetic5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check --bounds-check --function f
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_Arithmetic6/test.desc b/regression/cbmc/Pointer_Arithmetic6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic7/test.desc b/regression/cbmc/Pointer_Arithmetic7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic9/test.desc b/regression/cbmc/Pointer_Arithmetic9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Assume1/test.desc b/regression/cbmc/Pointer_Assume1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_array5/test.desc b/regression/cbmc/Pointer_array5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract1/test.desc b/regression/cbmc/Pointer_byte_extract1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract3/test.desc b/regression/cbmc/Pointer_byte_extract3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract6/test.desc b/regression/cbmc/Pointer_byte_extract6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract9/test.desc b/regression/cbmc/Pointer_byte_extract9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/pointer-overflow1/test.desc b/regression/cbmc/pointer-overflow1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-overflow-check --unsigned-overflow-check
 ^EXIT=10$
diff --git a/regression/cbmc/pointer-overflow2/test.desc b/regression/cbmc/pointer-overflow2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-overflow-check
 ^EXIT=0$
diff --git a/regression/cbmc/pointer-overflow3/test.desc b/regression/cbmc/pointer-overflow3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-overflow-check
 ^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
diff --git a/regression/cbmc/pointer-overflow4/test.desc b/regression/cbmc/pointer-overflow4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-overflow-check
 ^\[main.overflow.1\] line 10 arithmetic overflow on signed \* in (0x)?[0-9a-fA-F]+l* \* \(signed (long (long )?)?int\)4ul*: FAILURE$

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