Merge pull request #8576 from remi-delmas-3000/contracts-is-fresh-demonic

CONTRACTS: separation checks using nondet demonic variable

Author: tautschnig

Diff for: regression/contracts-dfcc/test_aliasing_ensure/main.c

@@ -1,35 +1,15 @@
-#include <assert.h>
-#include <stdbool.h>
-#include <stdlib.h>
-
-int z;
-
-// clang-format off
-int foo(int *x, int *y)
-  __CPROVER_assigns(z, *x)
-  __CPROVER_requires(
-    __CPROVER_is_fresh(x, sizeof(int)) &&
-    *x > 0 &&
-    *x < 4)
-  __CPROVER_ensures(
-    __CPROVER_is_fresh(y, sizeof(int)) &&
-    !__CPROVER_is_fresh(x, sizeof(int)) &&
-    x != NULL &&
-    x != y &&
-    __CPROVER_return_value == *x + 5)
+int *foo()
+  // clang-format off
+  __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value, sizeof(int)))
 // clang-format on
 {
-  *x = *x + 4;
-  y = malloc(sizeof(*y));
-  *y = *x;
-  z = *y;
-  return (*x + 5);
+  int *ret = malloc(sizeof(int));
+  __CPROVER_assume(ret);
+  return ret;
 }
 
 int main()
 {
-  int n = 4;
-  n = foo(&n, &n);
-  assert(!(n < 4));
+  foo();
   return 0;
 }

Diff for: regression/contracts-dfcc/test_aliasing_ensure/test.desc

@@ -4,10 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$
-\[foo.assigns.\d+\].*Check that \*x is assignable: SUCCESS
-\[foo.assigns.\d+\].*Check that \*y is assignable: SUCCESS
-\[foo.assigns.\d+\].*Check that z is assignable: SUCCESS
-\[main.assertion.\d+\].*assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --

Diff for: regression/contracts-dfcc/test_scalar_memory_enforce/main.c

@@ -21,7 +21,6 @@ int foo(int *x)
     ptr_ok(x))
   __CPROVER_ensures(
     !ptr_ok(x) &&
-    !__CPROVER_is_fresh(x, sizeof(int)) &&
     return_ok(__CPROVER_return_value, x))
 // clang-format on
 {