Tentative: pointers are invalid when pointer predicates return false.

Modifies the semantics of is_fresh and pointer_in_range_dfcc to
make pointers invalid in the `false` case. Solves the performance
blowup when pointer predicates are used in combination with
nondet-pointer for contract replacement.
Soundness needs to be reviewed/discussed.

Author: Remi Delmas

src/ansi-c/library/cprover_contracts.c

@@ -1206,6 +1206,8 @@ __CPROVER_HIDE:;
     }
     if(__VERIFIER_nondet___CPROVER_bool())
     {
+      __CPROVER_size_t dummy = __VERIFIER_nondet_size();
+      *elem = (void *) dummy;
       return 0;
     }
     void *ptr = __CPROVER_allocate(size, 0);
@@ -1263,6 +1265,8 @@ __CPROVER_HIDE:;
     }
     if(__VERIFIER_nondet___CPROVER_bool())
     {
+      __CPROVER_size_t dummy = __VERIFIER_nondet_size();
+      *elem = (void *) dummy;
       return 0;
     }
     void *ptr = __CPROVER_allocate(size, 0);
@@ -1365,7 +1369,11 @@ __CPROVER_HIDE:;
   if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx)
   {
     if(__VERIFIER_nondet___CPROVER_bool())
+    {
+      __CPROVER_size_t dummy = __VERIFIER_nondet_size();
+      *ptr = (void *)dummy;
       return 0;
+    }
 
     // add nondet offset
     __CPROVER_size_t offset = __VERIFIER_nondet_size();