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 84b4c945a42d75b6c6fe41d408dc3a266816433f..3a91e0b56c72837a7e697e98e3b2229db0d6572d 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 c31d8197a84ffedefe46120ae7acbc5edc489cff..a53c01337d8fcb758eea5ee4ea610d63d9770696 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 f1a03d0df9b027b55c47504fea78c2c4a2f677b1..9803865072cdd133dd46d488bd81b63b271be4b9 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); \
 }