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 7e74611ac5ee19b82530640f0ffa594151660c7b..4317ace0b93bc35b60ff88efe31380acb44035b1 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
@@ -25,6 +25,14 @@
 # define _DEFAULT_SOURCE 1
 #endif
 
+/* On Windows, setup minimum version to Windows 8 (or Server 2012) to be able to
+   use some specific API functions.
+   Check directly for windows instead of using E_ACSL_OS_IS_WINDOWS so that it
+   can be done without including anything. */
+#if defined(WIN32) || defined(_WIN32) || defined(__WIN32)
+# define _WIN32_WINNT 0x0602
+#endif
+
 // Internals
 #include "internals/e_acsl_bits.c"
 #include "internals/e_acsl_debug.c"
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c
index 0c42873864c1d7b89465dcc26403ac252afb3de3..3389f05f78e8d93125ba3759ce1baf45771047d4 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.c
@@ -24,6 +24,7 @@
 #include <fcntl.h>
 
 #include "../observation_model/internals/e_acsl_omodel_debug.h"
+#include "e_acsl_config.h"
 #include "e_acsl_private_assert.h"
 #include "e_acsl_rtl_io.h"
 
@@ -45,8 +46,13 @@ void initialize_report_file(int *argc, char ***argv) {
   if (!strcmp(dlog_name, "-") || !strcmp(dlog_name, "1")) {
     dlog_fd = 2;
   } else {
-    dlog_fd = open(dlog_name, O_WRONLY | O_CREAT | O_TRUNC  |O_NONBLOCK
+#if E_ACSL_OS_IS_LINUX
+    dlog_fd = open(dlog_name, O_WRONLY | O_CREAT | O_TRUNC | O_NONBLOCK
       | O_NOCTTY, S_IRUSR | S_IWUSR | S_IRGRP | S_IWGRP | S_IROTH | S_IWOTH);
+#elif E_ACSL_OS_IS_WINDOWS
+    dlog_fd = _open(dlog_name, _O_WRONLY | _O_CREAT | _O_TRUNC,
+      _S_IREAD | _S_IWRITE);
+#endif
   }
   if (dlog_fd == -1)
     private_abort("Cannot open file descriptor for %s\n", dlog_name);
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c
index 94516feab171db3523c2e71ce28f0fefd575cfb6..b5133be6fdc26828abba82fa819ce520af351ac9 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c
@@ -20,16 +20,12 @@
 /*                                                                        */
 /**************************************************************************/
 
-/* Get default definitions and macros e.g., PATH_MAX */
-// #ifndef _DEFAULT_SOURCE
-// # define _DEFAULT_SOURCE 1
-// #endif
-
 #include <limits.h>
 #include <signal.h>
 #include <stdarg.h>
 #include <stddef.h>
 
+#include "e_acsl_config.h"
 #include "e_acsl_rtl_io.h"
 #include "e_acsl_trace.h"
 
@@ -54,14 +50,18 @@ void raise_abort(const char *file, int line) {
 
 void private_abort_fail(const char * file, int line, char *fmt, ...) {
   va_list va;
+#if E_ACSL_OS_IS_LINUX
   sigset_t defer_abrt;
   sigemptyset(&defer_abrt);
   sigaddset(&defer_abrt,SIGABRT);
   sigprocmask(SIG_BLOCK,&defer_abrt,NULL);
+#endif // E_ACSL_OS_IS_LINUX
   va_start(va,fmt);
   rtl_veprintf(fmt, va);
   va_end(va);
+#if E_ACSL_OS_IS_LINUX
   sigprocmask(SIG_UNBLOCK,&defer_abrt,NULL);
+#endif // E_ACSL_OS_IS_LINUX
   raise_abort(file, line);
 }
 
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c
index e13e8dfdaa1972564d400fdb2d673294841a18cf..77f1b91237ebb27d9c8d6610089f6c2e190fd6fa 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.c
@@ -25,6 +25,11 @@
  * \brief Implementation for running shell commands
 ***************************************************************************/
 
+#include "e_acsl_config.h"
+
+// Only available on linux
+#if E_ACSL_OS_IS_LINUX
+
 #include <errno.h>
 #include <stddef.h>
 #include <sys/types.h>
@@ -201,3 +206,5 @@ ipr_t* shexec (char **data, const char *sin) {
   /* Run the command returning a pointer to `ipr_t` */
   return __shexec(ipr);
 }
+
+#endif // E_ACSL_OS_IS_LINUX
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h
index 16cb2d9a1d3a0161bc39ca0159d03962d07a8a00..754cabb418656fbde4bbfc1cb8a6bd9dbc85780b 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_shexec.h
@@ -28,6 +28,11 @@
 #ifndef E_ACSL_SHEXEC_H
 #define E_ACSL_SHEXEC_H
 
+#include "e_acsl_config.h"
+
+// Only available on linux
+#if E_ACSL_OS_IS_LINUX
+
 #include <sys/types.h>
 
 /*! \class ipr_t
@@ -68,4 +73,6 @@ typedef struct {
  *  `free_ipr` function. */
 ipr_t* shexec (char **data, const char *sin);
 
+#endif // E_ACSL_OS_IS_LINUX
+
 #endif // E_ACSL_SHEXEC_H
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
index 486c9458cac9e2dc8023efb358b5b13e312a6f70..64336e758bd4f23af52d118a5a8854be7985bed3 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
@@ -36,6 +36,7 @@
 
 #include "e_acsl_trace.h"
 
+#if E_ACSL_OS_IS_LINUX
 extern void  *__libc_stack_end;
 
 struct frame_layout {
@@ -70,6 +71,7 @@ static int native_backtrace (void **array, int size) {
   }
   return cnt;
 }
+#endif
 
 void trace() {
 # if E_ACSL_OS_IS_LINUX
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
index a605bbdb95f10e6f31fb443915653495c2e7ae4a..e0dcc56094698aaf8d1c0df34008a8b6d4ee2ee6 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
@@ -25,12 +25,24 @@
  * \brief Patricia Trie API Implementation
 ***************************************************************************/
 
+#include "../../internals/e_acsl_config.h"
 #include "../../internals/e_acsl_malloc.h"
 #include "../../internals/e_acsl_private_assert.h"
 
 #include "e_acsl_bittree.h"
 
+#if E_ACSL_OS_IS_LINUX
 #define WORDBITS __WORDSIZE
+#elif E_ACSL_OS_IS_WINDOWS
+// On windows, __WORDSIZE is not available
+# ifdef _WIN64
+#   define WORDBITS 64
+# else
+#   define WORDBITS 32
+# endif
+#else
+# error "Unsupported OS"
+#endif
 
 static size_t mask(size_t, size_t);
 
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
index e729c281313b6d416e029212f012a2cc90f31695..1f6296b66387b1971aa988af762766526fe9e681 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
@@ -587,11 +587,13 @@ void eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
   int i;
   for (i = 0; i < get_safe_locations_count(); i++) {
     memory_location * loc = get_safe_location(i);
-    void *addr = (void*)loc->address;
-    uintptr_t len = loc->length;
-    eacsl_store_block(addr, len);
-    if (loc->is_initialized)
-      eacsl_initialize(addr, len);
+    if (loc->is_on_static) {
+      void *addr = (void*)loc->address;
+      uintptr_t len = loc->length;
+      eacsl_store_block(addr, len);
+      if (loc->is_initialized)
+        eacsl_initialize(addr, len);
+    }
   }
   init_infinity_values();
 }
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
index 86d1ad4e0a63e4cc6c1b927e520a7f6877e2c4cd..9c2e61b587126620383f4c16337b7a457d4a3f58 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
@@ -23,6 +23,7 @@
 #include <stdio.h>
 #include <errno.h>
 
+#include "../../internals/e_acsl_config.h"
 #include "e_acsl_safe_locations.h"
 
 /* An array storing safe locations up to `safe_location_counter` position.
@@ -31,18 +32,20 @@
 static memory_location safe_locations [16];
 static int safe_location_counter = 0;
 
-#define add_safe_location(_addr,_len,_init) { \
+#define add_safe_location(_addr,_len,_init,_on_static) do { \
   safe_locations[safe_location_counter].address = _addr; \
   safe_locations[safe_location_counter].length = _len; \
+  safe_locations[safe_location_counter].is_initialized = _init; \
+  safe_locations[safe_location_counter].is_on_static = _on_static; \
   safe_location_counter++; \
-}
+} while (0)
 
 void collect_safe_locations() {
   /* Tracking of errno and standard streams */
-  add_safe_location((uintptr_t)&errno, sizeof(int), "errno");
-  add_safe_location((uintptr_t)stdout, sizeof(FILE), "stdout");
-  add_safe_location((uintptr_t)stderr, sizeof(FILE), "stderr");
-  add_safe_location((uintptr_t)stdin, sizeof(FILE), "stdin");
+  add_safe_location((uintptr_t)&errno, sizeof(int), 1, E_ACSL_OS_IS_LINUX);
+  add_safe_location((uintptr_t)stdout, sizeof(FILE), 1, E_ACSL_OS_IS_LINUX);
+  add_safe_location((uintptr_t)stderr, sizeof(FILE), 1, E_ACSL_OS_IS_LINUX);
+  add_safe_location((uintptr_t)stdin, sizeof(FILE), 1, E_ACSL_OS_IS_LINUX);
 }
 
 size_t get_safe_locations_count() {
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
index fa24ba37f875a71bbdf3d110be9d8054f47d5741..1b34dab3f464665b0b03c0ba6ac6e7a79960aada 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
@@ -34,11 +34,17 @@
 #include <stdint.h>
 #include <stddef.h>
 
-/* Simple representation of a safe location */
+/*! Simple representation of a safe location */
 struct memory_location {
-  uintptr_t address; /* Address */
-  uintptr_t length; /* Byte-length */
-  int is_initialized; /* Notion of initialization */
+  /*! Address */
+  uintptr_t address;
+  /*! Byte-length */
+  uintptr_t length;
+  /*! Notion of initialization */
+  int is_initialized;
+  /*! True if the address is on static memory, false if it is on dynamic
+      memory */
+  int is_on_static;
 };
 typedef struct memory_location memory_location;
 
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
index 87e369e22b43f37edb1567fb21ffe9f4f204a764..5dfcd7efd90c29821dfd16f131c1531c90a8b7b3 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
@@ -215,8 +215,8 @@ void mspaces_init() {
     describe_run();
     eacsl_make_memory_spaces(64*MB, get_heap_size());
     /* Allocate and log shadow memory layout of the execution.
-       Case of the heap, globals and tls. */
-    init_shadow_layout_heap_global_tls();
+       Case of the segments available before main. */
+    init_shadow_layout_pre_main();
     already_run = 1;
   }
 }
@@ -235,8 +235,9 @@ void eacsl_memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
     initialize_report_file(argc_ref, argv_ref);
     /* 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. Case of stack. */
-    init_shadow_layout_stack(argc_ref, argv_ref);
+    /* Allocate and log shadow memory layout of the execution. Case of the
+       segments available after main. */
+    init_shadow_layout_main(argc_ref, argv_ref);
     //DEBUG_PRINT_LAYOUT;
     /* Make sure the layout holds */
     DVALIDATE_SHADOW_LAYOUT;
@@ -250,12 +251,14 @@ void eacsl_memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
     collect_safe_locations();
     int i;
     for (i = 0; i < get_safe_locations_count(); i++) {
-    memory_location * loc = get_safe_location(i);
-      void *addr = (void*)loc->address;
-      uintptr_t len = loc->length;
-      shadow_alloca(addr, len);
-      if (loc->is_initialized)
-        eacsl_initialize(addr, len);
+      memory_location * loc = get_safe_location(i);
+      if (loc->is_on_static) {
+        void *addr = (void*)loc->address;
+        uintptr_t len = loc->length;
+        shadow_alloca(addr, len);
+        if (loc->is_initialized)
+          eacsl_initialize(addr, len);
+      }
     }
     init_infinity_values();
     already_run = 1;
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c
index 9be75d5bb9e087c6eda750aed9e13e53c3fc02cd..d6be5cd96e4abbc8a2202e9fa44ad4b7b1139b0d 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c
@@ -20,6 +20,7 @@
 /*                                                                        */
 /**************************************************************************/
 
+#include "../../internals/e_acsl_bits.h"
 #include "../../internals/e_acsl_rtl_io.h"
 #include "e_acsl_segment_tracking.h"
 #include "e_acsl_shadow_layout.h"
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
index 852f1447084e3b2569b4c28eb681abfe3f7bb06b..6e3011ce48c98c4637fcc3259b094df2c0cd8188 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
@@ -345,14 +345,6 @@ void shadow_freea(void *ptr) {
 
 /* Static querying {{{ */
 
-/*! \brief Checking whether a globally allocated memory block containing an
- * address _addr has read-only access. Note, this is light checking that
- * relies on the fact that a single block cannot contain read/write and
- * read-only parts, that is to check whether the block has read-only access it
- * is sufficient to check any of its bytes. */
-#define global_readonly(_addr) \
-  checkbit(READONLY_BIT, (*(char*)PRIMARY_GLOBAL_SHADOW(addr)))
-
 int static_allocated(uintptr_t addr, long size, uintptr_t base_ptr) {
   unsigned char *prim_shadow = (unsigned char*)PRIMARY_SHADOW(addr);
   /* Unless the address belongs to tracked allocation 0 is returned */
@@ -557,7 +549,7 @@ static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
   private_assert(mem_spaces.heap_end > max_addr,
     "Exceeded heap allocation limit of %luMB\n", E_ACSL_HEAP_SIZE);
 
-  DVALIDATE_MEMORY_INIT;
+  DVALIDATE_MEMORY_PRE_MAIN_INIT;
   /* Ensure the shadowed block in on the tracked heap portion */
   DVALIDATE_IS_ON_HEAP(((uintptr_t)ptr) - HEAP_SEGMENT, size);
   DVALIDATE_ALIGNMENT(ptr); /* Make sure alignment is right */
@@ -664,7 +656,7 @@ void *shadow_copy(const void *ptr, size_t size, int init) {
  * \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_MEMORY_PRE_MAIN_INIT;
   DVALIDATE_FREEABLE(((uintptr_t)ptr));
   /* Base address of shadow block */
   uintptr_t *base_shadow = (uintptr_t*)HEAP_SHADOW(ptr);
@@ -1134,10 +1126,23 @@ void print_shadow_layout() {
   print_memory_partition(&mem_layout.heap);
   DLOG(">>> STACK --------------------\n");
   print_memory_partition(&mem_layout.stack);
+#if E_ACSL_OS_IS_LINUX
   DLOG(">>> GLOBAL -------------------\n");
   print_memory_partition(&mem_layout.global);
   DLOG(">>> TLS ----------------------\n");
   print_memory_partition(&mem_layout.tls);
+#elif E_ACSL_OS_IS_WINDOWS
+  DLOG(">>> TEXT ---------------------\n");
+  print_memory_partition(&mem_layout.text);
+  DLOG(">>> BSS ----------------------\n");
+  print_memory_partition(&mem_layout.bss);
+  DLOG(">>> DATA --------------------\n");
+  print_memory_partition(&mem_layout.data);
+  DLOG(">>> IDATA --------------------\n");
+  print_memory_partition(&mem_layout.idata);
+  DLOG(">>> RDATA --------------------\n");
+  print_memory_partition(&mem_layout.rdata);
+#endif
   DLOG(">>> --------------------------\n");
 }
 
@@ -1147,10 +1152,23 @@ const char* which_segment(uintptr_t addr) {
     loc = "stack";
   else if (IS_ON_HEAP(addr))
     loc = "heap";
+#if E_ACSL_OS_IS_LINUX
   else if (IS_ON_GLOBAL(addr))
     loc = "global";
   else if (IS_ON_TLS(addr))
     loc = "TLS";
+#elif E_ACSL_OS_IS_WINDOWS
+  else if (IS_ON_TEXT(addr))
+    loc = "text";
+  else if (IS_ON_BSS(addr))
+    loc = "bss";
+  else if (IS_ON_DATA(addr))
+    loc = "data";
+  else if (IS_ON_IDATA(addr))
+    loc = "idata";
+  else if (IS_ON_RDATA(addr))
+    loc = "rdata";
+#endif
   else
     loc = "untracked";
   return loc;
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
index 4379e1cda6f1baa4d0783ba51654a0a788245248..0baf6b56c0f0942270575031dadcf9756bc79db5 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
@@ -114,8 +114,18 @@
   DVASSERT(((uintptr_t)_addr) % HEAP_SEGMENT == 0,  \
       "Heap base address %a is unaligned", _addr)
 
+#define DVALIDATE_MEMORY_PRE_MAIN_INIT \
+  DVASSERT(mem_layout.is_initialized_pre_main != 0, \
+           "Un-initialized pre-main shadow layout", NULL)
+
+#define DVALIDATE_MEMORY_MAIN_INIT \
+  DVASSERT(mem_layout.is_initialized_main != 0, \
+           "Un-initialized main shadow layout", NULL)
+
 #define DVALIDATE_MEMORY_INIT \
-  DVASSERT(mem_layout.is_initialized != 0, "Un-initialized shadow layout", NULL)
+  DVASSERT(mem_layout.is_initialized_pre_main != 0 && \
+           mem_layout.is_initialized_main != 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. */
@@ -137,12 +147,24 @@ void validate_shadow_layout();
 /* Assert that [_addr, _addr+_size] are within stack segment */
 #define DVALIDATE_IS_ON_STACK(_addr, _size) \
   DVALIDATE_IS_ON(_addr, _size, STACK)
+#if E_ACSL_OS_IS_LINUX
 /* Assert that [_addr, _addr+_size] are within global segment */
-#define DVALIDATE_IS_ON_GLOBAL(_addr, _size) \
+# define DVALIDATE_IS_ON_GLOBAL(_addr, _size) \
   DVALIDATE_IS_ON(_addr, _size, GLOBAL)
 /* Assert that [_addr, _addr+_size] are within TLS segment */
-#define DVALIDATE_IS_ON_TLS(_addr, _size) \
+# define DVALIDATE_IS_ON_TLS(_addr, _size) \
   DVALIDATE_IS_ON(_addr, _size, TLS)
+#elif E_ACSL_OS_IS_WINDOWS
+/* Assert that [_addr, _addr+_size] are within text segment */
+# define DVALIDATE_IS_ON_TEXT(_addr, _size) \
+  DVALIDATE_IS_ON(_addr, _size, TEXT)
+/* Assert that [_addr, _addr+_size] are within bss segment */
+# define DVALIDATE_IS_ON_BSS(_addr, _size) \
+  DVALIDATE_IS_ON(_addr, _size, BSS)
+/* Assert that [_addr, _addr+_size] are within idata segment */
+# define DVALIDATE_IS_ON_IDATA(_addr, _size) \
+  DVALIDATE_IS_ON(_addr, _size, IDATA)
+#endif
 /* Assert that [_addr, _addr+_size] are within stack, global or TLS segments */
 #define DVALIDATE_IS_ON_STATIC(_addr, _size) \
   DVALIDATE_IS_ON(_addr, _size, STATIC)
@@ -222,6 +244,8 @@ void validate_shadow_layout();
 
 #else
 /*! \cond exclude from doxygen */
+#  define DVALIDATE_MEMORY_PRE_MAIN_INIT
+#  define DVALIDATE_MEMORY_MAIN_INIT
 #  define DVALIDATE_MEMORY_INIT
 #  define DVALIDATE_SHADOW_LAYOUT
 #  define DVALIDATE_HEAP_ACCESS
@@ -231,8 +255,14 @@ void validate_shadow_layout();
 #  define DVALIDATE_IS_ON
 #  define DVALIDATE_IS_ON_HEAP
 #  define DVALIDATE_IS_ON_STACK
+#  if E_ACSL_OS_IS_LINUX
 #  define DVALIDATE_IS_ON_GLOBAL
 #  define DVALIDATE_IS_ON_TLS
+#  elif E_ACSL_OS_IS_WINDOWS
+#    define DVALIDATE_IS_ON_TEXT
+#    define DVALIDATE_IS_ON_BSS
+#    define DVALIDATE_IS_ON_IDATA
+#  endif
 #  define DVALIDATE_IS_ON_STATIC
 #  define DVALIDATE_FREEABLE
 #  define DVALIDATE_STATIC_FREE
@@ -309,6 +339,14 @@ void shadow_freea(void *ptr);
 
 /* Static querying {{{ */
 
+/*! \brief Checking whether a globally allocated memory block containing an
+ * address _addr has read-only access. Note, this is light checking that
+ * relies on the fact that a single block cannot contain read/write and
+ * read-only parts, that is to check whether the block has read-only access it
+ * is sufficient to check any of its bytes. */
+#define global_readonly(_addr) \
+  checkbit(READONLY_BIT, (*(char*)PRIMARY_GLOBAL_SHADOW(_addr)))
+
 /*! \brief Return a non-zero value if a memory region of length `size`
  * starting at address `addr` belongs to a tracked stack, tls or
  * global memory block and 0 otherwise.
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
index e070180edfc3d7f90a539120704675f210a28a6c..fa02c208e9d4f261498edd720e5e786d46617c14 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
@@ -20,7 +20,6 @@
 /*                                                                        */
 /**************************************************************************/
 
-#include <sys/resource.h>
 #include <errno.h>
 #include <stddef.h>
 
@@ -29,8 +28,23 @@
 
 #include "e_acsl_shadow_layout.h"
 
+#if E_ACSL_OS_IS_LINUX
+
+#include <sys/resource.h>
+
 /** Program stack information {{{ */
 
+/* Symbols exported by the linker script */
+
+/*!\brief The first address past the end of the text segment. */
+extern char etext;
+/*!\brief The first address past the end of the initialized data segment. */
+extern char edata;
+/*!\brief The first address past the end of the uninitialized data segment. */
+extern char end;
+/*!\brief The first address of a program. */
+extern char __executable_start;
+
 size_t increase_stack_limit(const size_t size) {
   rlim_t stacksz = (rlim_t)size;
   struct rlimit rl;
@@ -59,7 +73,15 @@ size_t get_stack_size() {
   return rlim.rlim_cur;
 }
 
-uintptr_t get_stack_start(int *argc_ref,  char *** argv_ref) {
+
+extern char ** environ;
+
+/*! \brief Return the greatest (known) address on a program's stack.
+ * This function presently determines the address using the address of the
+ * last string in `environ`. That is, it assumes that argc and argv are
+ * stored below environ, which holds for GCC/Glibc but is not necessarily
+ * true for some other compilers/libraries. */
+static uintptr_t get_stack_start(int *argc_ref,  char *** argv_ref) {
   char **env = environ;
   while (env[1])
     env++;
@@ -76,70 +98,54 @@ uintptr_t get_stack_start(int *argc_ref,  char *** argv_ref) {
 }
 /* }}} */
 
-/** Program heap information {{{ */
-uintptr_t get_heap_start() {
-  return mem_spaces.heap_start;
-}
-
-size_t get_heap_size() {
-  return PGM_HEAP_SIZE;
-}
-
-size_t get_heap_init_size() {
-  return get_heap_size()/8;
-}
-
-uintptr_t get_global_start() {
+/** Program global information {{{ */
+/*! \brief Return the start address of a segment holding globals (generally
+ * BSS and Data segments). */
+static uintptr_t get_global_start() {
   return (uintptr_t)&__executable_start;
 }
 
-size_t get_global_size() {
+/*! \brief Return byte-size of global segment */
+static size_t get_global_size() {
   return ((uintptr_t)&end - get_global_start());
 }
 /** }}} */
 
-/** Shadow Layout {{{ */
+/** Thread-local storage information {{{ */
 
-void set_application_segment(memory_segment *seg, uintptr_t start,
-    size_t size, const char *name, mspace msp) {
-  seg->name = name;
-  seg->start = start;
-  seg->size = size;
-  seg->end = seg->start + seg->size;
-  seg->mspace = msp;
-  seg->parent = NULL;
-  seg->shadow_ratio = 0;
-  seg->shadow_offset = 0;
-}
+/*! Thread-local storage (TLS) keeps track of copies of per-thread variables.
+ * Even though at the present stage, E-ACSL's RTL is not thread-safe, some
+ * of the variables (for instance ::errno) are allocated there. In X86, TLS
+ * is typically located somewhere below the program's stack but above mmap
+ * areas. TLS is typically separated into two sections: .tdata and .tbss.
+ * Similar to globals using .data and .bss, .tdata keeps track of initialized
+ * thread-local variables, while .tbss holds uninitialized ones.
+ *
+ * Start and end addresses of TLS are obtained by taking addresses of
+ * initialized and uninitialized variables in TLS (::id_tdata and ::id_tss)
+ * and adding fixed amount of shadow space around them. Visually it looks
+ * as follows:
+ *
+ *   end TLS address (&id_tdata + TLS_SHADOW_SIZE/2)
+ *   id_tdata address
+ *   ...
+ *   id_tbss address
+ *   start TLS address (&id_bss - TLS_SHADOW_SIZE/2)
+ *
+ * HOWEVER problems can occur if PGM_TLS_SIZE is too big:
+ * see get_tls_start for details.
+ */
 
-void set_shadow_segment(memory_segment *seg, memory_segment *parent,
-    size_t ratio, const char *name) {
-  seg->parent = parent;
-  seg->name = name;
-  seg->shadow_ratio = ratio;
-  seg->size = parent->size/seg->shadow_ratio;
-  seg->mspace = eacsl_create_mspace(seg->size + SHADOW_SEGMENT_PADDING, 0);
-  seg->start = (uintptr_t)eacsl_mspace_malloc(seg->mspace,1);
-  seg->end = seg->start + seg->size;
-  seg->shadow_offset = parent->start - seg->start;
+/*! \brief Return byte-size of the TLS segment */
+inline static size_t get_tls_size() {
+  return PGM_TLS_SIZE;
 }
 
-void init_shadow_layout_stack(int *argc_ref, char ***argv_ref) {
-  memory_partition *pstack = &mem_layout.stack;
-  set_application_segment(&pstack->application, get_stack_start(argc_ref, argv_ref),
-    get_stack_size(), "stack", NULL);
-  /* Changes of the ratio in the following will require changes in get_tls_start */
-  set_shadow_segment(&pstack->primary, &pstack->application, 1, "stack_primary");
-  set_shadow_segment(&pstack->secondary, &pstack->application, 1, "stack_secondary");
-#ifdef E_ACSL_TEMPORAL
-  set_shadow_segment(&pstack->temporal_primary, &pstack->application, 1, "temporal_stack_primary");
-  set_shadow_segment(&pstack->temporal_secondary, &pstack->application, 1, "temporal_stack_secondary");
-#endif
-
-  mem_layout.is_initialized = 1;
-}
+static __thread int id_tdata = 1;
+static __thread int id_tbss;
 
-uintptr_t get_tls_start() {
+/*! \brief Return start address of a program's TLS */
+static uintptr_t get_tls_start() {
   size_t tls_size = get_tls_size();
   uintptr_t data = (uintptr_t)&id_tdata,
             bss = (uintptr_t)&id_tbss;
@@ -173,17 +179,10 @@ uintptr_t get_tls_start() {
   return tls_start_half > max_shadow ? tls_start_half : max_shadow;
 }
 
-void init_shadow_layout_heap_global_tls() {
-  memory_partition *pheap = &mem_layout.heap;
-  set_application_segment(&pheap->application, get_heap_start(),
-    get_heap_size(), "heap", mem_spaces.heap_mspace);
-  set_shadow_segment(&pheap->primary, &pheap->application, 1, "heap_primary");
-  set_shadow_segment(&pheap->secondary, &pheap->application, 8, "heap_secondary");
-#ifdef E_ACSL_TEMPORAL
-  set_shadow_segment(&pheap->temporal_primary, &pheap->application, 1, "temporal_heap_primary");
-  set_shadow_segment(&pheap->temporal_secondary, &pheap->application, 1, "temporal_heap_secondary");
-#endif
+/* }}} */
 
+/** Memory partitions {{{ */
+static void init_shadow_layout_global() {
   memory_partition *pglobal = &mem_layout.global;
   set_application_segment(&pglobal->application, get_global_start(),
     get_global_size(), "global", NULL);
@@ -193,7 +192,9 @@ void init_shadow_layout_heap_global_tls() {
   set_shadow_segment(&pglobal->temporal_primary, &pglobal->application, 1, "temporal_global_primary");
   set_shadow_segment(&pglobal->temporal_secondary, &pglobal->application, 1, "temporal_global_secondary");
 #endif
+}
 
+static void init_shadow_layout_tls() {
   memory_partition *ptls = &mem_layout.tls;
   set_application_segment(&ptls->application, get_tls_start(),
     get_tls_size(), "tls", NULL);
@@ -203,12 +204,260 @@ void init_shadow_layout_heap_global_tls() {
   set_shadow_segment(&ptls->temporal_primary, &ptls->application, 1, "temporal_tls_primary");
   set_shadow_segment(&ptls->temporal_secondary, &ptls->application, 1, "temporal_tls_secondary");
 #endif
+}
+
+static void init_shadow_layout_stack(int *argc_ref, char ***argv_ref) {
+  memory_partition *pstack = &mem_layout.stack;
+  set_application_segment(&pstack->application, get_stack_start(argc_ref, argv_ref),
+    get_stack_size(), "stack", NULL);
+  /* Changes of the ratio in the following will require changes in get_tls_start */
+  set_shadow_segment(&pstack->primary, &pstack->application, 1, "stack_primary");
+  set_shadow_segment(&pstack->secondary, &pstack->application, 1, "stack_secondary");
+#ifdef E_ACSL_TEMPORAL
+  set_shadow_segment(&pstack->temporal_primary, &pstack->application, 1, "temporal_stack_primary");
+  set_shadow_segment(&pstack->temporal_secondary, &pstack->application, 1, "temporal_stack_secondary");
+#endif
+}
+/** }}} */
+#elif E_ACSL_OS_IS_WINDOWS
+
+#include <processthreadsapi.h>
+#include <windows.h>
+#include <dbghelp.h>
+
+
+/** Program segment informations {{{ */
+typedef struct mem_loc_info {
+  uintptr_t start;
+  size_t size;
+} mem_loc_info_t;
+
+static mem_loc_info_t get_section_info(HANDLE hModule, const char * section_name) {
+  // Get the location of the module's IMAGE_NT_HEADERS structure
+  IMAGE_NT_HEADERS *pNtHdr = ImageNtHeader(hModule);
+
+  // Section table immediately follows the IMAGE_NT_HEADERS
+  IMAGE_SECTION_HEADER *pSectionHdr = (IMAGE_SECTION_HEADER *)(pNtHdr + 1);
+
+  const char* imageBase = (const char*)hModule;
+  size_t scnNameSize = sizeof(pSectionHdr->Name);
+  char scnName[scnNameSize + 1];
+  // Enforce nul-termination for scn names that are the whole length of
+  // pSectionHdr->Name[]
+  scnName[scnNameSize] = '\0';
+
+  mem_loc_info_t res = { .start = 0, .size = 0 };
+
+  for (int scn = 0; scn < pNtHdr->FileHeader.NumberOfSections; ++scn, ++pSectionHdr) {
+    // Note: pSectionHdr->Name[] is 8-byte long. If the scn name is 8-byte
+    // long, ->Name[] will not be nul-terminated. For this reason, copy it to a
+    // local buffer that is nul-terminated to be sure we only print the real scn
+    // name, and no extra garbage beyond it.
+    strncpy(scnName, (const char*)pSectionHdr->Name, scnNameSize);
+
+    if (strcmp(scnName, section_name) == 0) {
+      res.start = (uintptr_t)imageBase + pSectionHdr->VirtualAddress;
+      res.size = pSectionHdr->Misc.VirtualSize;
+      break;
+    }
+  }
+
+  return res;
+}
+/** }}} */
+
+/** Program stack information {{{ */
+static mem_loc_info_t get_stack_mem_loc_info() {
+  ULONG_PTR low;
+  ULONG_PTR high;
+  GetCurrentThreadStackLimits(&low, &high);
+  return (mem_loc_info_t) {
+    .start = low,
+    .size = high - low + 1
+  };
+}
+
+size_t increase_stack_limit(const size_t size) {
+  size_t actual_size = get_stack_size();
+  if (actual_size < size) {
+    DLOG("Increasing stack size at runtime is unsupported on Windows.\n\
+      \t   Actual stack size: %lu\n\
+      \tRequested stack size: %lu\n",
+      actual_size, size);
+  }
+  return actual_size;
+}
+
+size_t get_stack_size() {
+  return get_stack_mem_loc_info().size;
+}
+/** }}} */
+
+/** Memory partitions {{{ */
+static void init_shadow_layout_stack(int *argc_ref, char ***argv_ref) {
+  memory_partition *pstack = &mem_layout.stack;
+  mem_loc_info_t stack_loc_info = get_stack_mem_loc_info();
+  set_application_segment(&pstack->application, stack_loc_info.start,
+    stack_loc_info.size, "stack", NULL);
+  set_shadow_segment(&pstack->primary, &pstack->application, 1, "stack_primary");
+  set_shadow_segment(&pstack->secondary, &pstack->application, 1, "stack_secondary");
+#ifdef E_ACSL_TEMPORAL
+  set_shadow_segment(&pstack->temporal_primary, &pstack->application, 1, "temporal_stack_primary");
+  set_shadow_segment(&pstack->temporal_secondary, &pstack->application, 1, "temporal_stack_secondary");
+#endif
+}
+
+static void init_shadow_layout_text(HMODULE module) {
+  // Retrieve mem loc info for the text section
+  mem_loc_info_t text = get_section_info(module, ".text");
+
+  memory_partition *ptext = &mem_layout.text;
+  set_application_segment(&ptext->application, text.start,
+    text.size, "text", NULL);
+  set_shadow_segment(&ptext->primary, &ptext->application, 1, "text_primary");
+  set_shadow_segment(&ptext->secondary, &ptext->application, 1, "text_secondary");
+#ifdef E_ACSL_TEMPORAL
+  set_shadow_segment(&ptext->temporal_primary, &ptext->application, 1, "temporal_text_primary");
+  set_shadow_segment(&ptext->temporal_secondary, &ptext->application, 1, "temporal_text_secondary");
+#endif
+}
+
+static void init_shadow_layout_bss(HMODULE module) {
+  // Retrieve mem loc info for the uninidialized data segment
+  mem_loc_info_t bss = get_section_info(module, ".bss");
+
+  memory_partition *pbss = &mem_layout.bss;
+  set_application_segment(&pbss->application, bss.start, bss.size, "bss", NULL);
+  set_shadow_segment(&pbss->primary, &pbss->application, 1, "bss_primary");
+  set_shadow_segment(&pbss->secondary, &pbss->application, 1, "bss_secondary");
+#ifdef E_ACSL_TEMPORAL
+  set_shadow_segment(&pbss->temporal_primary, &pbss->application, 1, "temporal_bss_primary");
+  set_shadow_segment(&pbss->temporal_secondary, &pbss->application, 1, "temporal_bss_secondary");
+#endif
+}
+
+static void init_shadow_layout_data(HMODULE module) {
+  // Retrieve mem loc info for the initialized data segment
+  mem_loc_info_t data = get_section_info(module, ".data");
+
+  memory_partition *pdata = &mem_layout.data;
+  set_application_segment(&pdata->application, data.start, data.size, "data", NULL);
+  set_shadow_segment(&pdata->primary, &pdata->application, 1, "data_primary");
+  set_shadow_segment(&pdata->secondary, &pdata->application, 1, "data_secondary");
+#ifdef E_ACSL_TEMPORAL
+  set_shadow_segment(&pdata->temporal_primary, &pdata->application, 1, "temporal_data_primary");
+  set_shadow_segment(&pdata->temporal_secondary, &pdata->application, 1, "temporal_data_secondary");
+#endif
+}
+
+static void init_shadow_layout_idata(HMODULE module) {
+  // Retrieve mem loc info for the initialized data segment
+  mem_loc_info_t idata = get_section_info(module, ".idata");
+
+  memory_partition *pidata = &mem_layout.idata;
+  set_application_segment(&pidata->application, idata.start, idata.size, "idata", NULL);
+  set_shadow_segment(&pidata->primary, &pidata->application, 1, "idata_primary");
+  set_shadow_segment(&pidata->secondary, &pidata->application, 1, "idata_secondary");
+#ifdef E_ACSL_TEMPORAL
+  set_shadow_segment(&pidata->temporal_primary, &pidata->application, 1, "temporal_idata_primary");
+  set_shadow_segment(&pidata->temporal_secondary, &pidata->application, 1, "temporal_idata_secondary");
+#endif
+}
+
+static void init_shadow_layout_rdata(HMODULE module) {
+  // Retrieve mem loc info for the initialized data segment
+  mem_loc_info_t rdata = get_section_info(module, ".rdata");
+
+  memory_partition *prdata = &mem_layout.rdata;
+  set_application_segment(&prdata->application, rdata.start, rdata.size, "rdata", NULL);
+  set_shadow_segment(&prdata->primary, &prdata->application, 1, "rdata_primary");
+  set_shadow_segment(&prdata->secondary, &prdata->application, 1, "rdata_secondary");
+#ifdef E_ACSL_TEMPORAL
+  set_shadow_segment(&prdata->temporal_primary, &prdata->application, 1, "temporal_rdata_primary");
+  set_shadow_segment(&prdata->temporal_secondary, &prdata->application, 1, "temporal_rdata_secondary");
+#endif
+}
+/** }}} */
+#endif
+
+/** Program heap information {{{ */
+static uintptr_t get_heap_start() {
+  return mem_spaces.heap_start;
+}
+
+size_t get_heap_size() {
+  return PGM_HEAP_SIZE;
+}
+
+static size_t get_heap_init_size() {
+  return get_heap_size()/8;
+}
+
+static void init_shadow_layout_heap() {
+  memory_partition *pheap = &mem_layout.heap;
+  set_application_segment(&pheap->application, get_heap_start(),
+    get_heap_size(), "heap", mem_spaces.heap_mspace);
+  set_shadow_segment(&pheap->primary, &pheap->application, 1, "heap_primary");
+  set_shadow_segment(&pheap->secondary, &pheap->application, 8, "heap_secondary");
+#ifdef E_ACSL_TEMPORAL
+  set_shadow_segment(&pheap->temporal_primary, &pheap->application, 1, "temporal_heap_primary");
+  set_shadow_segment(&pheap->temporal_secondary, &pheap->application, 1, "temporal_heap_secondary");
+#endif
+}
+/** }}} */
+
+/** Shadow Layout {{{ */
+
+void set_application_segment(memory_segment *seg, uintptr_t start,
+    size_t size, const char *name, mspace msp) {
+  seg->name = name;
+  seg->start = start;
+  seg->size = size;
+  seg->end = seg->start + seg->size;
+  seg->mspace = msp;
+  seg->parent = NULL;
+  seg->shadow_ratio = 0;
+  seg->shadow_offset = 0;
+}
+
+void set_shadow_segment(memory_segment *seg, memory_segment *parent,
+    size_t ratio, const char *name) {
+  seg->parent = parent;
+  seg->name = name;
+  seg->shadow_ratio = ratio;
+  seg->size = parent->size/seg->shadow_ratio;
+  seg->mspace = eacsl_create_mspace(seg->size + SHADOW_SEGMENT_PADDING, 0);
+  seg->start = (uintptr_t)eacsl_mspace_malloc(seg->mspace,1);
+  seg->end = seg->start + seg->size;
+  seg->shadow_offset = parent->start - seg->start;
+}
+
+void init_shadow_layout_pre_main() {
+  init_shadow_layout_heap();
+
+#if E_ACSL_OS_IS_LINUX
+  init_shadow_layout_global();
+  init_shadow_layout_tls();
+#elif E_ACSL_OS_IS_WINDOWS
+  HANDLE module = GetModuleHandle(NULL);
+  init_shadow_layout_text(module);
+  init_shadow_layout_bss(module);
+  init_shadow_layout_data(module);
+  init_shadow_layout_idata(module);
+  init_shadow_layout_rdata(module);
+#endif
+
+  mem_layout.is_initialized_pre_main = 1;
+}
+
+void init_shadow_layout_main(int *argc_ref, char *** argv_ref) {
+  init_shadow_layout_stack(argc_ref, argv_ref);
 
-  mem_layout.is_initialized = 1;
+  mem_layout.is_initialized_main = 1;
 }
 
 void clean_shadow_layout() {
-  if (mem_layout.is_initialized) {
+  if (mem_layout.is_initialized_pre_main && mem_layout.is_initialized_main) {
     int i;
     for (i = 0; i < sizeof(mem_partitions)/sizeof(memory_partition*); i++) {
       if (mem_partitions[i]->primary.mspace)
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
index b15415383d498ef48e84b392a5e6323cbbac5912..93dc849c54d3710c0b0a95581551d5b3e9a687ef 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
@@ -30,6 +30,7 @@
 
 #include <stddef.h>
 #include <stdint.h>
+#include "../../internals/e_acsl_config.h"
 #include "../../internals/e_acsl_malloc.h"
 
 /* Default size of a program's heap tracked via shadow memory */
@@ -42,21 +43,6 @@
 #define E_ACSL_STACK_SIZE 64
 #endif
 
-/* Symbols exported by the linker script */
-
-/*!\brief The first address past the end of the text segment. */
-extern char etext;
-/*!\brief The first address past the end of the initialized data segment. */
-extern char edata;
-/*!\brief The first address past the end of the uninitialized data segment. */
-extern char end;
-/*!\brief The first address of a program. */
-extern char __executable_start;
-
-/* \cond */
-void *sbrk(intptr_t increment);
-char *strerror(int errnum);
-
 /* MAP_ANONYMOUS is a mmap flag indicating that the contents of allocated blocks
  * should be nullified. Set value from <bits/mman-linux.h>, if MAP_ANONYMOUS is
  * undefined */
@@ -95,43 +81,7 @@ char *strerror(int errnum);
 #define SHADOW_SEGMENT_PADDING (512*KB)
 /* }}} */
 
-/** Thread-local storage information {{{ */
-
-/*! Thread-local storage (TLS) keeps track of copies of per-thread variables.
- * Even though at the present stage RTL of E-ACSL is not thread-safe, some
- * of the variables (for instance ::errno) are allocated there. In X86 TLS
- * is typically located somewhere below the program's stack but above mmap
- * areas. TLS is typically separated into two sections: .tdata and .tbss.
- * Similar to globals using .data and .bss, .tdata keeps track of initialized
- * thread-local variables, while .tbss holds uninitialized ones.
- *
- * Start and end addresses of TLS are obtained by taking addresses of
- * initialized and uninitialized variables in TLS (::id_tdata and ::id_tss)
- * and adding fixed amount of shadow space around them. Visually it looks
- * as follows:
- *
- *   end TLS address (&id_tdata + TLS_SHADOW_SIZE/2)
- *   id_tdata address
- *   ...
- *   id_tbss address
- *   start TLS address (&id_bss - TLS_SHADOW_SIZE/2)
- *
- * HOWEVER problems can occur if PGM_TLS_SIZE is too big:
- * see get_tls_start for details.
- */
-
-/*! \brief Return byte-size of the TLS segment */
-inline static size_t get_tls_size() {
-  return PGM_TLS_SIZE;
-}
-
-static __thread int id_tdata = 1;
-static __thread int id_tbss;
-
-/* }}} */
-
 /** Program stack information {{{ */
-extern char ** environ;
 
 /*! \brief Set a new soft stack limit
  *
@@ -149,35 +99,11 @@ size_t increase_stack_limit(const size_t size);
 /*! \brief Return byte-size of a program's stack. The return value is the soft
  * stack limit, i.e., it can be programmatically increased at runtime. */
 size_t get_stack_size();
-
-/*! \brief Return greatest (known) address on a program's stack.
- * This function presently determines the address using the address of the
- * last string in `environ`. That is, it assumes that argc and argv are
- * stored below environ, which holds for GCC/Glibc but is not necessarily
- * true for some other compilers/libraries. */
-uintptr_t get_stack_start(int *argc_ref,  char *** argv_ref);
 /* }}} */
 
 /** Program heap information {{{ */
-/*! \brief Return the start address of a program's heap. */
-uintptr_t get_heap_start();
-
 /*! \brief Return the tracked size of a program's heap. */
 size_t get_heap_size();
-
-/*! \brief Return the size of a secondary shadow region tracking
- * initialization (i.e., init shadow). */
-size_t get_heap_init_size();
-
-/** }}} */
-
-/** Program global information {{{ */
-/*! \brief Return the start address of a segment holding globals (generally
- * BSS and Data segments). */
-uintptr_t get_global_start();
-
-/*! \brief Return byte-size of global segment */
-size_t get_global_size();
 /** }}} */
 
 /** Shadow Layout {{{ */
@@ -257,20 +183,48 @@ typedef struct memory_partition memory_partition;
 struct memory_layout {
   memory_partition heap;
   memory_partition stack;
+#if E_ACSL_OS_IS_LINUX
+  // On linux
+  // The text, bss and data segments are contiguous and regrouped here in a
+  // global memory partition
   memory_partition global;
+  // The TLS is in a specific section and identifiable
   memory_partition tls;
-  int is_initialized;
+#elif E_ACSL_OS_IS_WINDOWS
+  // On windows
+  // The text, bss and data segments are not necessarily contiguous so each one
+  // is in its own memory partition
+  memory_partition text;
+  memory_partition bss;
+  memory_partition data;
+  memory_partition idata;
+  memory_partition rdata;
+  // The TLS is stored on the heap and is indistiguishable from it
+#endif
+  int is_initialized_pre_main;
+  int is_initialized_main;
 };
 
 /*! \brief Full program memory layout. */
-struct memory_layout mem_layout;
+struct memory_layout mem_layout = {
+  .is_initialized_pre_main = 0,
+  .is_initialized_main = 0,
+};
 
 /*! \brief Array of used partitions */
 memory_partition *mem_partitions [] = {
   &mem_layout.heap,
   &mem_layout.stack,
+#if E_ACSL_OS_IS_LINUX
   &mem_layout.global,
-  &mem_layout.tls
+  &mem_layout.tls,
+#elif E_ACSL_OS_IS_WINDOWS
+  &mem_layout.text,
+  &mem_layout.bss,
+  &mem_layout.data,
+  &mem_layout.idata,
+  &mem_layout.rdata,
+#endif
 };
 
 /*! \brief Initialize an application memory segment.
@@ -296,17 +250,18 @@ void set_shadow_segment(memory_segment *seg, memory_segment *parent,
 /*! \brief Initialize memory layout, i.e., determine bounds of program segments,
  * allocate shadow memory spaces and compute offsets. This function populates
  * global struct ::memory_layout holding that information with data.
-   Case of the stack. */
-void init_shadow_layout_stack(int *argc_ref, char ***argv_ref);
-
-/*! \brief Return start address of a program's TLS */
-uintptr_t get_tls_start();
+ *
+ * Case of segments available before main (for instance from a function marked
+ * as `__constructor__`). */
+void init_shadow_layout_pre_main();
 
 /*! \brief Initialize memory layout, i.e., determine bounds of program segments,
  * allocate shadow memory spaces and compute offsets. This function populates
  * global struct ::memory_layout holding that information with data.
-   Case of the heap, globals and tls. */
-void init_shadow_layout_heap_global_tls();
+ *
+ * Case of segments only available once inside of main (for instance the stack
+ * of the program). */
+void init_shadow_layout_main(int *argc_ref, char ***argv_ref);
 
 /*! \brief Deallocate shadow regions used by runtime analysis */
 void clean_shadow_layout();
@@ -333,10 +288,23 @@ void clean_shadow_layout();
 #define heap_secondary_offset   mem_layout.heap.secondary.shadow_offset
 #define stack_primary_offset    mem_layout.stack.primary.shadow_offset
 #define stack_secondary_offset  mem_layout.stack.secondary.shadow_offset
-#define global_primary_offset   mem_layout.global.primary.shadow_offset
-#define global_secondary_offset mem_layout.global.secondary.shadow_offset
-#define tls_primary_offset      mem_layout.tls.primary.shadow_offset
-#define tls_secondary_offset    mem_layout.tls.secondary.shadow_offset
+#if E_ACSL_OS_IS_LINUX
+# define global_primary_offset   mem_layout.global.primary.shadow_offset
+# define global_secondary_offset mem_layout.global.secondary.shadow_offset
+# define tls_primary_offset      mem_layout.tls.primary.shadow_offset
+# define tls_secondary_offset    mem_layout.tls.secondary.shadow_offset
+#elif E_ACSL_OS_IS_WINDOWS
+# define text_primary_offset mem_layout.text.primary.shadow_offset
+# define text_secondary_offset mem_layout.text.secondary.shadow_offset
+# define bss_primary_offset mem_layout.bss.primary.shadow_offset
+# define bss_secondary_offset mem_layout.bss.secondary.shadow_offset
+# define data_primary_offset mem_layout.data.primary.shadow_offset
+# define data_secondary_offset mem_layout.data.secondary.shadow_offset
+# define idata_primary_offset mem_layout.idata.primary.shadow_offset
+# define idata_secondary_offset mem_layout.idata.secondary.shadow_offset
+# define rdata_primary_offset mem_layout.rdata.primary.shadow_offset
+# define rdata_secondary_offset mem_layout.rdata.secondary.shadow_offset
+#endif
 
 /*! \brief Compute a shadow address using displacement offset
  * @param _addr - an application space address
@@ -374,29 +342,97 @@ void clean_shadow_layout();
 #define SECONDARY_STACK_SHADOW(_addr) \
   SHADOW_ACCESS(_addr, stack_secondary_offset)
 
+#if E_ACSL_OS_IS_LINUX
 /*! \brief Convert a global address into its primary shadow counterpart */
-#define PRIMARY_GLOBAL_SHADOW(_addr)  \
+# define PRIMARY_GLOBAL_SHADOW(_addr)  \
   SHADOW_ACCESS(_addr, global_primary_offset)
 
 /*! \brief Convert a global address into its secondary shadow counterpart */
-#define SECONDARY_GLOBAL_SHADOW(_addr) \
+# define SECONDARY_GLOBAL_SHADOW(_addr) \
   SHADOW_ACCESS(_addr, global_secondary_offset)
 
 /*! \brief Convert a TLS address into its primary shadow counterpart */
-#define PRIMARY_TLS_SHADOW(_addr)  \
+# define PRIMARY_TLS_SHADOW(_addr)  \
   SHADOW_ACCESS(_addr, tls_primary_offset)
 
 /*! \brief Convert a TLS address into its secondary shadow counterpart */
-#define SECONDARY_TLS_SHADOW(_addr) \
+# define SECONDARY_TLS_SHADOW(_addr) \
   SHADOW_ACCESS(_addr, tls_secondary_offset)
+#elif E_ACSL_OS_IS_WINDOWS
+/*! \brief Convert a text address into its primary shadow counterpart */
+# define PRIMARY_TEXT_SHADOW(_addr)  \
+  SHADOW_ACCESS(_addr, text_primary_offset)
+
+/*! \brief Convert a text address into its secondary shadow counterpart */
+# define SECONDARY_TEXT_SHADOW(_addr) \
+  SHADOW_ACCESS(_addr, text_secondary_offset)
+
+/*! \brief Convert a bss address into its primary shadow counterpart */
+# define PRIMARY_BSS_SHADOW(_addr)  \
+  SHADOW_ACCESS(_addr, bss_primary_offset)
+
+/*! \brief Convert a bss address into its secondary shadow counterpart */
+# define SECONDARY_BSS_SHADOW(_addr) \
+  SHADOW_ACCESS(_addr, bss_secondary_offset)
+
+/*! \brief Convert an data address into its primary shadow counterpart */
+# define PRIMARY_DATA_SHADOW(_addr)  \
+  SHADOW_ACCESS(_addr, data_primary_offset)
+
+/*! \brief Convert an data address into its secondary shadow counterpart */
+# define SECONDARY_DATA_SHADOW(_addr) \
+  SHADOW_ACCESS(_addr, data_secondary_offset)
+
+/*! \brief Convert an idata address into its primary shadow counterpart */
+# define PRIMARY_IDATA_SHADOW(_addr)  \
+  SHADOW_ACCESS(_addr, idata_primary_offset)
+
+/*! \brief Convert an idata address into its secondary shadow counterpart */
+# define SECONDARY_IDATA_SHADOW(_addr) \
+  SHADOW_ACCESS(_addr, idata_secondary_offset)
+
+/*! \brief Convert an rdata address into its primary shadow counterpart */
+# define PRIMARY_RDATA_SHADOW(_addr)  \
+  SHADOW_ACCESS(_addr, rdata_primary_offset)
+
+/*! \brief Convert an rdata address into its secondary shadow counterpart */
+# define SECONDARY_RDATA_SHADOW(_addr) \
+  SHADOW_ACCESS(_addr, rdata_secondary_offset)
+
+/*! \brief Convert a global address into its primary shadow counterpart */
+# define PRIMARY_GLOBAL_SHADOW(_addr) \
+    (IS_ON_TEXT(_addr) ? PRIMARY_TEXT_SHADOW(_addr) : \
+     IS_ON_BSS(_addr) ? PRIMARY_BSS_SHADOW(_addr) : \
+     IS_ON_DATA(_addr) ? PRIMARY_DATA_SHADOW(_addr) : \
+     IS_ON_IDATA(_addr) ? PRIMARY_IDATA_SHADOW(_addr) : \
+     IS_ON_RDATA(_addr) ? PRIMARY_RDATA_SHADOW(_addr) : (intptr_t)0)
+
+/*! \brief Convert a global address into its secondary shadow counterpart */
+# define SECONDARY_GLOBAL_SHADOW(_addr) \
+    (IS_ON_TEXT(_addr) ? SECONDARY_TEXT_SHADOW(_addr) : \
+     IS_ON_BSS(_addr) ? SECONDARY_BSS_SHADOW(_addr) : \
+     IS_ON_DATA(_addr) ? SECONDARY_DATA_SHADOW(_addr) : \
+     IS_ON_IDATA(_addr) ? SECONDARY_IDATA_SHADOW(_addr) : \
+     IS_ON_RDATA(_addr) ? SECONDARY_RDATA_SHADOW(_addr) : (intptr_t)0)
+#endif
 
 /* \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.
  * For an untracked address `0` is returned. */
-#define SHADOW_REGION_ADDRESS(_addr, _region) \
-  (IS_ON_STACK(_addr) ? _region##_STACK_SHADOW(_addr) : \
-    IS_ON_GLOBAL(_addr) ? _region##_GLOBAL_SHADOW(_addr) : \
-      IS_ON_TLS(_addr) ? _region##_TLS_SHADOW(_addr) : 0)
+#if E_ACSL_OS_IS_LINUX
+# define SHADOW_REGION_ADDRESS(_addr, _region) \
+    (IS_ON_STACK(_addr) ? _region##_STACK_SHADOW(_addr) : \
+     IS_ON_GLOBAL(_addr) ? _region##_GLOBAL_SHADOW(_addr) : \
+     IS_ON_TLS(_addr) ? _region##_TLS_SHADOW(_addr) : (intptr_t)0)
+#elif E_ACSL_OS_IS_WINDOWS
+# define SHADOW_REGION_ADDRESS(_addr, _region) \
+    (IS_ON_STACK(_addr) ? _region##_STACK_SHADOW(_addr) : \
+     IS_ON_TEXT(_addr) ? _region##_TEXT_SHADOW(_addr) : \
+     IS_ON_BSS(_addr) ? _region##_BSS_SHADOW(_addr) : \
+     IS_ON_DATA(_addr) ? _region##_DATA_SHADOW(_addr) : \
+     IS_ON_IDATA(_addr) ? _region##_IDATA_SHADOW(_addr) : \
+     IS_ON_RDATA(_addr) ? _region##_RDATA_SHADOW(_addr) : (intptr_t)0)
+#endif
 
 /*! \brief Primary shadow address of a non-dynamic region */
 #define PRIMARY_SHADOW(_addr) SHADOW_REGION_ADDRESS(_addr, PRIMARY)
@@ -422,22 +458,50 @@ void clean_shadow_layout();
 /*! \brief Evaluate to true if `_addr` is a stack address */
 #define IS_ON_STACK(_addr) IS_ON(_addr, mem_layout.stack.application)
 
+#if E_ACSL_OS_IS_LINUX
 /*! \brief Evaluate to true if `_addr` is a global address */
-#define IS_ON_GLOBAL(_addr) IS_ON(_addr, mem_layout.global.application)
+# define IS_ON_GLOBAL(_addr) IS_ON(_addr, mem_layout.global.application)
 
 /*! \brief Evaluate to true if _addr is a TLS address */
-#define IS_ON_TLS(_addr) IS_ON(_addr, mem_layout.tls.application)
+# define IS_ON_TLS(_addr) IS_ON(_addr, mem_layout.tls.application)
 
 /*! \brief Shortcut for evaluating an address via ::IS_ON_STACK,
  * ::IS_ON_GLOBAL or ::IS_ON_TLS  */
-#define IS_ON_STATIC(_addr) \
-  (IS_ON_STACK(_addr) || IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr))
+# define IS_ON_STATIC(_addr) \
+    (IS_ON_STACK(_addr) || IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr))
+#elif E_ACSL_OS_IS_WINDOWS
+/*! \brief Evaluate to true if `_addr` is a text address */
+# define IS_ON_TEXT(_addr) IS_ON(_addr, mem_layout.text.application)
+
+/*! \brief Evaluate to true if `_addr` is a bss address */
+# define IS_ON_BSS(_addr) IS_ON(_addr, mem_layout.bss.application)
+
+/*! \brief Evaluate to true if `_addr` is an idata address */
+# define IS_ON_DATA(_addr) IS_ON(_addr, mem_layout.data.application)
+
+/*! \brief Evaluate to true if `_addr` is an idata address */
+# define IS_ON_IDATA(_addr) IS_ON(_addr, mem_layout.idata.application)
+
+/*! \brief Evaluate to true if `_addr` is an rdata address */
+# define IS_ON_RDATA(_addr) IS_ON(_addr, mem_layout.rdata.application)
+
+/*! \brief Evaluate to true if `_addr` is a global address */
+# define IS_ON_GLOBAL(_addr) \
+    (IS_ON_TEXT(_addr) || IS_ON_BSS(_addr) || IS_ON_DATA(_addr) || \
+     IS_ON_IDATA(_addr) || IS_ON_RDATA(_addr))
+
+/*! \brief Shortcut for evaluating an address via ::IS_ON_STACK,
+ * ::IS_ON_TEXT, :: IS_ON_BSS, ::IS_ON_IDATA, or ::IS_ON_RDATA  */
+# define IS_ON_STATIC(_addr) \
+    (IS_ON_STACK(_addr) || IS_ON_TEXT(_addr) || IS_ON_BSS(_addr) || \
+     IS_ON_DATA(_addr) || IS_ON_IDATA(_addr) || IS_ON_RDATA(_addr))
+#endif
 
 /*! \brief Evaluate to a true value if a given address belongs to tracked
- * allocation (i.e., found within tls, stack, heap or globally) */
+ * allocation (i.e., found within static or dynamic allocation) */
 #define IS_ON_VALID(_addr) \
-  (IS_ON_STACK(_addr) || IS_ON_HEAP(_addr) || \
-   IS_ON_GLOBAL(_addr) || IS_ON_TLS(_addr))
+  (IS_ON_STATIC(_addr) || IS_ON_HEAP(_addr))
+
 /* }}} */
 
 #ifdef E_ACSL_TEMPORAL /* {{{ */
@@ -453,21 +517,79 @@ void clean_shadow_layout();
 #define TEMPORAL_SECONDARY_STACK_SHADOW(_addr) \
   SHADOW_ACCESS(_addr, mem_layout.stack.temporal_secondary.shadow_offset)
 
+#if E_ACSL_OS_IS_LINUX
 /*! \brief Convert a global address into its primary temporal shadow counterpart */
-#define TEMPORAL_PRIMARY_GLOBAL_SHADOW(_addr)  \
-  SHADOW_ACCESS(_addr, mem_layout.global.temporal_primary.shadow_offset)
+# define TEMPORAL_PRIMARY_GLOBAL_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.global.temporal_primary.shadow_offset)
 
 /*! \brief Convert a global address into its primary temporal shadow counterpart */
-#define TEMPORAL_SECONDARY_GLOBAL_SHADOW(_addr)  \
-  SHADOW_ACCESS(_addr, mem_layout.global.temporal_secondary.shadow_offset)
+# define TEMPORAL_SECONDARY_GLOBAL_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.global.temporal_secondary.shadow_offset)
 
 /*! \brief Convert a TLS address into its primary temporal shadow counterpart */
-#define TEMPORAL_PRIMARY_TLS_SHADOW(_addr)  \
-  SHADOW_ACCESS(_addr, mem_layout.tls.temporal_primary.shadow_offset)
+# define TEMPORAL_PRIMARY_TLS_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.tls.temporal_primary.shadow_offset)
 
 /*! \brief Convert a TLS address into its secondary temporal shadow counterpart */
-#define TEMPORAL_SECONDARY_TLS_SHADOW(_addr)  \
-  SHADOW_ACCESS(_addr, mem_layout.tls.temporal_secondary.shadow_offset)
+# define TEMPORAL_SECONDARY_TLS_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.tls.temporal_secondary.shadow_offset)
+#elif E_ACSL_OS_IS_WINDOWS
+/*! \brief Convert a text address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_TEXT_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.text.temporal_primary.shadow_offset)
+
+/*! \brief Convert a text address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_TEXT_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.text.temporal_secondary.shadow_offset)
+
+/*! \brief Convert a bss address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_BSS_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.bss.temporal_primary.shadow_offset)
+
+/*! \brief Convert a bss address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_BSS_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.bss.temporal_secondary.shadow_offset)
+
+/*! \brief Convert an data address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_DATA_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.data.temporal_primary.shadow_offset)
+
+/*! \brief Convert an data address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_DATA_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.data.temporal_secondary.shadow_offset)
+
+/*! \brief Convert an idata address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_IDATA_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.idata.temporal_primary.shadow_offset)
+
+/*! \brief Convert an idata address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_IDATA_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.idata.temporal_secondary.shadow_offset)
+
+/*! \brief Convert an rdata address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_RDATA_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.rdata.temporal_primary.shadow_offset)
+
+/*! \brief Convert an rdata address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_RDATA_SHADOW(_addr)  \
+    SHADOW_ACCESS(_addr, mem_layout.rdata.temporal_secondary.shadow_offset)
+
+/*! \brief Convert a global address into its primary temporal shadow counterpart */
+# define TEMPORAL_PRIMARY_GLOBAL_SHADOW(_addr) \
+    (IS_ON_TEXT(_addr) ? TEMPORAL_PRIMARY_TEXT_SHADOW(_addr) : \
+     IS_ON_BSS(_addr) ? TEMPORAL_PRIMARY_BSS_SHADOW(_addr) : \
+     IS_ON_DATA(_addr) ? TEMPORAL_PRIMARY_DATA_SHADOW(_addr) : \
+     IS_ON_IDATA(_addr) ? TEMPORAL_PRIMARY_IDATA_SHADOW(_addr) : \
+     IS_ON_RDATA(_addr) ? TEMPORAL_PRIMARY_RDATA_SHADOW(_addr) : (intptr_t)0)
+
+/*! \brief Convert a global address into its primary temporal shadow counterpart */
+# define TEMPORAL_SECONDARY_GLOBAL_SHADOW(_addr) \
+    (IS_ON_TEXT(_addr) ? TEMPORAL_SECONDARY_TEXT_SHADOW(_addr) : \
+     IS_ON_BSS(_addr) ? TEMPORAL_SECONDARY_BSS_SHADOW(_addr) : \
+     IS_ON_DATA(_addr) ? TEMPORAL_SECONDARY_DATA_SHADOW(_addr) : \
+     IS_ON_IDATA(_addr) ? TEMPORAL_SECONDARY_IDATA_SHADOW(_addr) : \
+     IS_ON_RDATA(_addr) ? TEMPORAL_SECONDARY_RDATA_SHADOW(_addr) : (intptr_t)0)
+#endif
 
 /*! \brief Temporal primary shadow address of a non-dynamic region */
 #define TEMPORAL_PRIMARY_STATIC_SHADOW(_addr) \