Merge pull request #6858 from tautschnig/cleanup/deallocated-updates

Remove unnecessary __CPROVER_deallocated updates

Author: tautschnig

src/ansi-c/library/stdlib.c

@@ -146,10 +146,6 @@ __CPROVER_HIDE:;
   // and __CPROVER_allocate doesn't, but no one cares
   malloc_res = __CPROVER_allocate(alloc_size, 1);
 
-  // make sure it's not recorded as deallocated
-  __CPROVER_deallocated =
-    (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
-
   // record the object size for non-determistic bounds checking
   __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_malloc_is_new_array =
@@ -210,10 +206,6 @@ __CPROVER_HIDE:;
   void *malloc_res;
   malloc_res = __CPROVER_allocate(malloc_size, 0);
 
-  // make sure it's not recorded as deallocated
-  __CPROVER_deallocated =
-    (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
-
   // record the object size for non-determistic bounds checking
   __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_malloc_is_new_array =
@@ -241,9 +233,6 @@ void *__builtin_alloca(__CPROVER_size_t alloca_size)
   void *res;
   res = __CPROVER_allocate(alloca_size, 0);
 
-  // make sure it's not recorded as deallocated
-  __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
-
   // record the object size for non-determistic bounds checking
   __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
   __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;

src/cpp/library/new.c

@@ -10,9 +10,6 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
   void *res;
   res = __CPROVER_allocate(malloc_size, 0);
 
-  // ensure it's not recorded as deallocated
-  __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
-
   // non-deterministically record the object for delete/delete[] checking
   __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
   __CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;
@@ -37,9 +34,6 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
   void *res;
   res = __CPROVER_allocate(size*count, 0);
 
-  // ensure it's not recorded as deallocated
-  __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
-
   // non-deterministically record the object for delete/delete[] checking
   __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
   __CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;