CONTRACTS: allow is_fresh to fail in assume contexts

Restores sound behaviour for is_fresh in assumption contexts.
Flip a coin to decide if the predicate must hold or not.
If it must hold, enforce its post conditions by allocating a
fresh object, otherwise, leave state undefined.
This behaviour was present in the initial version of the
predicate but was mistakenly erased when refatoring was
made to add malloc failure modes due to size overflow,
and we did not have a test covering that behaviour.

Author: Remi Delmas

regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c

@@ -0,0 +1,18 @@
+void foo(int *x)
+  // clang-format off
+  __CPROVER_requires(
+  /* Case A -- pointer is valid */
+  __CPROVER_is_fresh(x, sizeof(*x))
+  /* Case B -- pointer is invalid */
+      || 1)
+  __CPROVER_assigns(*x)
+// clang-format on
+{
+  *x = 0;
+}
+
+void main()
+{
+  int *x;
+  foo(x);
+}

regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc

@@ -0,0 +1,22 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
+^\[foo.assigns.\d+\] line 11 Check that *x is assignable: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer NULL in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer invalid in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 11 dereference failure: deallocated dynamic object in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 11 dereference failure: dead object in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer outside object bounds in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 11 dereference failure: invalid integer address in \*x: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when __CPROVER_is_fresh is disjunctions,
+the goto model accepts traces where __CPROVER_is_fresh evaluates to false
+and no object gets allocated, and pointers remains undefined.

src/ansi-c/library/cprover_contracts.c

@@ -1204,7 +1204,10 @@ __CPROVER_HIDE:;
         "__CPROVER_is_fresh max allocation size exceeded");
       __CPROVER_assume(size <= __CPROVER_max_malloc_size);
     }
-
+    if(__VERIFIER_nondet___CPROVER_bool())
+    {
+      return 0;
+    }
     void *ptr = __CPROVER_allocate(size, 0);
     *elem = ptr;
 
@@ -1258,7 +1261,10 @@ __CPROVER_HIDE:;
         "__CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size");
       __CPROVER_assume(size <= __CPROVER_max_malloc_size);
     }
-
+    if(__VERIFIER_nondet___CPROVER_bool())
+    {
+      return 0;
+    }
     void *ptr = __CPROVER_allocate(size, 0);
     *elem = ptr;