From b832f69c70da2542d11e29c01eef732bf5fc6539 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 2 Aug 2017 10:57:38 +0200
Subject: [PATCH] Sync interfaces for ALLOCATED and WRITEABLE debug macros
across models
---
.../bittree_model/e_acsl_bittree_mmodel.c | 18 +++++++++---------
.../e-acsl/share/e-acsl/e_acsl_temporal.h | 6 +++---
.../segment_model/e_acsl_segment_tracking.h | 12 ++++++------
3 files changed, 18 insertions(+), 18 deletions(-)
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 84b4c945a42..3a91e0b56c7 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
@@ -43,21 +43,21 @@
#define E_ACSL_MMODEL_DESC "patricia trie"
/* Assertions in debug mode */
-#define ALLOCATED(_ptr,_size) \
- ((allocated(_ptr, _size, _ptr) == NULL) ? 0 : 1)
+#define ALLOCATED(_ptr,_size, _base) \
+ ((allocated(_ptr, _size, _base) == NULL) ? 0 : 1)
#ifdef E_ACSL_DEBUG
-#define DVALIDATE_ALLOCATED(_ptr, _size) \
- vassert(ALLOCATED(_ptr, _size), \
+#define DVALIDATE_ALLOCATED(_ptr, _size, _base) \
+ vassert(ALLOCATED(_ptr, _size, _base), \
"Not allocated [%a, %a + %lu]", (uintptr_t)_ptr, _size)
-#define DVALIDATE_WRITEABLE(_ptr, _size) { \
- DVALIDATE_ALLOCATED(_ptr, _size); \
+#define DVALIDATE_WRITEABLE(_ptr, _size, _base) { \
+ DVALIDATE_ALLOCATED(_ptr, _size, _base); \
vassert(!readonly(_ptr), "Location %a is read-only", (uintptr_t)_ptr); \
}
#else
-#define DVALIDATE_ALLOCATED(_ptr, _size)
-#define DVALIDATE_WRITEABLE(_ptr, _size)
+#define DVALIDATE_ALLOCATED(_ptr, _size, _base)
+#define DVALIDATE_WRITEABLE(_ptr, _size, _base)
#endif
/**************************/
@@ -435,7 +435,7 @@ int posix_memalign(void **memptr, size_t alignment, size_t size) {
return -1;
/* Make sure that the first argument to posix memalign is indeed allocated */
- DVALIDATE_WRITEABLE((void*)memptr, sizeof(void*));
+ DVALIDATE_WRITEABLE((void*)memptr, sizeof(void*), (void*)memptr);
int res = public_posix_memalign(memptr, alignment, size);
if (!res)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal.h
index c31d8197a84..a53c01337d8 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal.h
@@ -66,8 +66,8 @@ void temporal_memcpy(void *dest, void *src, size_t size) {
/* Memcpy is only relevant for pointers here, so if there is a
* copy under a pointer's size then there no point in copying memory*/
if (size >= sizeof(void*)) {
- DVALIDATE_RO_ACCESS(src, size);
- DVALIDATE_RW_ACCESS(dest, size);
+ DVALIDATE_ALLOCATED(src, size, src);
+ DVALIDATE_WRITEABLE(dest, size, dest);
void *dest_shadow = (void *)temporal_referent_shadow(dest);
void *src_shadow = (void *)temporal_referent_shadow(src);
memcpy(dest_shadow, src_shadow, size);
@@ -75,7 +75,7 @@ void temporal_memcpy(void *dest, void *src, size_t size) {
}
void temporal_memset(void *dest, int c, size_t size) {
- DVALIDATE_RW_ACCESS(dest, size);
+ DVALIDATE_WRITEABLE(dest, size, dest);
void *dest_shadow = (void *)temporal_referent_shadow(dest);
memset(dest_shadow, 0, size);
}
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index f1a03d0df9b..9803865072c 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
@@ -357,16 +357,16 @@ static void validate_shadow_layout() {
} \
}
-/* Assert that neither of `_len` addresses immediately preceding `_addr` are
- * base addresses of some other block and that `_len` addresses past
+/* Assert that neither of `_len - 1` addresses immediately preceding `_addr`
+ * are base addresses of some other block and that `_len` addresses past
* `_addr` are free */
#define DVALIDATE_STATIC_SUFFICIENTLY_ALIGNED(_addr, _len) { \
int _i; \
for (_i = 0; _i < _len; _i++) { \
- uintptr_t _prev = _addr - _i - 1; \
+ uintptr_t _prev = _addr - _i; \
if (static_allocated_one(_prev)) { \
vassert(_base_addr(_prev) != _prev, \
- "Potential backward overlap of: \n previous block [%a]\n" \
+ "Potential backward overlap of: \n previous block [%a]\n" \
" with allocated block [%a]\n", _prev, _addr); \
} \
uintptr_t _next = _addr + _i; \
@@ -389,8 +389,8 @@ static void validate_shadow_layout() {
/* Assert that memory block [_addr, _addr + _size] is allocated
* and can be written to */
-# define DVALIDATE_WRITEABLE(_addr, _size) { \
- DVALIDATE_ALLOCATED((uintptr_t)_addr, _size, (uintptr_t)_addr); \
+# define DVALIDATE_WRITEABLE(_addr, _size, _base) { \
+ DVALIDATE_ALLOCATED((uintptr_t)_addr, _size, (uintptr_t)_base); \
DVASSERT(!readonly((void*)_addr), \
"Unexpected readonly address: %lu\n", _addr); \
}
--
GitLab