diff --git a/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c b/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c
index f05688d7fc9cbba53422e2fdeefbc93bb1f0f094..98744d443fadc8c52dab25fc317429e08d95c466 100644
--- a/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c
+++ b/src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.c
@@ -9,6 +9,12 @@
            ftp://gee.cs.oswego.edu/pub/misc/malloc.c
          Check before installing!
 
+* This file has been modified by CEA for use together with Runtime Library
+  of the E-ACSL plugin of Frama-C.
+  The changes introduced by CEA are limited to the following modifications:
+    * Added declaration/definition of mspace_least_addr function
+    * Added functionality to modify prefix of `mspace_...` functions
+
 * Quickstart
 
   This library is all in one file to simplify the most common usage:
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index d868d9de0203f46139c64d144857d773c6d731f1..57d94f16286f5e90c8b30681510fae6714eef2c0 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -330,16 +330,15 @@ let add_assert env stmt annot = match current_kf env with
       env.visitor#get_filling_actions
 
 let add_stmt ?(post=false) ?(init=false) ?before env stmt =
-  if post = false then begin
-    Extlib.may (fun old -> E_acsl_label.move env.visitor ~old stmt) before
-  end;
+  if not post then
+    Extlib.may (fun old -> E_acsl_label.move env.visitor ~old stmt) before;
   let local_env, tl = top init env in
   let block = local_env.block_info in
   let block =
-    if post = false then
-      { block with new_stmts = stmt :: block.new_stmts }
-    else
+    if post then
       { block with post_stmts = stmt :: block.post_stmts }
+    else
+      { block with new_stmts = stmt :: block.new_stmts }
   in
   let local_env = { local_env with block_info = block } in
   { env with
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 8bdf605326cb7a56b169933b9619fa6d4f0f47e4..f6fa2ebbdf4c9dafc7615815f3d902f28be4b122 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
@@ -40,21 +40,24 @@
 #endif
 /* }}} */
 
+#define E_ACSL_MMODEL_DESC "patricia trie"
+
 /* Assertions in debug mode */
 #define ALLOCATED(_ptr,_size) \
   ((allocated(_ptr, _size, _ptr) == NULL) ? 0 : 1)
 
 #ifdef E_ACSL_DEBUG
-#define DVALIDATE_RO_ACCESS(_ptr, _size) \
+#define DVALIDATE_ALLOCATED(_ptr, _size) \
   vassert(ALLOCATED(_ptr, _size), \
   "Not allocated [%a, %a + %lu]", (uintptr_t)_ptr, _size)
-#define DVALIDATE_RW_ACCESS(_ptr, _size) { \
-  DVALIDATE_RO_ACCESS(_ptr, _size); \
+
+#define DVALIDATE_WRITEABLE(_ptr, _size) { \
+  DVALIDATE_ALLOCATED(_ptr, _size); \
   vassert(!readonly(_ptr), "Location %a is read-only", (uintptr_t)_ptr); \
 }
 #else
-#define DVALIDATE_RO_ACCESS(_ptr, _size)
-#define DVALIDATE_RW_ACCESS(_ptr, _size)
+#define DVALIDATE_ALLOCATED(_ptr, _size)
+#define DVALIDATE_WRITEABLE(_ptr, _size)
 #endif
 
 /**************************/
@@ -71,7 +74,7 @@ static const int nbr_bits_to_1[256] = {
 };
 
 /* given the size of the memory block (_size) return (or rather evaluate to)
- * size in bytes requred to represent its partial initialization */
+ * size in bytes required to represent its partial initialization */
 #define needed_bytes(_size) \
   ((_size % 8) == 0 ? (_size/8) : (_size/8 + 1))
 /* }}} */
@@ -432,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_RW_ACCESS((void*)memptr, sizeof(void*));
+  DVALIDATE_WRITEABLE((void*)memptr, sizeof(void*));
 
   int res = public_posix_memalign(memptr, alignment, size);
   if (!res)
@@ -539,6 +542,7 @@ void memory_clean() {
   report_heap_leaks();
 }
 
+/* POSIX-compliant array of character pointers to the environment strings. */
 extern char **environ;
 
 /* add `argv` to the memory model */
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
index 3685c9d990b78cdff2404a3d11b55759c493e107..b8fb641f374d31982d2b3c6fdbd26f7a6ff6bebe 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
@@ -51,7 +51,7 @@ static void vabort(char *fmt, ...);
 #define vassert(expr, fmt, ...) \
   vassert_fail(expr, __LINE__, __FILE__, fmt, __VA_ARGS__)
 
-/* This gets replaced by `abort` */
+/* This ::exec_abort replaces `abort` via a macro at the top of this file */
 static void exec_abort(int line, const char *file) {
 #ifdef E_ACSL_DEBUG
   trace();
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
index 1ec6aec4ab5cb62334331166a7c2936913d356b3..1e7459cf2e91d1a77586a3c2df61c19769786b1a 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
@@ -33,8 +33,8 @@
 #include <stddef.h>
 
 /* Memory allocated for internal use of RTL and for the use by the application
- * is split into to mspaces (memory spaces). Memory allocation itself is
- * delegated to a slightly cusomised version of dlmalloc shipped with the
+ * is split into two mspaces (memory spaces). Memory allocation itself is
+ * delegated to a slightly customised version of dlmalloc shipped with the
  * RTL. The overall pattern is as follows:
  *    mspace space = create_mspace(capacity, locks);
  *    char *p = mspace_malloc(space, size); */
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 d84b6aa2b770a2faca75a1d5992807c4ea0323ae..5087e0e39613408a6dc378457990afad0fd69624 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
@@ -198,7 +198,7 @@ int freeable(void * ptr)
 /*! \brief Implementation of the \b \\valid predicate of E-ACSL.
  *
  * \\valid evaluates an expression of the form `p+i`, where `p` is a pointer
- * and `i` is an integer offset and returns `true` of both `p` and `p+i` belong
+ * and `i` is an integer offset and returns `true` if both `p` and `p+i` belong
  * to the same allocated memory block.
  *
  * @param ptr - memory address under question
@@ -208,7 +208,7 @@ int freeable(void * ptr)
  *  `base` refers to `p`
  *  @param addrof_base - if `ptr` can be represented by the expression `p+i`
  *  then `addrof_base` refers to `&p`. For the cases when the address of `p`
- *  cannot be taked (e.g., address of s static array or a constant value
+ *  cannot be taken (e.g., address of a static array or a constant value
  *  casted to a pointer) then `addrof_base` is zero.
  *
  * @returns
@@ -218,6 +218,9 @@ int freeable(void * ptr)
  *  then only region `[ptr, ptr + size]` should lie within the same block
  *  and be writable.
  */
+
+/* FIXME: The following E-ACSL contract is obsolete and needs to be
+   synchronized with the above description. */
 /*@ ensures \result == 0 || \result == 1;
   @ ensures \result == 1 ==> \valid(((char *)ptr)+(0..size-1));
   @ assigns \result \from *(((char*)ptr)+(0..size-1)); */
@@ -228,6 +231,9 @@ int valid(void * ptr, size_t size, void *base, void *addrof_base)
  *
  * Same as ::valid except the checked memory locations are only
  * required to be allocated.  */
+
+/* FIXME: The following E-ACSL contract is obsolete and needs to be
+   synchronized with the above description. */
 /*@ ensures \result == 0 || \result == 1;
   @ ensures \result == 1 ==> \valid_read(((char *)ptr)+(0..size-1));
   @ assigns \result \from *(((char*)ptr)+(0..size-1)); */
@@ -295,7 +301,7 @@ size_t get_heap_allocation_size(void)
 /*! \brief A variable holding a byte size of tracked heap allocation. */
 extern size_t heap_allocation_size;
 
-/*@predicate diffSize{L1,L2}(integer i) =
+/*@ predicate diffSize{L1,L2}(integer i) =
   \at(heap_allocation_size, L1)
     - \at(heap_allocation_size, L2) == i; */
 
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
index 740c9da96caad32a10f2834822272fc7e8921509..55db362411c22848166f9fe4974c86782c5c279e 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
@@ -49,10 +49,10 @@
  *      E_ACSL_BITTREE_MMODEL - use Patricia-trie (tree-based) memory model, or
  *      E_ACSL_SEGMENT_MMODEL - use segment-based (shadow) memory model
  *    Verbosity level:
- *      E_ACSL_VERBOSE - is set puts an executable in verbose mode (which
- *        may print some extra messages
+ *      E_ACSL_VERBOSE - put an executable in verbose mode that
+ *        prints extra messages (unset by default)
  *    Debug Features:
- *      E_ACSL_DEBUG - enable debug features in RTL
+ *      E_ACSL_DEBUG - enable debug features in RTL (unset by default)
  *      E_ACSL_DEBUG_VERBOSE - verbose debug output (via DVLOG macro)
  *      E_ACSL_DEBUG_LOG - name of the log file where debug messages are
  *        output. The file name should be unquoted string with '-'
@@ -62,7 +62,7 @@
  *        Given an expression `(p+i)`, where `p` is a pointer and `i` is an
  *        integer offset weak validity indicates that `(p+i)` is valid if it
  *        belongs to memory allocation. In strong validity `(p+i)` is valid
- *        iff both `p` and `(p+i)` belong to memory allocation and to one
+ *        iff both `p` and `(p+i)` belong to memory allocation and to the same
  *        memory block.
  *    Temporal analysis:
  *      E_ACSL_TEMPORAL - enable temporal analysis in RTL
@@ -120,12 +120,10 @@ static void describe_run() {
 #if defined(E_ACSL_VERBOSE) || defined(E_ACSL_DEBUG)
   rtl_printf("/* ========================================================= */\n");
   rtl_printf(" * E-ACSL instrumented run\n" );
+  rtl_printf(" * Memory tracking: %s\n", E_ACSL_MMODEL_DESC);
 #ifdef E_ACSL_SEGMENT_MMODEL
-  rtl_printf(" * Memory tracking: shadow memory with\n" );
   rtl_printf(" *   Heap  %d MB\n", E_ACSL_HEAP_SIZE);
   rtl_printf(" *   Stack %d MB\n", E_ACSL_STACK_SIZE);
-#else
-  rtl_printf(" * Memory tracking: patricia trie\n" );
 #endif
   rtl_printf(" * Temporal checks: %s\n", E_ACSL_TEMPORAL_DESC);
   rtl_printf(" * Execution mode:  %s\n", E_ACSL_DEBUG_DESC);
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 3ca4e0ecfeb0ac25fbbb92bbd3babdf3c128cb21..2a7729f97dc83dd07b1eec84aaaa9e0b5dc2fb86 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,8 @@
 #include "e_acsl_shadow_layout.h"
 #include "e_acsl_segment_tracking.h"
 
+#define E_ACSL_MMODEL_DESC "shadow memory"
+
 #define ALLOCATED(_ptr,_size) allocated((uintptr_t)_ptr, _size, (uintptr_t)_ptr)
 
 void * store_block(void * ptr, size_t size) {
@@ -138,6 +140,8 @@ int initialized(void * ptr, size_t size) {
 /* }}} */
 
 /* Track program arguments (ARGC/ARGV) {{{ */
+
+/* POSIX-compliant array of character pointers to the environment strings. */
 extern char ** environ;
 
 static void argv_alloca(int *argc_ref,  char *** argv_ref) {
@@ -153,6 +157,7 @@ static void argv_alloca(int *argc_ref,  char *** argv_ref) {
 
   /* Track argument strings */
   while (*argv) {
+    /* Account for `\0` when copying C strings */
     size_t arglen = strlen(*argv) + 1;
 #ifdef E_ACSL_TEMPORAL
     /* Move `argv` strings to heap. This is because they are allocated
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 f3d33a53ded3cea5069a4c5837272979895e9fe3..94101e24955198fce58609d2e54b8303fd14e488 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
@@ -232,6 +232,9 @@ static void validate_shadow_layout() {
   /* Check that the struct holding memory layout is marked as initialized. */
   DVALIDATE_MEMORY_INIT;
 
+  /* Each segment has 3 partitions:
+	 - application memory
+     - primary/secondary shadows */
   int num_partitions = sizeof(mem_partitions)/sizeof(memory_partition*);
   int num_seg_in_part = 3;
 #ifdef E_ACSL_TEMPORAL
@@ -354,13 +357,13 @@ static void validate_shadow_layout() {
   } \
 }
 
-/* Assert neither of `_len` addresses immediately preceding `_addr` are
+/* Assert that neither of `_len` 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; \
+    uintptr_t _prev = _addr - _i - 1; \
     if (static_allocated_one(_prev)) { \
       vassert(_base_addr(_prev) != _prev, \
         "Potential backward overlap of: \n  previous block       [%a]\n" \
@@ -386,16 +389,12 @@ static void validate_shadow_layout() {
 
 /* Assert that memory block [_addr, _addr + _size] is allocated
  * and can be written to */
-# define DVALIDATE_RW_ACCESS(_addr, _size) { \
+# define DVALIDATE_WRITEABLE(_addr, _size) { \
   DVALIDATE_ALLOCATED((uintptr_t)_addr, _size, (uintptr_t)_addr); \
   DVASSERT(!readonly((void*)_addr), \
     "Unexpected readonly address: %lu\n", _addr); \
 }
 
-/* Assert that memory block [_addr, _addr + _size] is allocated */
-# define DVALIDATE_RO_ACCESS(_addr, _size) \
-  DVALIDATE_ALLOCATED((uintptr_t)_addr, _size, (uintptr_t)_addr)
-
 #else
 /*! \cond exclude from doxygen */
 #  define DVALIDATE_MEMORY_INIT
@@ -414,9 +413,8 @@ static void validate_shadow_layout() {
 #  define DVALIDATE_FREEABLE
 #  define DVALIDATE_STATIC_FREE
 #  define DVALIDATE_HEAP_FREE
-#  define DVALIDATE_RO_ACCESS
-#  define DVALIDATE_RW_ACCESS
 #  define DVALIDATE_ALLOCATED
+#  define DVALIDATE_WRITEABLE
 #  define DVALIDATE_STATIC_SUFFICIENTLY_ALIGNED
 /*! \endcond */
 #endif
@@ -931,7 +929,9 @@ void* calloc(size_t nmemb, size_t size) {
   return res;
 }
 
-/** \brief Return shadowed copy of a memory chunk on a program's heap */
+/** \brief Return shadowed copy of a memory chunk on a program's heap using.
+ * If `init` parameter is set to a non-zero value the memory occupied by the
+ * resulting block is set to be initialized and uninitialized otherwise. */
 static void *shadow_copy(const void *ptr, size_t size, int init) {
   char *ret = (init) ?	calloc(1, size) : malloc(size);
   vassert(ret != NULL, "Shadow copy failed\n", NULL);
@@ -946,10 +946,16 @@ static void *shadow_copy(const void *ptr, size_t size, int init) {
 
 /*! \brief Remove a memory block with base address given by `ptr` from tracking.
  * This function effectively nullifies block shadow tracking an application
- * block and optionally nullifies an init shadow associated with the block.
+ * block.
  *
  * NOTE: ::unset_heap_segment assumes that `ptr` is a base address of an
- * allocated heap memory block, i.e., `freeable(ptr)` evaluates to true. */
+ * allocated heap memory block, i.e., `freeable(ptr)` evaluates to true.
+ *
+ * \param ptr - base address of the memory block to be removed from tracking
+ * \param init - if evaluated to a non-zero value then initialization shadow
+ *  of the memory block with base address `ptr` is nullified as well.
+ * \param function - name of the de-allocation function (e.g., `free` or `cfree`)
+*/
 static void unset_heap_segment(void *ptr, int init, const char *function) {
   DVALIDATE_MEMORY_INIT;
   DVALIDATE_FREEABLE(((uintptr_t)ptr));
@@ -1127,7 +1133,11 @@ static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr) {
      *  after base address)
      * offset is the difference between the address and base address (shadow[0])
      * Then an address belongs to heap allocation if
-     *  offset + size <= length */
+     *  offset + size <= length
+     *
+     * Additionally, if strong validity is enforced
+     * (i.e., E_ACSL_WEAK_VALIDITY macro undefined) make sure that both
+     * `addr` and `base_ptr` belong to the same block. */
 #ifndef E_ACSL_WEAK_VALIDITY
     return base_shadow[0] == shadow[0] &&
       (addr - shadow[0]) + size <= first_segment[1];
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
index 32df2970324dcf537aae4521a76ef599a1cd1b6b..76572755eb4713dd7e76010ce430e616b3568ab6 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h
@@ -139,6 +139,8 @@ static size_t increase_stack_limit(const size_t size) {
         vabort("setrlimit: %s \n", strerror(errno));
       }
     }
+  } else {
+    vabort("getrlimit: %s \n", strerror(errno));
   }
   return size;
 }
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 27c055e1b1ce114282c7eef3aa723c17e420ab29..91a22644d4de57561c6c2a3b2300ce3bfd3998f3 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -413,7 +413,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
               (* Case of an empty CompoundInit, treat it as if there were
                * no initializer at all *)
               | CompoundInit(_,[]) -> ()
-              | _ -> Varinfo.Hashtbl.add global_vars vi (off, (Some i)))
+              | CompoundInit(_,_) | SingleInit _ ->
+                Varinfo.Hashtbl.add global_vars vi (off, (Some i)))
             | false-> ());
             is_initializer <- false;
           i)