Definition of __e_acsl_store_block_duplicate API function

src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c

@@ -314,6 +314,17 @@ static void delete_block(void* ptr) {
     }
   }
 }
+
+static void* store_block_duplicate(void* ptr, size_t size) {
+  if (ptr != NULL) {
+    bt_block * tmp = bt_lookup(ptr);
+    if (tmp)
+      delete_block(tmp);
+    store_block(ptr, size);
+  }
+  return ptr;
+}
+
 /* }}} */
 
 /* HEAP ALLOCATION {{{ */
@@ -566,6 +577,7 @@ strong_alias(bittree_aligned_alloc, aligned_alloc)
 /* Explicit tracking */
 public_alias(delete_block)
 public_alias(store_block)
+public_alias(store_block_duplicate)
 /* Predicates */
 public_alias(offset)
 public_alias(base_addr)

src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h

@@ -82,6 +82,16 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
 void * __e_acsl_store_block(void * ptr, size_t size)
   __attribute__((FC_BUILTIN));
 
+/*! \brief Same as `__e_acsl_store_block`, but first check
+ * checks whether a block with a base address given by `ptr` exists in the
+ * tracked allocation and remove it before storing a new block.
+ *
+ * \param ptr base address of the tracked memory block
+ * \param size size of the tracked block in bytes */
+/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
+void * __e_acsl_store_block_duplicate(void * ptr, size_t size)
+  __attribute__((FC_BUILTIN));
+
 /*! \brief Remove a memory block which base address is \p ptr from tracking. */
 /*@ assigns \nothing; */
 void __e_acsl_delete_block(void * ptr)

src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c

@@ -31,6 +31,7 @@
 #include <sys/resource.h>
 
 static int valid(void * ptr, size_t size);
+static int valid_read(void * ptr, size_t size);
 
 #include "e_acsl_string.h"
 #include "e_acsl_bits.h"
@@ -57,6 +58,13 @@ static void delete_block(void * ptr) {
   shadow_freea(ptr);
 }
 
+static void * store_block_duplicate(void * ptr, size_t size) {
+  if (valid_read(ptr, size))
+    delete_block(ptr);
+  shadow_alloca(ptr, size);
+  return ptr;
+}
+
 static void full_init(void * ptr) {
   initialize(ptr, block_length(ptr));
 }
@@ -180,6 +188,7 @@ strong_alias(shadow_posix_memalign, posix_memalign)
 /* Explicit tracking */
 public_alias(delete_block)
 public_alias(store_block)
+public_alias(store_block_duplicate)
 /* Predicates */
 public_alias2(segment_offset, offset)
 public_alias2(segment_base_addr, base_addr)