make smt2_conv extensible

This adds a mechanism to extend the SMT2 conversion with a functor for a
given expression id.

Author: kroening

regression/cprover/arrays/array_r_ok1.c

@@ -0,0 +1,7 @@
+int main()
+{
+  unsigned char array[10];
+  __CPROVER_assert(__CPROVER_r_ok(array, 10), "property 1");
+  unsigned char *array_ptr = array;
+  __CPROVER_assert(__CPROVER_r_ok(array_ptr, 10), "property 2");
+}

regression/cprover/arrays/array_r_ok1.desc

@@ -0,0 +1,8 @@
+CORE
+array_r_ok1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
+--

regression/cprover/basic/assume1.desc

@@ -9,7 +9,6 @@ assume1.c
 ^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)$
 ^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
 ^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=nondet::S25-0\]\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --

regression/cprover/basic/nondet1.desc

@@ -3,10 +3,10 @@ nondet1.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet::S22-0\]\)$
+^\(\d+\) ∀ ς : state, nondet::S22-0 : signedbv\[32\] \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet::S22-0\]\)$
 ^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
 ^\(\d+\) S23 = S22$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet::S24-0\]\)$
+^\(\d+\) ∀ ς : state, nondet::S24-0 : signedbv\[32\] \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet::S24-0\]\)$
 ^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
 ^\(\d+\) S25 = S24$
 ^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$

regression/cprover/contracts/check_assigns1.desc

@@ -1,6 +1,6 @@
 CORE
 check_assigns1.c
---no-inline
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[my_function1\.assigns\.1\] line \d+ assigns clause: SUCCESS$

regression/cprover/contracts/check_assigns2.desc

@@ -1,6 +1,6 @@
 CORE
 check_assigns2.c
---no-inline
+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cprover/contracts/check_postcondition1.desc

@@ -1,6 +1,6 @@
 CORE
 check_postcondition1.c
---no-inline
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[my_function1\.postcondition\.1\] line \d+ postcondition: SUCCESS$

regression/cprover/contracts/check_postcondition2.desc

@@ -1,6 +1,6 @@
 CORE
 check_postcondition2.c
---no-inline
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[my_function1\.postcondition\.1\] line \d+ postcondition: SUCCESS$

regression/cprover/contracts/check_postcondition3.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 check_postcondition3.c
---no-inline
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[my_function1\.postcondition\.1\] line \d+ postcondition: SUCCESS$

regression/cprover/contracts/check_precondition1.desc

@@ -1,6 +1,6 @@
 CORE
 check_precondition1.c
---no-inline
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.precondition\.1\] line \d+ precondition my_function: REFUTED$

regression/cprover/contracts/check_precondition2.desc

@@ -1,6 +1,6 @@
 CORE
 check_precondition2.c
---no-inline
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[caller\.precondition\.1\] line \d+ precondition callee: SUCCESS$

regression/cprover/contracts/check_return_value1.desc

@@ -1,6 +1,6 @@
 CORE
 check_return_value1.c
---no-inline
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[my_function1\.postcondition\.1\] line \d+ postcondition: SUCCESS$

regression/cprover/contracts/recursive_function1.desc

@@ -1,6 +1,6 @@
 CORE
 recursive_function1.c
---no-inline
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[recursive_function\.precondition\.1] line \d+ precondition recursive_function: SUCCESS$

regression/cprover/contracts/use_assigns1.desc

@@ -1,6 +1,6 @@
 CORE
 use_assigns1.c
---no-inline
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$

regression/cprover/contracts/use_assigns2.desc

@@ -1,6 +1,6 @@
 CORE
 use_assigns2.c
---no-inline
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$

regression/cprover/contracts/use_postcondition1.desc

@@ -1,6 +1,6 @@
 CORE
 use_postcondition1.c
---no-inline
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[callee\.assigns\.1\] line \d+ assigns clause: SUCCESS$

regression/cprover/contracts/use_precondition1.desc

@@ -1,6 +1,6 @@
 CORE
 use_precondition1.c
---no-inline
+
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[my_function\.assertion\.1\] line \d+ property 1: SUCCESS$

regression/cprover/cstrings/cstring_preserved2.desc

@@ -1,6 +1,6 @@
 CORE
 cstring_preserved2.c
---no-inline
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[cstring_preserved\.assertion\.1\] line \d+ p is still a cstring: SUCCESS$

regression/cprover/function_calls/call_no_body1.desc

@@ -4,6 +4,6 @@ call_no_body1.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\*\*\*\* WARNING: no body for function function_without_body$
-^\(\d+\) ∀ ς : state \. S28\.1\(ς\) ⇒ S28\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S28\.2-0\]\)$
+^\(\d+\) ∀ ς : state, nondet::S28\.2-0 : signedbv\[32\] \. S28\.1\(ς\) ⇒ S28\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S28\.2-0\]\)$
 ^\(\d+\) ∀ ς : state \. S28\.2\(ς\) ⇒ S28\.3\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$
 --

regression/cprover/function_calls/call_no_body2.desc

@@ -3,5 +3,5 @@ call_no_body2.c
 --text
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S28\.1\(ς\) ⇒ S28\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S28\.2-0\]\)$
+^\(\d+\) ∀ ς : state, nondet::S28\.2-0 : signedbv\[32\] \. S28\.1\(ς\) ⇒ S28\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S28\.2-0\]\)$
 --

regression/cprover/function_calls/va_args1.desc

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

regression/cprover/function_calls/va_args2.c

@@ -0,0 +1,18 @@
+#include <stdarg.h>
+
+void f(int first, ...)
+{
+  va_list ap;
+  va_start(ap, first);
+
+  int second;
+  second = va_arg(ap, int);
+
+  __CPROVER_assert(first == 1, "property 1");
+  __CPROVER_assert(second == 2, "property 2");
+}
+
+int main()
+{
+  f(1, 2);
+}

regression/cprover/function_calls/va_args2.desc

@@ -0,0 +1,8 @@
+CORE
+va_args2.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[f\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[f\.assertion\.2\] line \d+ property 2: SUCCESS$
+--

regression/cprover/function_calls/va_args3.c

@@ -0,0 +1,22 @@
+#include <stdarg.h>
+
+void f(int first, ...)
+{
+  va_list ap;
+  va_start(ap, first);
+
+  int second;
+  second = va_arg(ap, int);
+
+  int third;
+  third = va_arg(ap, int);
+
+  __CPROVER_assert(first == 1, "property 1");
+  __CPROVER_assert(second == 2, "property 2");
+  __CPROVER_assert(third == 3, "property 3");
+}
+
+int main()
+{
+  f(1, 2, 3);
+}

regression/cprover/function_calls/va_args3.desc

@@ -0,0 +1,9 @@
+CORE
+va_args3.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[f\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[f\.assertion\.2\] line \d+ property 2: SUCCESS$
+^\[f\.assertion\.3\] line \d+ property 3: SUCCESS$
+--

regression/cprover/loops/assigns1.c

@@ -0,0 +1,12 @@
+int main()
+{
+  int *p;
+  __CPROVER_assume(__CPROVER_r_ok(p));
+
+  for(int i=0; i<10; i++)
+  {
+    // does not assign p
+  }
+
+  __CPROVER_assert(__CPROVER_r_ok(p), "property 1"); // passes
+}

regression/cprover/loops/assigns1.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+assigns1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+--
+--

regression/cprover/loops/while_loop2.c

@@ -0,0 +1,11 @@
+int nondet_int();
+
+int main()
+{
+  int N = nondet_int();
+  int x = 0;
+  while(x < N)
+    x++;
+
+  __CPROVER_assert(x == N, "property 1"); // fails
+}

regression/cprover/loops/while_loop2.desc

@@ -0,0 +1,7 @@
+CORE
+while_loop2.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
+--

regression/cprover/pointers/const2.desc

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

regression/cprover/pointers/pointer_array1.c

@@ -0,0 +1,12 @@
+int some_int = 123;
+void *ptr_array[10] = { &some_int };
+  
+int main()
+{
+  __CPROVER_assert(ptr_array[0] == &some_int, "property 1");
+
+  void **array_pointer = ptr_array;
+
+  __CPROVER_assert(array_pointer[0] == &some_int, "property 2");
+  __CPROVER_assert(*((int *)(array_pointer[0])) == 123, "property 3");  
+}

regression/cprover/pointers/pointer_array1.desc

@@ -0,0 +1,9 @@
+CORE
+pointer_array1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
+^\[main\.assertion\.3\] line \d+ property 3: SUCCESS$
+--

regression/cprover/pointers/pointer_to_local1.desc

@@ -1,6 +1,6 @@
 CORE
 pointer_to_local1.c
---no-inline
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[foo\.assertion\.1\] line \d+ property 1: SUCCESS$

regression/cprover/pointers/pointer_to_pointer1.c

@@ -1,10 +1,12 @@
 #include <stdlib.h>
 
+int *p;
+void **p_ptr;
+
 int main()
 {
-  int *p;
   p = malloc(1);
-  void **q = &p;
-  void *new_mem = malloc(1);
-  free(*q);
+  p_ptr = &p;
+  __CPROVER_assert(__CPROVER_LIVE_OBJECT(*p_ptr), "property 1");
+  return 0;
 }

regression/cprover/pointers/pointer_to_pointer1.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 pointer_to_pointer1.c
---safety
+
 ^EXIT=0$
 ^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
-^\[main\.pointer\.1\] line \d+ pointer q safe: SUCCESS$
-^\[main\.free\.1\] line \d+ free argument must be valid dynamic object: SUCCESS$

regression/cprover/pointers/pointers0.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int x, *p;
+  p = &x;
+  __CPROVER_assert(*p == x, "property 1"); // should pass
+  return 0;
+}

regression/cprover/pointers/pointers0.desc

@@ -0,0 +1,9 @@
+CORE
+pointers0.c
+--text --solve --inline
+^EXIT=0$
+^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::p❞:=❝main::1::x❞\]\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(❝main::1::x❞\)\)$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+--

regression/cprover/pointers/struct_pointer6.c

@@ -5,6 +5,7 @@ struct buf {
 int main()
 {
   struct buf *b;
+  __CPROVER_assume(__CPROVER_r_ok(b));
   __CPROVER_assume(b->len == 456);
 
   __CPROVER_size_t x, *size_t_ptr = &x;

regression/cprover/safety/dynamic_object1.c

@@ -0,0 +1,12 @@
+int main()
+{
+  void *p, *q;
+  // functional consistency of dynamic_object
+  __CPROVER_assume(p == q);
+
+  __CPROVER_assert(
+    __CPROVER_DYNAMIC_OBJECT(p) == __CPROVER_DYNAMIC_OBJECT(q), "property 1");
+
+  __CPROVER_assert(
+    __CPROVER_DYNAMIC_OBJECT(p) == __CPROVER_DYNAMIC_OBJECT(q + 1), "property 2");
+}

regression/cprover/safety/dynamic_object1.desc

@@ -0,0 +1,8 @@
+CORE
+dynamic_object1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
+--