Mark dummy objects as deallocated

Author: Remi Delmas

src/ansi-c/library/cprover_contracts.c

@@ -1207,14 +1207,17 @@ __CPROVER_HIDE:;
     if(__VERIFIER_nondet___CPROVER_bool())
     {
       // in the failure case, make pointer null or pointing to a unique
-      // dummy object of size 0.
+      // dummy deallocated object of size 0.
       if(__VERIFIER_nondet___CPROVER_bool())
       {
         *elem = (void *)0;
       }
       else
       {
-        *elem = __CPROVER_allocate(0, 0);
+        void *dummy = __CPROVER_allocate(0, 0);
+        __CPROVER_deallocated =
+          __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated;
+        *elem = dummy;
       }
       return 0;
     }
@@ -1274,14 +1277,17 @@ __CPROVER_HIDE:;
     if(__VERIFIER_nondet___CPROVER_bool())
     {
       // in the failure case, make pointer null or pointing to a unique
-      // dummy object of size 0.
+      // dummy deallocated object of size 0.
       if(__VERIFIER_nondet___CPROVER_bool())
       {
         *elem = (void *)0;
       }
       else
       {
-        *elem = __CPROVER_allocate(0, 0);
+        void *dummy = __CPROVER_allocate(0, 0);
+        __CPROVER_deallocated =
+          __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated;
+        *elem = dummy;
       }
       return 0;
     }
@@ -1387,14 +1393,17 @@ __CPROVER_HIDE:;
     if(__VERIFIER_nondet___CPROVER_bool())
     {
       // in the failure case, make pointer null or pointing to a unique
-      // dummy object of size 0.
+      // dummy deallocated object of size 0.
       if(__VERIFIER_nondet___CPROVER_bool())
       {
         *ptr = (void *)0;
       }
       else
       {
-        *ptr = __CPROVER_allocate(0, 0);
+        void *dummy = __CPROVER_allocate(0, 0);
+        __CPROVER_deallocated =
+          __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated;
+        *ptr = dummy;
       }
       return 0;
     }