Hide __CPROVER_deallocated updates behind a function

This avoids repeating similar code in several places.

Author: tautschnig

src/ansi-c/ansi_c_internal_additions.cpp

@@ -179,6 +179,7 @@ void ansi_c_internal_additions(std::string &code)
     "void *" CPROVER_PREFIX "allocate("
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
     "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
+    "void " CPROVER_PREFIX "deallocate(void *);\n"
 
     CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
     integer2string(max_malloc_size(config.ansi_c.pointer_width, config

src/ansi-c/library/cprover.h

@@ -19,6 +19,7 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t;
 typedef signed long long __CPROVER_ssize_t;
 
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
+void __CPROVER_deallocate(void *);
 extern const void *__CPROVER_deallocated;
 extern const void *__CPROVER_new_object;
 extern __CPROVER_bool __CPROVER_malloc_is_new_array;

src/ansi-c/library/mman.c

@@ -112,8 +112,7 @@ int munmap(void *addr, __CPROVER_size_t length)
 {
   (void)length;
 
-  if(__VERIFIER_nondet___CPROVER_bool())
-    __CPROVER_deallocated = addr;
+  __CPROVER_deallocate(addr);
 
   return 0;
 }
@@ -126,8 +125,7 @@ int _munmap(void *addr, __CPROVER_size_t length)
 {
   (void)length;
 
-  if(__VERIFIER_nondet___CPROVER_bool())
-    __CPROVER_deallocated = addr;
+  __CPROVER_deallocate(addr);
 
   return 0;
 }

src/ansi-c/library/stdlib.c

@@ -271,9 +271,7 @@ inline void free(void *ptr)
 
   if(ptr!=0)
   {
-    // non-deterministically record as deallocated
-    __CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
-    if(record) __CPROVER_deallocated=ptr;
+    __CPROVER_deallocate(ptr);
 
     // detect memory leaks
     if(__CPROVER_memory_leak==ptr)
@@ -590,3 +588,13 @@ __CPROVER_HIDE:;
   __CPROVER_assume(result >= 0);
   return result;
 }
+
+/* FUNCTION: __CPROVER_deallocate */
+
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+
+void __CPROVER_deallocate(void *ptr)
+{
+  if(__VERIFIER_nondet___CPROVER_bool())
+    __CPROVER_deallocated = ptr;
+}

src/cpp/library/new.c

@@ -88,9 +88,7 @@ inline void __delete(void *ptr)
   // This is a requirement by the standard, not generosity!
   if(ptr!=0)
   {
-    // non-deterministically record as deallocated
-    __CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
-    __CPROVER_deallocated=record?ptr:__CPROVER_deallocated;
+    __CPROVER_deallocate(ptr);
 
     // detect memory leaks
     if(__CPROVER_memory_leak==ptr)
@@ -125,9 +123,7 @@ inline void __delete_array(void *ptr)
 
   if(ptr!=0)
   {
-    // non-deterministically record as deallocated
-    __CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
-    __CPROVER_deallocated=record?ptr:__CPROVER_deallocated;
+    __CPROVER_deallocate(ptr);
 
     // detect memory leaks
     if(__CPROVER_memory_leak==ptr) __CPROVER_memory_leak=0;