Mark dummy objects as deallocated

remi-delmas-3000 · Jan 14, 2025 · 9facabc · 9facabc
1 parent 2d8ab18
commit 9facabc
Showing 1 changed file with 15 additions and 6 deletions.
diff --git a/src/ansi-c/library/cprover_contracts.c b/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;
     }