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/share/e-acsl/e_acsl.h b/src/plugins/e-acsl/share/e-acsl/e_acsl.h
index 1045095a0b66c632681a5b6493fe74dbadb0ceb4..d217505a2d6347f669324cd8b7be6610797e49b0 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(int *argc_ref, char *** argv_ref)
+ __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/e_acsl_safe_locations.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h
index d98a944cc10831639161c033795ba7d590c7c4ac..78a52b136857fb1afd9d1866d6fcd6813ea250fe 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_safe_locations.h
@@ -69,9 +69,11 @@ extern FILE *stderr; /* Standard error output stream. */
static 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");
+ /* 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");
}
#endif
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..033325efd97df9da1b85c5fbff2d0166194c1c3d 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,15 +193,12 @@ 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(int *argc_ref, char *** argv_ref) {
+ if(MSPACES_INIT) return;
describe_run();
- /** 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 */
@@ -209,6 +206,17 @@ void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
//DEBUG_PRINT_LAYOUT;
/* Make sure the layout holds */
DVALIDATE_SHADOW_LAYOUT;
+ 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. */
+ arch_assert(ptr_size);
+ /* Initialize report file with debug logs (only in debug mode). */
+ initialize_report_file(argc_ref, argv_ref);
/* Track program arguments. */
if (argc_ref && argv_ref)
argv_alloca(argc_ref, argv_ref);
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..9a093e62ae0556c797aa03398dccd3e2543fdc4c 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(0, 0); // arguments of main are not (?) known at this point
+ 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/tests/segment-only/constructor.c b/src/plugins/e-acsl/tests/segment-only/constructor.c
new file mode 100644
index 0000000000000000000000000000000000000000..68df399f553dfd75e3e2f0acda50da760736d521
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/constructor.c
@@ -0,0 +1,25 @@
+/* run.config
+ COMMENT: bts #2405. Memory not initialized for code executed before main.
+*/
+
+#include <errno.h>
+#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");
+ 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
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..71defa5cfea659c3744b0fc09e09d79b034dc179
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/oracle/constructor.res.oracle
@@ -0,0 +1,22 @@
+[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:17: Warning:
+ E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/segment-only/constructor.c:17: 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 construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] tests/segment-only/constructor.c:11: 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).
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..995599d7c5cabb8707610432cf65b1891d232f25
--- /dev/null
+++ b/src/plugins/e-acsl/tests/segment-only/oracle/gen_constructor.c
@@ -0,0 +1,97 @@
+/* Generated by Frama-C */
+#include "errno.h"
+#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);
+ __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;
+}
+
+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);
+ 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;
+}
+
+
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