Mark dummy objects as deallocated

Remi Delmas · Remi Delmas · commit 9facabcafdc5 · 2025-01-14T13:53:56.000-05:00
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;
     }

Original file line number	Diff line number	Diff line change
`@@ -1207,14 +1207,17 @@ __CPROVER_HIDE:;`
`1207`	`1207`	`if(__VERIFIER_nondet___CPROVER_bool())`
`1208`	`1208`	`{`
`1209`	`1209`	`// in the failure case, make pointer null or pointing to a unique`
`1210`		`- // dummy object of size 0.`
	`1210`	`+ // dummy deallocated object of size 0.`
`1211`	`1211`	`if(__VERIFIER_nondet___CPROVER_bool())`
`1212`	`1212`	`{`
`1213`	`1213`	`elem = (void )0;`
`1214`	`1214`	`}`
`1215`	`1215`	`else`
`1216`	`1216`	`{`
`1217`		`- *elem = __CPROVER_allocate(0, 0);`
	`1217`	`+ void *dummy = __CPROVER_allocate(0, 0);`
	`1218`	`+ __CPROVER_deallocated =`
	`1219`	`+ __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated;`
	`1220`	`+ *elem = dummy;`
`1218`	`1221`	`}`
`1219`	`1222`	`return 0;`
`1220`	`1223`	`}`
`@@ -1274,14 +1277,17 @@ __CPROVER_HIDE:;`
`1274`	`1277`	`if(__VERIFIER_nondet___CPROVER_bool())`
`1275`	`1278`	`{`
`1276`	`1279`	`// in the failure case, make pointer null or pointing to a unique`
`1277`		`- // dummy object of size 0.`
	`1280`	`+ // dummy deallocated object of size 0.`
`1278`	`1281`	`if(__VERIFIER_nondet___CPROVER_bool())`
`1279`	`1282`	`{`
`1280`	`1283`	`elem = (void )0;`
`1281`	`1284`	`}`
`1282`	`1285`	`else`
`1283`	`1286`	`{`
`1284`		`- *elem = __CPROVER_allocate(0, 0);`
	`1287`	`+ void *dummy = __CPROVER_allocate(0, 0);`
	`1288`	`+ __CPROVER_deallocated =`
	`1289`	`+ __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated;`
	`1290`	`+ *elem = dummy;`
`1285`	`1291`	`}`
`1286`	`1292`	`return 0;`
`1287`	`1293`	`}`
`@@ -1387,14 +1393,17 @@ __CPROVER_HIDE:;`
`1387`	`1393`	`if(__VERIFIER_nondet___CPROVER_bool())`
`1388`	`1394`	`{`
`1389`	`1395`	`// in the failure case, make pointer null or pointing to a unique`
`1390`		`- // dummy object of size 0.`
	`1396`	`+ // dummy deallocated object of size 0.`
`1391`	`1397`	`if(__VERIFIER_nondet___CPROVER_bool())`
`1392`	`1398`	`{`
`1393`	`1399`	`ptr = (void )0;`
`1394`	`1400`	`}`
`1395`	`1401`	`else`
`1396`	`1402`	`{`
`1397`		`- *ptr = __CPROVER_allocate(0, 0);`
	`1403`	`+ void *dummy = __CPROVER_allocate(0, 0);`
	`1404`	`+ __CPROVER_deallocated =`
	`1405`	`+ __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated;`
	`1406`	`+ *ptr = dummy;`
`1398`	`1407`	`}`
`1399`	`1408`	`return 0;`
`1400`	`1409`	`}`