Julien's review no.1:

 - Safe locations are ok but need to increase TLS to 32 Mo for the libxml usecase
 - Fix order of operations during memory initialization
 - TODO: memory allocated before main are not seen as being valid

src/plugins/e-acsl/doc/Changelog

@@ -23,8 +23,10 @@
 Plugin E-ACSL 18.0 (Argon)
 ##########################
 
+-* runtime      [2018/11/13] Fix bug #!2405 about memory initialization
+                in presence of GCC constructors.
 -* E-ACSL       [2018/10/23] Fix bug #2406 about monitoring of variables
-	        with incomplete types.
+                with incomplete types.
 -* E-ACSL       [2018/10/04] Fix bug #2386 about incorrect typing when
                 performing pointer subtraction.
 -* E-ACSL       [2018/10/04] Support for \at on purely logic variables.

src/plugins/e-acsl/share/e-acsl/e_acsl.h

@@ -177,7 +177,7 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
 /************************************************************************/
 
 /*! \brief Initialize memory locations. */
-void mspaces_init(int *argc_ref, char *** argv_ref)
+void mspaces_init()
   __attribute__((FC_BUILTIN));
 
 /*! \brief Initialize memory tracking state.

src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h

@@ -69,11 +69,9 @@ extern FILE *stderr;		/* Standard error output stream. */
 
 static void collect_safe_locations() {
   /* Tracking of errno and standard streams */
-  /* TODO: how to corrrectly add the following locations
-     in presence of contructors? */
-  // 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), "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");
 }
 #endif

src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c

@@ -195,17 +195,13 @@ extern int main(void);
 
 int MSPACES_INIT = 0;
 
-void mspaces_init(int *argc_ref, char *** argv_ref) {
+void mspaces_init() {
   if(MSPACES_INIT) return;
   describe_run();
   make_memory_spaces(64*MB, get_heap_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_shadow_layout(argc_ref, argv_ref);
-  //DEBUG_PRINT_LAYOUT;
-  /* Make sure the layout holds */
-  DVALIDATE_SHADOW_LAYOUT;
+  /* Allocate and log shadow memory layout of the execution.
+    Case of the heap, globals and tls. */
+  init_shadow_layout_heap_global_tls();
   MSPACES_INIT = 1;
 }
 
@@ -217,6 +213,13 @@ void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
   arch_assert(ptr_size);
   /* Initialize report file with debug logs (only in debug mode). */
   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);
+  //DEBUG_PRINT_LAYOUT;
+  /* Make sure the layout holds */
+  DVALIDATE_SHADOW_LAYOUT;
   /* Track program arguments. */
   if (argc_ref && argv_ref)
     argv_alloca(argc_ref, argv_ref);

src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h

@@ -895,7 +895,7 @@ extern int MSPACES_INIT;
  *    returned pointer shall not be used to access an object." */
 void* malloc(size_t size) {
   if(! MSPACES_INIT) {
-    mspaces_init(0, 0); // arguments of main are not (?) known at this point
+    mspaces_init();
     MSPACES_INIT = 1;
   }
   size_t alloc_size = ALLOC_SIZE(size);

src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_shadow_layout.h

@@ -72,8 +72,12 @@ char *strerror(int errnum);
 /*! \brief Size of a program's heap */
 #define PGM_HEAP_SIZE (E_ACSL_HEAP_SIZE * MB)
 
-/*! \brief Size of a program's Thread-local storage (TLS) */
-#define PGM_TLS_SIZE (16 * MB)
+/*! \brief Size of a program's Thread-local storage (TLS).
+  Standard streams stdin, stdout and stderr are put here.
+  Some libraries such as libxml use it quite a lot:
+  it may occur that the given size is not enough,
+  in which case it MUST be increased. */
+#define PGM_TLS_SIZE (32 * MB)
 
 /*! \brief Mspace padding used by shadow segments. This is to make sure that
  * some allocation which exceeds the size of an initial memspace does not
@@ -350,18 +354,9 @@ static 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. */
-static void init_shadow_layout(int *argc_ref, char ***argv_ref) {
-  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
-
+ * global struct ::memory_layout holding that information with data.
+   Case of the stack. */
+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);
@@ -372,6 +367,24 @@ static void init_shadow_layout(int *argc_ref, char ***argv_ref) {
   set_shadow_segment(&pstack->temporal_secondary, &pstack->application, 1, "temporal_stack_secondary");
 #endif
 
+  mem_layout.is_initialized = 1;
+}
+
+/*! \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. */
+static 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_partition *pglobal = &mem_layout.global;
   set_application_segment(&pglobal->application, get_global_start(),
     get_global_size(), "global", NULL);

src/plugins/e-acsl/tests/segment-only/constructor.c

@@ -2,7 +2,6 @@
    COMMENT: bts #2405. Memory not initialized for code executed before main.
 */
 
-#include <errno.h>
 #include <stdio.h>
 #include <stdlib.h>
 
@@ -15,11 +14,5 @@ void f() {
 
 int main() {
   printf("main\n");
-  int *p = &errno;
-  // TODO: see e_acsl_safe_locations.h regarding the standard streams
-  /*@ assert ! \valid(p);      */ ;
-  /*@ assert ! \valid(stderr); */ ;
-  /*@ assert ! \valid(stdin);  */ ;
-  /*@ assert ! \valid(stdout); */ ;
   return 0;
 }
\ No newline at end of file

src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle

@@ -5,18 +5,16 @@
 [e-acsl] Warning: annotating undefined function `printf_va_2':
   the generated program may miss memory instrumentation
   if there are memory-related annotations.
-[e-acsl] tests/segment-only/constructor.c:17: Warning: 
+[e-acsl] tests/segment-only/constructor.c:16: Warning: 
   E-ACSL construct `logic function application' is not yet supported.
   Ignoring annotation.
-[e-acsl] tests/segment-only/constructor.c:17: Warning: 
+[e-acsl] tests/segment-only/constructor.c:16: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] tests/segment-only/constructor.c:11: Warning: 
+[e-acsl] tests/segment-only/constructor.c:10: Warning: 
   E-ACSL construct `logic function application' is not yet supported.
   Ignoring annotation.
-[e-acsl] tests/segment-only/constructor.c:11: Warning: 
+[e-acsl] tests/segment-only/constructor.c:10: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/segment-only/constructor.c:19: Warning: 
-  assertion got status invalid (stopping propagation).

src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c

 /* Generated by Frama-C */
-#include "errno.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string_2;
@@ -24,14 +23,6 @@ void __e_acsl_globals_init(void)
   __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("f\n"));
   __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
   __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
-  __e_acsl_store_block((void *)(& stdout),(size_t)8);
-  __e_acsl_full_init((void *)(& stdout));
-  __e_acsl_store_block((void *)(& stdin),(size_t)8);
-  __e_acsl_full_init((void *)(& stdin));
-  __e_acsl_store_block((void *)(& stderr),(size_t)8);
-  __e_acsl_full_init((void *)(& stderr));
-  __e_acsl_store_block((void *)(& errno),(size_t)4);
-  __e_acsl_full_init((void *)(& errno));
   return;
 }
 
@@ -41,55 +32,7 @@ int main(void)
   __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __e_acsl_globals_init();
   __gen_e_acsl_printf_va_2(__gen_e_acsl_literal_string_2);
-  int *p = & errno;
-  __e_acsl_store_block((void *)(& p),(size_t)8);
-  __e_acsl_full_init((void *)(& p));
-  /*@ assert ¬\valid(p); */
-  {
-    int __gen_e_acsl_initialized;
-    int __gen_e_acsl_and;
-    __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& p),
-                                                    sizeof(int *));
-    if (__gen_e_acsl_initialized) {
-      int __gen_e_acsl_valid;
-      __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
-                                          (void *)(& p));
-      __gen_e_acsl_and = __gen_e_acsl_valid;
-    }
-    else __gen_e_acsl_and = 0;
-    __e_acsl_assert(! __gen_e_acsl_and,(char *)"Assertion",(char *)"main",
-                    (char *)"!\\valid(p)",19);
-  }
-  /*@ assert ¬\valid(__fc_stderr); */
-  {
-    int __gen_e_acsl_valid_2;
-    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stderr,sizeof(FILE),
-                                          (void *)stderr,(void *)(& stderr));
-    __e_acsl_assert(! __gen_e_acsl_valid_2,(char *)"Assertion",
-                    (char *)"main",(char *)"!\\valid(__fc_stderr)",20);
-  }
-  /*@ assert ¬\valid(__fc_stdin); */
-  {
-    int __gen_e_acsl_valid_3;
-    __gen_e_acsl_valid_3 = __e_acsl_valid((void *)stdin,sizeof(FILE),
-                                          (void *)stdin,(void *)(& stdin));
-    __e_acsl_assert(! __gen_e_acsl_valid_3,(char *)"Assertion",
-                    (char *)"main",(char *)"!\\valid(__fc_stdin)",21);
-  }
-  /*@ assert ¬\valid(__fc_stdout); */
-  {
-    int __gen_e_acsl_valid_4;
-    __gen_e_acsl_valid_4 = __e_acsl_valid((void *)stdout,sizeof(FILE),
-                                          (void *)stdout,(void *)(& stdout));
-    __e_acsl_assert(! __gen_e_acsl_valid_4,(char *)"Assertion",
-                    (char *)"main",(char *)"!\\valid(__fc_stdout)",22);
-  }
   __retres = 0;
-  __e_acsl_delete_block((void *)(& stdout));
-  __e_acsl_delete_block((void *)(& stdin));
-  __e_acsl_delete_block((void *)(& stderr));
-  __e_acsl_delete_block((void *)(& errno));
-  __e_acsl_delete_block((void *)(& p));
   __e_acsl_memory_clean();
   return __retres;
 }