Merge pull request #6829 from remi-delmas-3000/contracts-havoc-statics

CONTRACTS: havoc all statics by default

Author: feliperodri

doc/cprover-manual/contracts-functions.md

@@ -6,6 +6,10 @@ These clauses formally describe the specification of a function.
 CBMC also provides a series of built-in constructs to be used with functions
 contracts (e.g., _history variables_, _quantifiers_, and _memory predicates_).
 
+When a function contract is checked, the tool automatically havocs all static variables
+of the program (to start the analysis in an arbitrary state), in the same way
+as using `--nondet-static` would do. If one wishes not to havoc some static variables,
+then `--nondet-static-exclude name-of-variable` can be used.
 ## Overview
 
 Take a look at the example below.

doc/cprover-manual/contracts-loops.md

@@ -9,6 +9,11 @@ These clauses formally describe an abstraction of a loop for the purpose of a pr
 CBMC also provides a series of built-in constructs
 to aid writing loop contracts (e.g., _history variables_ and _quantifiers_).
 
+When a function contract is checked, the tool automatically havocs all static variables
+of the program (to start the analysis in an arbitrary state), in the same way
+as using `--nondet-static` would do. If one wishes not to havoc some static variables,
+then `--nondet-static-exclude name-of-variable` can be used.
+
 ## Overview
 
 Consider an implementation of the [binary search algorithm] below.

regression/contracts/assigns_enforce_17/main.c

@@ -1,6 +1,6 @@
 #include <assert.h>
 
-int x = 0;
+int x;
 
 void pure() __CPROVER_assigns()
 {
@@ -10,6 +10,7 @@ void pure() __CPROVER_assigns()
 
 int main()
 {
+  x = 0;
   pure();
   assert(x == 0);
   return 0;

regression/contracts/assigns_enforce_17/test.desc

@@ -7,5 +7,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Checks whether verification correctly distincts local variables
+Checks whether verification correctly distinguishes local variables
 and global variables with same name when checking frame conditions.

regression/contracts/assigns_function_pointer/main.c

@@ -1,7 +1,7 @@
 #include <assert.h>
 #include <stddef.h>
 
-int x = 0;
+int x;
 
 struct fptr_t
 {
@@ -26,7 +26,7 @@ void bar(struct fptr_t *s, void (**f)()) __CPROVER_assigns(s->f, *f)
 
 int main()
 {
-  assert(x == 0);
+  x = 0;
   struct fptr_t s;
   void (*f)();
   bar(&s, &f);

regression/contracts/assigns_function_pointer/test.desc

@@ -3,7 +3,6 @@ main.c
 --enforce-contract bar
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that s->f is assignable: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that \*f is assignable: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion x \=\= 1: SUCCESS$

regression/contracts/assigns_replace_08/main.c

@@ -1,7 +1,6 @@
 #include <stdlib.h>
 
-int x;
-int *z = &x;
+int *z;
 
 void bar() __CPROVER_assigns(*z)
 {
@@ -14,6 +13,8 @@ void foo() __CPROVER_assigns()
 
 int main()
 {
+  int x;
+  z = &x;
   foo();
   return 0;
 }

regression/contracts/assigns_replace_08/test.desc

@@ -11,4 +11,4 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 Checks whether CBMC properly evaluates subset relationship on assigns
-during replacement.
+during replacement when the targets are global variables.

regression/contracts/assigns_replace_09/main.c

@@ -1,7 +1,6 @@
 #include <stdlib.h>
 
-int x;
-int *z = &x;
+int *z;
 
 void bar() __CPROVER_assigns(*z)
 {
@@ -14,6 +13,8 @@ static void foo() __CPROVER_assigns(*z)
 
 int main()
 {
+  int x;
+  z = &x;
   foo();
   return 0;
 }

regression/contracts/assigns_replace_09/test.desc

@@ -10,4 +10,4 @@ main.c
 ^Condition: \!not\_found$
 --
 Checks whether CBMC properly evaluates subset relationship on assigns
-during replacement with static functions.
+during replacement with static functions when targets are global variables.