Add cbmc-from-CVS regression tests

Move the remaining tests from cbmc-from-CVS to cbmc and fix their test
specifications to work with current CBMC. This enables otherwise unused
tests.

Author: tautschnig

regression/cbmc-from-CVS/Makefile

@@ -1,4 +1,4 @@
-//void *malloc(unsigned);
+#include <stdlib.h>
 
 void __blast_assert()
 {

regression/cbmc-from-CVS/Malloc4/test.desc

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

regression/cbmc-from-CVS/Malloc5/test.desc

@@ -3,7 +3,6 @@ main.c
 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^Counterexample:$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-from-CVS/Malloc8/test.desc

@@ -1,5 +1,6 @@
+#include <stdlib.h>
+
 int nondet_int();
-void *malloc(unsigned s);
 
 typedef struct {
     int i;

regression/cbmc-from-CVS/Pointer3/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^SIGNAL=0$
+^EXIT=10$
+^VERIFICATION FAILED$
+^\[analyze_this.pointer_dereference.5\] line 19 dereference failure: pointer outside dynamic object bounds in p->i: FAILURE$
+--
+^warning: ignoring

regression/cbmc-from-CVS/Pointer31/test.desc

@@ -1,5 +1,6 @@
+#include <stdlib.h>
+
 _Bool nondet_bool();
-void *malloc(unsigned s);
 
 int analyze_this()
 {

regression/cbmc-from-CVS/return2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^SIGNAL=0$
+^EXIT=10$
+^VERIFICATION FAILED$
+^\[analyze_this.pointer_dereference.5\] line 16 dereference failure: pointer outside dynamic object bounds in \*p_int: FAILURE$
+--
+^warning: ignoring

regression/cbmc-from-CVS/Array_Access1/main.c renamed to regression/cbmc/Array_Access1/main.c

@@ -1,5 +1,6 @@
+#include <stdlib.h>
+
 _Bool nondet_bool();
-void *malloc(unsigned s);
 
 int analyze_this()
 {

regression/cbmc-from-CVS/Array_Access1/test.desc renamed to regression/cbmc/Array_Access1/test.desc

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

regression/cbmc-from-CVS/Array_Access2/main.c renamed to regression/cbmc/Array_Access2/main.c

@@ -1,6 +1,6 @@
-int *global;
+#include <stdlib.h>
 
-void *malloc(unsigned);
+int *global;
 
 struct X
 {

regression/cbmc-from-CVS/Array_Access2/test.desc renamed to regression/cbmc/Array_Access2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.pointer_dereference.\d+\] line 27 dereference failure: pointer invalid in \*ptr_ptr_p2: FAILURE$
+--

regression/cbmc-from-CVS/Array_Access3/main.c renamed to regression/cbmc/Array_Access3/main.c

@@ -1,4 +1,4 @@
-void *malloc(unsigned);
+#include <stdlib.h>
 
 void *my_malloc(unsigned size)
 {

regression/cbmc-from-CVS/Array_Access3/test.desc renamed to regression/cbmc/Array_Access3/test.desc

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

regression/cbmc-from-CVS/Array_Pointer1/main.c renamed to regression/cbmc/Array_Pointer1/main.c

@@ -1,8 +1,8 @@
 CORE
 main.c
 --pointer-check
-^SIGNAL=0$
-^Counterexample:$
 ^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc-from-CVS/Array_Pointer1/test.desc renamed to regression/cbmc/Array_Pointer1/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 --pointer-check
 ^SIGNAL=0$
-^Counterexample:$
+^EXIT=10$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-from-CVS/Array_Pointer2/main.c renamed to regression/cbmc/Array_Pointer2/main.c

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

regression/cbmc-from-CVS/Array_Pointer2/test.desc renamed to regression/cbmc/Array_Pointer2/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 --pointer-check
 ^SIGNAL=0$
-^Counterexample:$
+^EXIT=10$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-from-CVS/Array_Pointer3/main.c renamed to regression/cbmc/Array_Pointer3/main.c

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

regression/cbmc-from-CVS/Array_Pointer3/test.desc renamed to regression/cbmc/Array_Pointer3/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 
 ^SIGNAL=0$
-^Counterexample:$
+^EXIT=10$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-from-CVS/Array_Pointer4/main.c renamed to regression/cbmc/Array_Pointer4/main.c

@@ -1,6 +1,7 @@
 int main()
 {
   int *p=(int *)4;
+  __CPROVER_allocated_memory(4, sizeof(int));
   int i;
   int **q;
   char *pp;
@@ -20,6 +21,7 @@ int main()
     __CPROVER_assert(p==0, "i==0 => p==NULL");
 
   q=(int **)8;
+  __CPROVER_allocated_memory(8, sizeof(int *));
   *q=&i;
   **q=0x01020304;
   __CPROVER_assert(i==0x01020304, "**q");

regression/cbmc-from-CVS/Array_Pointer4/test.desc renamed to regression/cbmc/Array_Pointer4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --little-endian
 ^EXIT=0$

regression/cbmc-from-CVS/Array_Pointer5/main.c renamed to regression/cbmc/Array_Pointer5/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^SIGNAL=0$
+^EXIT=10$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-from-CVS/Array_Pointer5/test.desc renamed to regression/cbmc/Array_Pointer5/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^SIGNAL=0$
+^EXIT=10$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-from-CVS/Array_Pointer6/main.c renamed to regression/cbmc/Array_Pointer6/main.c

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

regression/cbmc-from-CVS/Array_Pointer6/test.desc renamed to regression/cbmc/Array_Pointer6/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 --pointer-check --bounds-check
 ^SIGNAL=0$
-^Counterexample:$
+^EXIT=10$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-from-CVS/Array_Pointer7/main.c renamed to regression/cbmc/Array_Pointer7/main.c

@@ -1,6 +1,6 @@
 CORE
 main.c
---fixedbv
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-from-CVS/Array_Pointer7/test.desc renamed to regression/cbmc/Array_Pointer7/test.desc

@@ -0,0 +1,8 @@
+CORE
+tcas_v23_523.c
+--bounds-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[ALIM.array_bounds.2\] line 68 array 'Positive_RA_Alt_Thresh' upper bound in Positive_RA_Alt_Thresh\[\(signed (long (long )?)?int\)Alt_Layer_Value\]: FAILURE$
+--