klaas' Contracts work

.gitignore

@@ -19,6 +19,8 @@ src/.settings/*
 # Visual Studio
 Debug/*
 Release/*
+#vi(m)
+*.swp
 
 # compilation files
 *.lo
@@ -65,6 +67,8 @@ jbmc/regression/**/tests-symex-driven-loading.log
 
 # files stored by editors
 *~
+.*.swp
+.*.swo
 
 # libs downloaded by make [name]-download
 minisat*/

regression/ansi-c/code_contracts1/main.c

@@ -0,0 +1,21 @@
+int foo() __CPROVER_ensures(__CPROVER_forall {
+  int i;
+  1 == 1
+})
+{
+  return 1;
+}
+
+int bar() __CPROVER_ensures(__CPROVER_forall {
+  int i;
+  1 == 1
+} && __CPROVER_return_value == 1)
+{
+  return 1;
+}
+
+int main()
+{
+  foo();
+  bar();
+}

regression/ansi-c/code_contracts1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/contracts/function_apply_01/test.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 main.c
 --apply-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Applying code contracts currently also checks them.

regression/contracts/function_check_01/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/contracts/function_check_04/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^\[main.assertion.1\] .* assertion x == 0: SUCCESS$
-^\[foo.1\] line 9 : FAILURE$
+^\[foo.1\] .* : FAILURE$
 ^VERIFICATION FAILED$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/contracts/function_check_05/test.desc

@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 main.c
 --check-code-contracts
-^\[main.assertion.1\] assertion y == 0: FAILURE$
-^\[main.assertion.2\] assertion z == 1: SUCCESS$
-^\[foo.1\] : SUCCESS$
-^VERIFICATION SUCCESSFUL$
+^\[main.assertion.1\] .* assertion y == 0: FAILURE$
+^\[main.assertion.2\] .* assertion z == 1: SUCCESS$
+^\[foo.1\] .* : SUCCESS$
+^VERIFICATION FAILED$
 --
 --
-Contract checking does not properly havoc function calls.

regression/contracts/function_check_mem_01/main.c

@@ -33,7 +33,7 @@ void foo(bar *x)
   __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar)))
 {
   x->x += 1;
-  return
+  return;
 }
 
 int main()

regression/contracts/function_check_mem_01/test.desc

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

regression/contracts/invar_check_01/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/contracts/invar_check_02/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/contracts/invar_check_03/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/contracts/invar_check_04/test.desc

@@ -1,12 +1,11 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
+^EXIT=10$
+^SIGNAL=0$
 ^\[main.1\] .* Loop invariant violated before entry: SUCCESS$
 ^\[main.2\] .* Loop invariant not preserved: SUCCESS$
 ^\[main.assertion.1\] .* assertion r == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/goto-instrument/expand-pointer-predicates1/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x));
+  *x = 1;
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates2/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x, sizeof(int)));
+  *x = 1;
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates3/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x, sizeof(int)));
+  __CPROVER_assert(
+    __CPROVER_points_to_valid_memory(x, sizeof(int)), "Assert matches assume");
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates4/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int x;
+  int *y = &x;
+  __CPROVER_assert(__CPROVER_points_to_valid_memory(y), "Assert works on &");
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates5/main.c

@@ -0,0 +1,19 @@
+struct bar
+{
+  int w;
+  int x;
+  int y;
+  int z;
+};
+
+int main()
+{
+  struct bar s;
+  s.z = 5;
+  int *x_pointer = &(s.x);
+  __CPROVER_assert(
+    __CPROVER_points_to_valid_memory(x_pointer, 3 * sizeof(int)),
+    "Variable length assert");
+  assert(x_pointer[2] == 5);
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates5/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.assertion.1\] Variable length assert: SUCCESS$
+^\[main.assertion.2\] assertion x_pointer\[\(signed long( long)? int\)2\] == 5: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates6/main.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+
+struct my_struct
+{
+  int *field1;
+  int *field2;
+};
+
+void example(struct my_struct *s)
+{
+  s->field2 = malloc(sizeof(*(s->field2)));
+}
+
+int main()
+{
+  struct my_struct *s;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(s));
+  example(s);
+  __CPROVER_assert(__CPROVER_points_to_valid_memory(s->field2), "");
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates6/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.assertion.1\] : SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates7/main.c

@@ -0,0 +1,22 @@
+#include <stdlib.h>
+
+struct my_struct
+{
+  int *field;
+};
+
+void example(struct my_struct *s)
+{
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(s));
+  size_t size;
+  __CPROVER_assume(size == sizeof(*(s->field)));
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(s->field, size));
+  int read = *(s->field);
+}
+
+int main()
+{
+  struct my_struct *s;
+  example(s);
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates7/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates8/main.c

@@ -0,0 +1,16 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *x;
+  int *y;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x, 2 * sizeof(int)));
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(y, 2 * sizeof(int) - 1));
+  (void)(x[0]);  // Should succeed
+  (void)(x[1]);  // Should succeed
+  (void)(x[2]);  // Should fail
+  (void)(x[-1]); // Should fail
+  (void)(y[0]);  // Should succeed
+  (void)(y[1]);  // Should fail
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates8/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in x\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)2\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)-1\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in y\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)1\]: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

regression/goto-instrument/expand-pointer-predicates9/main.c

@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+int main()
+{
+  char *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x));
+  (void)(*x);       // Should succeed
+  (void)(*(x + 1)); // Should fail
+  (void)(*(x - 1)); // Should fail
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates9/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in \*x: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*\(x - \(signed long( long)? int\)1\): FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--