diff --git a/src/plugins/e-acsl/.Makefile.lint b/src/plugins/e-acsl/.Makefile.lint
new file mode 100644
index 0000000000000000000000000000000000000000..758d9b5af383b304d78c5a666065d92b32d495be
--- /dev/null
+++ b/src/plugins/e-acsl/.Makefile.lint
@@ -0,0 +1,43 @@
+ML_LINT_KO+=src/plugins/e-acsl/E_ACSL.mli
+ML_LINT_KO+=src/plugins/e-acsl/at_with_lscope.ml
+ML_LINT_KO+=src/plugins/e-acsl/at_with_lscope.mli
+ML_LINT_KO+=src/plugins/e-acsl/builtins.ml
+ML_LINT_KO+=src/plugins/e-acsl/demo/script.ml
+ML_LINT_KO+=src/plugins/e-acsl/dup_functions.ml
+ML_LINT_KO+=src/plugins/e-acsl/env.ml
+ML_LINT_KO+=src/plugins/e-acsl/env.mli
+ML_LINT_KO+=src/plugins/e-acsl/error.ml
+ML_LINT_KO+=src/plugins/e-acsl/error.mli
+ML_LINT_KO+=src/plugins/e-acsl/exit_points.ml
+ML_LINT_KO+=src/plugins/e-acsl/exit_points.mli
+ML_LINT_KO+=src/plugins/e-acsl/functions.ml
+ML_LINT_KO+=src/plugins/e-acsl/functions.mli
+ML_LINT_KO+=src/plugins/e-acsl/gmpz.ml
+ML_LINT_KO+=src/plugins/e-acsl/gmpz.mli
+ML_LINT_KO+=src/plugins/e-acsl/interval.ml
+ML_LINT_KO+=src/plugins/e-acsl/keep_status.ml
+ML_LINT_KO+=src/plugins/e-acsl/label.ml
+ML_LINT_KO+=src/plugins/e-acsl/literal_strings.ml
+ML_LINT_KO+=src/plugins/e-acsl/loops.ml
+ML_LINT_KO+=src/plugins/e-acsl/loops.mli
+ML_LINT_KO+=src/plugins/e-acsl/lscope.ml
+ML_LINT_KO+=src/plugins/e-acsl/lscope.mli
+ML_LINT_KO+=src/plugins/e-acsl/main.ml
+ML_LINT_KO+=src/plugins/e-acsl/misc.ml
+ML_LINT_KO+=src/plugins/e-acsl/misc.mli
+ML_LINT_KO+=src/plugins/e-acsl/mmodel_analysis.ml
+ML_LINT_KO+=src/plugins/e-acsl/mmodel_translate.ml
+ML_LINT_KO+=src/plugins/e-acsl/mmodel_translate.mli
+ML_LINT_KO+=src/plugins/e-acsl/options.ml
+ML_LINT_KO+=src/plugins/e-acsl/prepare_ast.ml
+ML_LINT_KO+=src/plugins/e-acsl/quantif.ml
+ML_LINT_KO+=src/plugins/e-acsl/quantif.mli
+ML_LINT_KO+=src/plugins/e-acsl/rte.ml
+ML_LINT_KO+=src/plugins/e-acsl/temporal.ml
+ML_LINT_KO+=src/plugins/e-acsl/temporal.mli
+ML_LINT_KO+=src/plugins/e-acsl/top/E_ACSL.mli
+ML_LINT_KO+=src/plugins/e-acsl/translate.ml
+ML_LINT_KO+=src/plugins/e-acsl/translate.mli
+ML_LINT_KO+=src/plugins/e-acsl/typing.ml
+ML_LINT_KO+=src/plugins/e-acsl/typing.mli
+ML_LINT_KO+=src/plugins/e-acsl/visit.ml
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 9bfbc386ed762119c9b9c166bbc0c165d9ddcb62..96261e258805fa212c30b1e1166fa82af3386666 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -63,6 +63,7 @@
/tests/no-main/result/*
/tests/full-mmodel/result/*
/tests/full-mmodel-only/result/*
+/tests/segment-only/result/*
/tests/bts/result/*
/tests/gmp/result/*
/tests/reject/result/*
diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 0f31a88fe9c117485030123185d39c06d6e65787..3a48ff126f4f03ea3b2eb133fb1b2de6bb40e772 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-18.0-beta
\ No newline at end of file
+18.0+dev
\ No newline at end of file
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 36f1ff2a80e090c0eb193a7a38d7064fafca7846..83371e18524155eecca382e4ac918533e58bdcaf 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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.
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl.h b/src/plugins/e-acsl/share/e-acsl/e_acsl.h
index 1045095a0b66c632681a5b6493fe74dbadb0ceb4..e25be516e6ce131f083a5a5e3766b7760e91fa69 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl.h
@@ -84,6 +84,7 @@
/* Memory state initialization */
#define memory_clean export_alias(memory_clean)
+#define mspaces_init export_alias(mspaces_init)
#define memory_init export_alias(memory_init)
/* Heap size */
@@ -175,6 +176,10 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
/*** Memory tracking {{{ ***/
/************************************************************************/
+/*! \brief Initialize memory locations. */
+void mspaces_init()
+ __attribute__((FC_BUILTIN));
+
/*! \brief Initialize memory tracking state.
* Called before any other statement in \p main */
/*@ assigns \nothing; */
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 580274d9b85e203cb38f453c9e5070b3e65ce820..eae9f787e3a438ba80f47393ceee9e70745a14f9 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
@@ -193,19 +193,30 @@ static void argv_alloca(int *argc_ref, char *** argv_ref) {
/* Program initialization {{{ */
extern int main(void);
-void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
+int MSPACES_INIT = 0;
+
+void mspaces_init() {
+ if(MSPACES_INIT) return;
describe_run();
+ 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();
+ MSPACES_INIT = 1;
+}
+
+void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
+ mspaces_init(argc_ref, argv_ref);
/** Verify that the given size of a pointer matches the one in the present
* architecture. This is a guard against Frama-C instrumentations using
* architectures different to the given one. */
- make_memory_spaces(64*MB, get_heap_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 */
- init_shadow_layout(argc_ref, argv_ref);
+ /* 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;
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 100e167734f7aa1fc08a372c2eadfa09f53deabb..e3cf2c42b9e65d02d00e571d695d8cdaf891543e 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
@@ -880,6 +880,7 @@ static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
}
}
+extern int MSPACES_INIT;
/*! \brief Replacement for a malloc function that additionally tracks the
* allocated memory block.
*
@@ -893,6 +894,10 @@ static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
* behaviour is as if the size were some non-zero value, except that the
* returned pointer shall not be used to access an object." */
void* malloc(size_t size) {
+ if(! MSPACES_INIT) {
+ mspaces_init();
+ MSPACES_INIT = 1;
+ }
size_t alloc_size = ALLOC_SIZE(size);
/* Return NULL if the size is too large to be aligned */
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 0822602dd21d5f9d00fc85b207601619f8be2276..f7a779e89259d08a893b83ca94b3b91fb14c2af1 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
@@ -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);
diff --git a/src/plugins/e-acsl/tests/segment-only/constructor.c b/src/plugins/e-acsl/tests/segment-only/constructor.c
new file mode 100644
index 0000000000000000000000000000000000000000..6600992870e3d1809cb467a56479b9060ad9bfdc
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/constructor.c
@@ -0,0 +1,18 @@
+/* run.config
+ COMMENT: bts #2405. Memory not initialized for code executed before main.
+*/
+
+#include <stdio.h>
+#include <stdlib.h>
+
+__attribute__((constructor))
+void f() {
+ printf("f\n");
+ char *buf = (char*)malloc(10*sizeof(char));
+ free(buf);
+}
+
+int main() {
+ printf("main\n");
+ return 0;
+}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle b/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fb1184a3e5634daf84200d210428dfcd8c91aa44
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
@@ -0,0 +1,20 @@
+[e-acsl] beginning translation.
+[e-acsl] Warning: annotating undefined function `printf_va_1':
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
+[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:16: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[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:10: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[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".
diff --git a/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c b/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
new file mode 100644
index 0000000000000000000000000000000000000000..eefdbbe0fd9c57b351169fd473ed0a95dc5ef0c9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
@@ -0,0 +1,40 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+char *__gen_e_acsl_literal_string_2;
+char *__gen_e_acsl_literal_string;
+void f(void) __attribute__((__constructor__));
+void f(void)
+{
+ __gen_e_acsl_printf_va_1(__gen_e_acsl_literal_string);
+ char *buf = malloc((unsigned long)10 * sizeof(char));
+ free((void *)buf);
+ return;
+}
+
+void __e_acsl_globals_init(void)
+{
+ __gen_e_acsl_literal_string_2 = "main\n";
+ __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+ sizeof("main\n"));
+ __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
+ __gen_e_acsl_literal_string = "f\n";
+ __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);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __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);
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/segment-only/test_config b/src/plugins/e-acsl/tests/segment-only/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..3aa2fcbc6b1e0f167afe722d6f48c707129bab6d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/test_config
@@ -0,0 +1,3 @@
+LOG: gen_@PTEST_NAME@.c
+OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/segment-only/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva -eva-verbose 0
+EXEC: ./scripts/testrun.sh @PTEST_NAME@ segment-only "" "--frama-c=@frama-c@" "segment"
\ No newline at end of file