Skip to content

Commit c3e05b1

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 d932d6f commit c3e05b1

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
@@ -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;

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)