From 9ef3540efebc74b91b68b24585814dc172f9481a Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Tue, 17 Jan 2017 10:58:39 +0100
Subject: [PATCH] Definition of __e_acsl_store_block_duplicate API function
---
.../e-acsl/bittree_model/e_acsl_bittree_mmodel.c | 12 ++++++++++++
src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h | 10 ++++++++++
.../e-acsl/segment_model/e_acsl_segment_mmodel.c | 9 +++++++++
3 files changed, 31 insertions(+)
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 21985b94e1c..b35e8dc11f8 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/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)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index 46a375dc46c..f19c4294999 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/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)
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
index a740e1e360c..4699f2d8171 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+++ b/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)
--
GitLab