Skip to content

Commit 1fdaf6f

Browse files
committed
Remove unnecessary __CPROVER_deallocated updates
We always allocated fresh objects, it is impossible for the condition in these assignments to be true.
1 parent 1cfc93f commit 1fdaf6f

File tree

2 files changed

+0
-17
lines changed

2 files changed

+0
-17
lines changed

src/ansi-c/library/stdlib.c

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -112,10 +112,6 @@ __CPROVER_HIDE:;
112112
// and __CPROVER_allocate doesn't, but no one cares
113113
malloc_res = __CPROVER_allocate(alloc_size, 1);
114114

115-
// make sure it's not recorded as deallocated
116-
__CPROVER_deallocated =
117-
(malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
118-
119115
// record the object size for non-determistic bounds checking
120116
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
121117
__CPROVER_malloc_is_new_array =
@@ -174,10 +170,6 @@ __CPROVER_HIDE:;
174170
void *malloc_res;
175171
malloc_res = __CPROVER_allocate(malloc_size, 0);
176172

177-
// make sure it's not recorded as deallocated
178-
__CPROVER_deallocated =
179-
(malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
180-
181173
// record the object size for non-determistic bounds checking
182174
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
183175
__CPROVER_malloc_is_new_array =
@@ -205,9 +197,6 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
205197
void *res;
206198
res = __CPROVER_allocate(alloca_size, 0);
207199

208-
// make sure it's not recorded as deallocated
209-
__CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
210-
211200
// record the object size for non-determistic bounds checking
212201
__CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
213202
__CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;

src/cpp/library/new.c

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,6 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
1010
void *res;
1111
res = __CPROVER_allocate(malloc_size, 0);
1212

13-
// ensure it's not recorded as deallocated
14-
__CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
15-
1613
// non-deterministically record the object for delete/delete[] checking
1714
__CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
1815
__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)
3734
void *res;
3835
res = __CPROVER_allocate(size*count, 0);
3936

40-
// ensure it's not recorded as deallocated
41-
__CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
42-
4337
// non-deterministically record the object for delete/delete[] checking
4438
__CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
4539
__CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;

0 commit comments

Comments
 (0)