@@ -130,10 +130,6 @@ __CPROVER_HIDE:;
130130 // and __CPROVER_allocate doesn't, but no one cares
131131 malloc_res = __CPROVER_allocate (alloc_size , 1 );
132132
133- // make sure it's not recorded as deallocated
134- __CPROVER_deallocated =
135- (malloc_res == __CPROVER_deallocated ) ? 0 : __CPROVER_deallocated ;
136-
137133 // record the object size for non-determistic bounds checking
138134 __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool ();
139135 __CPROVER_malloc_is_new_array =
@@ -194,10 +190,6 @@ __CPROVER_HIDE:;
194190 void * malloc_res ;
195191 malloc_res = __CPROVER_allocate (malloc_size , 0 );
196192
197- // make sure it's not recorded as deallocated
198- __CPROVER_deallocated =
199- (malloc_res == __CPROVER_deallocated ) ? 0 : __CPROVER_deallocated ;
200-
201193 // record the object size for non-determistic bounds checking
202194 __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool ();
203195 __CPROVER_malloc_is_new_array =
@@ -225,9 +217,6 @@ void *__builtin_alloca(__CPROVER_size_t alloca_size)
225217 void * res ;
226218 res = __CPROVER_allocate (alloca_size , 0 );
227219
228- // make sure it's not recorded as deallocated
229- __CPROVER_deallocated = (res == __CPROVER_deallocated )?0 :__CPROVER_deallocated ;
230-
231220 // record the object size for non-determistic bounds checking
232221 __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool ();
233222 __CPROVER_malloc_is_new_array = record_malloc ?0 :__CPROVER_malloc_is_new_array ;
0 commit comments