From c3e05b161e5da4e6ca30457304e687547b355019 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 May 2022 14:51:14 +0000 Subject: [PATCH] Remove unnecessary __CPROVER_deallocated updates We always allocated fresh objects, it is impossible for the condition in these assignments to be true. --- src/ansi-c/library/stdlib.c | 11 ----------- src/cpp/library/new.c | 6 ------ 2 files changed, 17 deletions(-) diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index 6454ef92383..f9535fb094f 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -130,10 +130,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 = @@ -194,10 +190,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 = @@ -225,9 +217,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; diff --git a/src/cpp/library/new.c b/src/cpp/library/new.c index 673311c60f5..1f623058581 100644 --- a/src/cpp/library/new.c +++ b/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;