In failure cases for is_fresh, create nondet pointer to null or unique empty object.

Removes nondeterminism on the pointer offset but solves performance problem with quantifiers.

Author: Remi Delmas

src/ansi-c/library/cprover_contracts.c

@@ -1206,9 +1206,16 @@ __CPROVER_HIDE:;
     }
     if(__VERIFIER_nondet___CPROVER_bool())
     {
-      // make pointer invalid, empty value set and nondet bit pattern
-      __CPROVER_size_t dummy = __VERIFIER_nondet_size();
-      *elem = (void *)dummy;
+      // in the failure case, make pointer null or pointing to a unique
+      // dummy object of size 0.
+      if(__VERIFIER_nondet___CPROVER_bool())
+      {
+        *elem = (void *)0;
+      }
+      else
+      {
+        *elem = __CPROVER_allocate(0, 0);
+      }
       return 0;
     }
     void *ptr = __CPROVER_allocate(size, 0);
@@ -1266,9 +1273,16 @@ __CPROVER_HIDE:;
     }
     if(__VERIFIER_nondet___CPROVER_bool())
     {
-      // make pointer invalid, empty value set and nondet bit pattern
-      __CPROVER_size_t dummy = __VERIFIER_nondet_size();
-      *elem = (void *)dummy;
+      // in the failure case, make pointer null or pointing to a unique
+      // dummy object of size 0.
+      if(__VERIFIER_nondet___CPROVER_bool())
+      {
+        *elem = (void *)0;
+      }
+      else
+      {
+        *elem = __CPROVER_allocate(0, 0);
+      }
       return 0;
     }
     void *ptr = __CPROVER_allocate(size, 0);
@@ -1372,9 +1386,16 @@ __CPROVER_HIDE:;
   {
     if(__VERIFIER_nondet___CPROVER_bool())
     {
-      // make pointer invalid, empty value set and nondet bit pattern
-      __CPROVER_size_t dummy = __VERIFIER_nondet_size();
-      *ptr = (void *)dummy;
+      // in the failure case, make pointer null or pointing to a unique
+      // dummy object of size 0.
+      if(__VERIFIER_nondet___CPROVER_bool())
+      {
+        *ptr = (void *)0;
+      }
+      else
+      {
+        *ptr = __CPROVER_allocate(0, 0);
+      }
       return 0;
     }