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 9be817a176adb7a298e680bd34b5eda223b13f7a..af6673a426cda78cf8740e301124ba37ba25f106 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
@@ -171,7 +171,7 @@ static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
   /* Lift stack limit to account for extra stack memory overhead.  */
   increase_stack_limit(get_stack_size()*2);
   /* Allocate and log shadow memory layout of the execution */
-  init_memory_layout(argc_ref, argv_ref);
+  init_shadow_layout(argc_ref, argv_ref);
   /* Make sure the layout holds */
   DVALIDATE_SHADOW_LAYOUT;
   /* Track program arguments. */
@@ -190,7 +190,7 @@ static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
 }
 
 static void memory_clean(void) {
-  clean_memory_layout();
+  clean_shadow_layout();
 }
 
 /* }}} */
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 3bc186850f953d816c87fb00107a50f2b441615b..80507862558a3a0483da8a239799c24ae73b72cb 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
@@ -224,11 +224,11 @@ static const uint64_t static_readonly_masks [] = {
       "Heap base address %a is unaligned", _addr)
 
 #define DVALIDATE_MEMORY_INIT \
-  DVASSERT(mem_layout.initialized != 0, "Un-initialized shadow layout", NULL)
+  DVASSERT(shd_layout.initialized != 0, "Un-initialized shadow layout", NULL)
 
 /* Debug function making sure that the order of program segments is as expected
  * and that the program and the shadow segments used do not overlap. */
-static void validate_memory_layout() {
+static void validate_shadow_layout() {
   /* Check that the struct holding memory layout is marked as initialized. */
   DVALIDATE_MEMORY_INIT;
   /* Make sure the order of program segments is as expected, i.e.,
@@ -236,17 +236,17 @@ static void validate_memory_layout() {
 
   #define NO_MEM_SEGMENTS 11
   uintptr_t segments[NO_MEM_SEGMENTS][2] = {
-     {mem_layout.stack.start, mem_layout.stack.end},
-     {mem_layout.stack.prim_start, mem_layout.stack.prim_end},
-     {mem_layout.stack.sec_start, mem_layout.stack.sec_end},
-     {mem_layout.tls.start, mem_layout.tls.end},
-     {mem_layout.tls.prim_start, mem_layout.tls.prim_end},
-     {mem_layout.tls.sec_start, mem_layout.tls.sec_end},
-     {mem_layout.global.start, mem_layout.global.end},
-     {mem_layout.global.prim_start, mem_layout.global.prim_end},
-     {mem_layout.global.sec_start, mem_layout.global.sec_end},
-     {mem_layout.heap.start, mem_layout.heap.end},
-     {mem_layout.heap.prim_start, mem_layout.heap.prim_end}
+     {shd_layout.stack.start, shd_layout.stack.end},
+     {shd_layout.stack.prim_start, shd_layout.stack.prim_end},
+     {shd_layout.stack.sec_start, shd_layout.stack.sec_end},
+     {shd_layout.tls.start, shd_layout.tls.end},
+     {shd_layout.tls.prim_start, shd_layout.tls.prim_end},
+     {shd_layout.tls.sec_start, shd_layout.tls.sec_end},
+     {shd_layout.global.start, shd_layout.global.end},
+     {shd_layout.global.prim_start, shd_layout.global.prim_end},
+     {shd_layout.global.sec_start, shd_layout.global.sec_end},
+     {shd_layout.heap.start, shd_layout.heap.end},
+     {shd_layout.heap.prim_start, shd_layout.heap.prim_end}
   };
 
   /* Make sure all segments (shadow or otherwise) are disjoint */
@@ -265,17 +265,17 @@ static void validate_memory_layout() {
     }
   }
 
-  DVASSERT(mem_layout.stack.end > mem_layout.tls.end,
+  DVASSERT(shd_layout.stack.end > shd_layout.tls.end,
       "Unexpected location of stack (above tls)", NULL);
-  DVASSERT(mem_layout.tls.end > mem_layout.heap.end,
+  DVASSERT(shd_layout.tls.end > shd_layout.heap.end,
       "Unexpected location of tls (above heap)", NULL);
-  DVASSERT(mem_layout.heap.end > mem_layout.global.end,
+  DVASSERT(shd_layout.heap.end > shd_layout.global.end,
       "Unexpected location of heap (above global)", NULL);
 }
 
 /* Assert that memory layout has been initialized and all segments appear
  * in the expected order */
-# define DVALIDATE_SHADOW_LAYOUT validate_memory_layout()
+# define DVALIDATE_SHADOW_LAYOUT validate_shadow_layout()
 
 /* Assert that boundaries of a block [_addr, _addr+_size] are within a segment
  * given by `_s`. `_s` is either HEAP, STACK, TLS, GLOBAL or STATIC. */
@@ -423,7 +423,7 @@ static void validate_memory_layout() {
 
 /* Runtime assertions  {{{ */
 #define VALIDATE_HEAP_ALLOCATION(_res, _size) \
-  vassert(mem_layout.heap.end > (uintptr_t)_res + _size, \
+  vassert(shd_layout.heap.end > (uintptr_t)_res + _size, \
     "e-acsl error: Insufficient heap size %lu\n", E_ACSL_HEAP_SIZE);
 /* }}} */
 
@@ -1304,11 +1304,11 @@ static void print_memory_segment(struct memory_segment *seg, const char *name) {
     MB_SZ(seg->sec_size), seg->sec_start, seg->sec_end, seg->sec_offset);
 }
 
-static void print_memory_layout() {
-  print_memory_segment(&mem_layout.heap, "Heap");
-  print_memory_segment(&mem_layout.stack, "Stack");
-  print_memory_segment(&mem_layout.global, "Global");
-  print_memory_segment(&mem_layout.tls, "TLS");
+static void print_shadow_layout() {
+  print_memory_segment(&shd_layout.heap, "Heap");
+  print_memory_segment(&shd_layout.stack, "Stack");
+  print_memory_segment(&shd_layout.global, "Global");
+  print_memory_segment(&shd_layout.tls, "TLS");
   DLOG("-----------------------------------------------------\n");
 }
 
@@ -1335,7 +1335,7 @@ static const char* which_segment(uintptr_t addr) {
 /*! \brief Print program layout. This function outputs start/end addresses of
  * various program segments, their shadow counterparts and sizes of shadow
  * regions used. */
-#define DEBUG_PRINT_LAYOUT print_memory_layout()
+#define DEBUG_PRINT_LAYOUT print_shadow_layout()
 void ___e_acsl_debug_print_layout() { DEBUG_PRINT_LAYOUT; }
 
 /*! \brief Print the shadow segment address addr belongs to */
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 ef8d8ed379d90dd9ed383f40981e4a85d1d9bd84..af1481b6c9d65e45dea6f752d2ea118c5e3bb19f 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
@@ -306,14 +306,12 @@ struct memory_segment {
   uintptr_t sec_start; //!< Least address in the secondary shadow
   uintptr_t sec_end; //!< Greatest address in the secondary shadow
   uintptr_t sec_offset; //!< Secondary shadow offset
-
-  int initialized; //! Notion on whether the layout is initialized
 };
 
 /*! \brief Full program memory layout. */
-static struct memory_layout mem_layout;
+static struct shadow_layout shd_layout;
 
-struct memory_layout {
+struct shadow_layout {
   struct memory_segment heap;
   struct memory_segment stack;
   struct memory_segment global;
@@ -362,18 +360,18 @@ static void set_shadow_segment(struct memory_segment *seg, uintptr_t start,
 
 /*! \brief Initialize memory layout, i.e., determine bounds of program segments,
  * allocate shadow memory spaces and compute offsets. This function populates
- * global struct ::mem_layout holding that information with data. */
-static void init_memory_layout(int *argc_ref, char ***argv_ref) {
+ * global struct ::shd_layout holding that information with data. */
+static void init_shadow_layout(int *argc_ref, char ***argv_ref) {
   /* Use DEBUG_PRINT_LAYOUT to output the details */
-  set_shadow_segment(&mem_layout.heap,
+  set_shadow_segment(&shd_layout.heap,
     get_heap_start(), get_heap_size(), 1, 8, "heap");
-  set_shadow_segment(&mem_layout.stack,
+  set_shadow_segment(&shd_layout.stack,
     get_stack_start(argc_ref, argv_ref), get_stack_size(), 1, 1, "stack");
-  set_shadow_segment(&mem_layout.global,
+  set_shadow_segment(&shd_layout.global,
     get_global_start(), get_global_size(), 1, 1, "global");
-  set_shadow_segment(&mem_layout.tls,
+  set_shadow_segment(&shd_layout.tls,
     get_tls_start(), get_tls_size(), 1, 1, "tls");
-  mem_layout.initialized = 1;
+  shd_layout.initialized = 1;
 }
 
 /*! \brief Deallocate a shadow segment */
@@ -385,12 +383,12 @@ void clean_memory_segment(struct memory_segment *seg) {
 }
 
 /*! \brief Deallocate shadow regions used by runtime analysis */
-static void clean_memory_layout() {
-  if (mem_layout.initialized) {
-    clean_memory_segment(&mem_layout.heap);
-    clean_memory_segment(&mem_layout.stack);
-    clean_memory_segment(&mem_layout.global);
-    clean_memory_segment(&mem_layout.tls);
+static void clean_shadow_layout() {
+  if (shd_layout.initialized) {
+    clean_memory_segment(&shd_layout.heap);
+    clean_memory_segment(&shd_layout.stack);
+    clean_memory_segment(&shd_layout.global);
+    clean_memory_segment(&shd_layout.tls);
   }
 }
 /* }}} */
@@ -447,27 +445,27 @@ static void clean_memory_layout() {
 
 /*! \brief Convert a stack address into its primary shadow counterpart */
 #define PRIMARY_STACK_SHADOW(_addr) \
-  LOWER_SHADOW_ACCESS(_addr, mem_layout.stack.prim_offset)
+  LOWER_SHADOW_ACCESS(_addr, shd_layout.stack.prim_offset)
 
 /*! \brief Convert a stack address into its secondary shadow counterpart */
 #define SECONDARY_STACK_SHADOW(_addr) \
-  LOWER_SHADOW_ACCESS(_addr, mem_layout.stack.sec_offset)
+  LOWER_SHADOW_ACCESS(_addr, shd_layout.stack.sec_offset)
 
 /*! \brief Convert a global address into its primary shadow counterpart */
 #define PRIMARY_GLOBAL_SHADOW(_addr)  \
-  HIGHER_SHADOW_ACCESS(_addr, mem_layout.global.prim_offset)
+  HIGHER_SHADOW_ACCESS(_addr, shd_layout.global.prim_offset)
 
 /*! \brief Convert a global address into its secondary shadow counterpart */
 #define SECONDARY_GLOBAL_SHADOW(_addr) \
-  HIGHER_SHADOW_ACCESS(_addr, mem_layout.global.sec_offset)
+  HIGHER_SHADOW_ACCESS(_addr, shd_layout.global.sec_offset)
 
 /*! \brief Convert a TLS address into its primary shadow counterpart */
 #define PRIMARY_TLS_SHADOW(_addr)  \
-  LOWER_SHADOW_ACCESS(_addr, mem_layout.tls.prim_offset)
+  LOWER_SHADOW_ACCESS(_addr, shd_layout.tls.prim_offset)
 
 /*! \brief Convert a TLS address into its secondary shadow counterpart */
 #define SECONDARY_TLS_SHADOW(_addr) \
-  LOWER_SHADOW_ACCESS(_addr, mem_layout.tls.sec_offset)
+  LOWER_SHADOW_ACCESS(_addr, shd_layout.tls.sec_offset)
 
 /* \brief Compute a primary or a secondary shadow address (based on the value of
  * parameter `_region`) of an address tracked via an offset-based encoding.
@@ -484,16 +482,16 @@ static void clean_memory_layout() {
 
 /*! \brief Convert a heap address into its shadow counterpart */
 #define HEAP_SHADOW(_addr) \
-  HIGHER_SHADOW_ACCESS(_addr, mem_layout.heap.prim_offset)
+  HIGHER_SHADOW_ACCESS(_addr, shd_layout.heap.prim_offset)
 
-#define HEAP_START mem_layout.heap.start
+#define HEAP_START shd_layout.heap.start
 
 /*! \brief Convert a heap address into its init shadow counterpart */
 #define HEAP_INIT_SHADOW(_addr) \
   HIGHER_SCALED_SHADOW_ACCESS(_addr, \
-      mem_layout.heap.start, \
-      mem_layout.heap.sec_offset, \
-      mem_layout.heap.sec_ratio)
+      shd_layout.heap.start, \
+      shd_layout.heap.sec_offset, \
+      shd_layout.heap.sec_ratio)
 
 /* }}} */
 
@@ -501,7 +499,7 @@ static void clean_memory_layout() {
 /*! \brief Evaluate to a true value if address _addr resides within a given
  * memory segment.
  * \param _addr - a memory address
- * \param _seg - a memory segment (one of the structs within ::mem_layout)
+ * \param _seg - a memory segment (one of the structs within ::shd_layout)
 */
 #define IS_ON(_addr,_seg) ( \
   ((uintptr_t)_addr) >= _seg.start && \
@@ -509,16 +507,16 @@ static void clean_memory_layout() {
 )
 
 /*! \brief Evaluate to true if `_addr` is a heap address */
-#define IS_ON_HEAP(_addr) IS_ON(_addr, mem_layout.heap)
+#define IS_ON_HEAP(_addr) IS_ON(_addr, shd_layout.heap)
 
 /*! \brief Evaluate to true if `_addr` is a stack address */
-#define IS_ON_STACK(_addr) IS_ON(_addr, mem_layout.stack)
+#define IS_ON_STACK(_addr) IS_ON(_addr, shd_layout.stack)
 
 /*! \brief Evaluate to true if `_addr` is a global address */
-#define IS_ON_GLOBAL(_addr) IS_ON(_addr, mem_layout.global)
+#define IS_ON_GLOBAL(_addr) IS_ON(_addr, shd_layout.global)
 
 /*! \brief Evaluate to true if _addr is a TLS address */
-#define IS_ON_TLS(_addr) IS_ON(_addr, mem_layout.tls)
+#define IS_ON_TLS(_addr) IS_ON(_addr, shd_layout.tls)
 
 /*! \brief Shortcut for evaluating an address via ::IS_ON_STACK,
  * ::IS_ON_GLOBAL or ::IS_ON_TLS  */