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 6a9c7c655cee406a57b3935e602f9e2ffdc91c79..dcbcd31994740c244779015c585b614e21844217 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
@@ -39,6 +39,7 @@ static int valid(void * ptr, size_t size);
 #include "e_acsl_debug.h"
 #include "e_acsl_malloc.h"
 #include "e_acsl_shadow_layout.h"
+#include "e_acsl_safe_locations.h"
 #include "e_acsl_segment_tracking.h"
 #include "e_acsl_mmodel_api.h"
 
@@ -72,7 +73,7 @@ static int valid(void * ptr, size_t size) {
   uintptr_t addr = (uintptr_t)ptr;
   if (IS_ON_HEAP(addr))
     return heap_allocated(addr, size);
-  else if (IS_ON_STACK(addr))
+  else if (IS_ON_STACK(addr) || IS_ON_TLS(addr))
     return static_allocated(addr, size);
   else if (IS_ON_GLOBAL(addr))
     return static_allocated(addr, size) && !global_readonly(addr);
@@ -150,6 +151,16 @@ static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
   /* Track program arguments. */
   if (argc_ref && argv_ref)
     argv_alloca(*argc_ref, *argv_ref);
+  /* Tracking safe locations */
+  collect_safe_locations();
+  int i;
+  for (i = 0; i < safe_location_counter; i++) {
+    void *addr = (void*)safe_locations[i].address;
+    uintptr_t len = safe_locations[i].length;
+    shadow_alloca(addr, len);
+    if (safe_locations[i].initialized)
+      initialize(addr, len);
+  }
 }
 
 static void memory_clean(void) {
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 fc55e67f3390a41d41547cada10a0a93731cb304..7f3cc35ef7c35107b0ee4f9a73b55f3f6fb49a5f 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
@@ -34,10 +34,10 @@
  * \b FIXME: in the current implementation there might be issues with segment
  * size greater than 64 bytes. This is because presently some initialization
  * functionality relies on the fact that initialization per segment can be set
- * and/or evaluated using 8-byte bitmask. */
+ * and/or evaluated using an 8-byte bitmask. */
 #define HEAP_SEGMENT 16
 
-/*! \brief Number of required to represent initialization of a segment. */
+/*! \brief Number of bytes required to represent initialization of a segment. */
 #define INIT_BYTES (HEAP_SEGMENT/8)
 
 /*! \brief Size (in bytes) of a long block on the stack. */
@@ -1158,8 +1158,8 @@ static void print_memory_layout() {
 }
 
 /*! \brief Output the shadow segment the address belongs to */
-static void which_segment(uintptr_t addr) {
-  char *loc = NULL;
+static const char* which_segment(uintptr_t addr) {
+  const char *loc = NULL;
   if (IS_ON_STACK(addr))
     loc = "stack";
   else if (IS_ON_HEAP(addr))
@@ -1170,7 +1170,7 @@ static void which_segment(uintptr_t addr) {
     loc = "TLS";
   else
     loc = "untracked";
-  DLOG("Address: %a -> %s\n", addr, loc);
+  return loc;
 }
 
 /* NOTE: Above functions are designed to be used only through the following
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 84378b423313e79bc1869a186474ce517e24919e..f648c00c9d38ccc4e87f8d40fb22a5d87cfe8a98 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
@@ -396,11 +396,11 @@ static void clean_memory_layout() {
 
 /*! \brief Convert a TLS address into its primary shadow counterpart */
 #define PRIMARY_TLS_SHADOW(_addr)  \
-  HIGHER_SHADOW_ACCESS(_addr, mem_layout.tls.prim_offset)
+  LOWER_SHADOW_ACCESS(_addr, mem_layout.tls.prim_offset)
 
 /*! \brief Convert a TLS address into its secondary shadow counterpart */
 #define SECONDARY_TLS_SHADOW(_addr) \
-  HIGHER_SHADOW_ACCESS(_addr, mem_layout.tls.sec_offset)
+  LOWER_SHADOW_ACCESS(_addr, mem_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.