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 127f85e94c70331573fca8b6819d09cd183b3292..97554ed727124db28f53e843394bc728e6a725de 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
@@ -67,8 +67,19 @@ extern __thread int errno;
# error "Unknown convention for errno definition"
#endif
+/* TODO: May not be utterly portable */
+#include <libio.h>
+
+extern struct _IO_FILE *stdin; /* Standard input stream. */
+extern struct _IO_FILE *stdout; /* Standard output stream. */
+extern struct _IO_FILE *stderr; /* Standard error output stream. */
+
void collect_safe_locations() {
/* Tracking of errno */
add_safe_location((uintptr_t)&errno, sizeof(int), "errno");
+ /* Tracking standard streams */
+ add_safe_location((uintptr_t)stdout, sizeof(struct _IO_FILE), "stdout");
+ add_safe_location((uintptr_t)stderr, sizeof(struct _IO_FILE), "stderr");
+ add_safe_location((uintptr_t)stdin, sizeof(struct _IO_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 dcbcd31994740c244779015c585b614e21844217..a740e1e360c7fd0646467249027c2b6d61182a33 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
@@ -155,6 +155,7 @@ static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
collect_safe_locations();
int i;
for (i = 0; i < safe_location_counter; i++) {
+ DLOG("Safe location %lu\n", safe_locations[i].address, safe_locations[i].address + safe_locations[i].length);
void *addr = (void*)safe_locations[i].address;
uintptr_t len = safe_locations[i].length;
shadow_alloca(addr, len);
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 a3562a7d679193333a837379209c3d7c8f2e78aa..afe67693198baa0603f74fffa61d121d46732c46 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
@@ -71,7 +71,7 @@ char *strerror(int errnum);
#define PGM_HEAP_SIZE (256 * MB)
/*! \brief Size of a program's Thread-local storage (TLS) */
-#define PGM_TLS_SIZE (8 * MB)
+#define PGM_TLS_SIZE (16 * MB)
/* }}} */
/** Thread-local storage information {{{ */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
index b61258b90e22ac831e276a49b9477e3442ce4a3b..fc39fb8d82f92be7a2871ef87a102350d0bb201b 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
@@ -1,42 +1,53 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
-char *__gen_e_acsl_literal_string_2;
-char *__gen_e_acsl_literal_string;
void __e_acsl_globals_init(void)
{
- __gen_e_acsl_literal_string_2 = "wb";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("wb"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
- __gen_e_acsl_literal_string = "/tmp/foo";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
- sizeof("/tmp/foo"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_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));
return;
}
int main(void)
{
int __retres;
- FILE *f;
- FILE *f2;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& f),(size_t)8);
- __e_acsl_full_init((void *)(& f));
- f = stdout;
- f2 = __gen_e_acsl_fopen(__gen_e_acsl_literal_string,
- __gen_e_acsl_literal_string_2);
- /*@ assert f ≡ __fc_stdout; */
- __e_acsl_assert(f == stdout,(char *)"Assertion",(char *)"main",
- (char *)"f == __fc_stdout",10);
+ /*@ assert \valid(__fc_stderr); */
+ {
+ {
+ int __gen_e_acsl_valid;
+ __gen_e_acsl_valid = __e_acsl_valid((void *)stderr,sizeof(FILE));
+ __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(__fc_stderr)",8);
+ }
+ }
+ /*@ assert \valid(__fc_stdin); */
+ {
+ {
+ int __gen_e_acsl_valid_2;
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stdin,sizeof(FILE));
+ __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
+ (char *)"main",(char *)"\\valid(__fc_stdin)",9);
+ }
+ }
+ /*@ assert \valid(__fc_stdout); */
+ {
+ {
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)stdout,sizeof(FILE));
+ __e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Assertion",
+ (char *)"main",(char *)"\\valid(__fc_stdout)",10);
+ }
+ }
__retres = 0;
__e_acsl_delete_block((void *)(& stdout));
- __e_acsl_delete_block((void *)(& f));
+ __e_acsl_delete_block((void *)(& stdin));
+ __e_acsl_delete_block((void *)(& stderr));
__e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
index 53d24663ffc0de50e36ce79d6669f42418b1df3a..38c5e3a415ed6def49191034606c87e5ec8eebb5 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
@@ -1,12 +1,7 @@
[e-acsl] beginning translation.
-[e-acsl] warning: annotating undefined function `fopen':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
-tests/runtime/stdout.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-FRAMAC_SHARE/libc/stdio.h:109:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-tests/runtime/stdout.c:10:[value] warning: assertion got status unknown.
+tests/runtime/stdout.c:8:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/runtime/stdout.c:9:[value] warning: assertion got status unknown.
+tests/runtime/stdout.c:10:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/stdout.c b/src/plugins/e-acsl/tests/runtime/stdout.c
index b19a951d5327af5d3b4966a151d15d63f9725cf5..0238e9d99a5bc81c1c2720f928cf98a4fd2d0465 100644
--- a/src/plugins/e-acsl/tests/runtime/stdout.c
+++ b/src/plugins/e-acsl/tests/runtime/stdout.c
@@ -1,11 +1,12 @@
/* run.config
- COMMENT: __fc_stdout et __fc_fopen
+ COMMENT: ensure that standard streams are properly tracked
*/
-#include<stdio.h>
+#include <stdio.h>
-int main(){
- FILE *f = stdout;
- FILE *f2 = fopen("/tmp/foo","wb");
- //@ assert f == stdout;
+int main(void) {
+ /*@assert \valid(stderr); */
+ /*@assert \valid(stdin); */
+ /*@assert \valid(stdout); */
+ return 0;
}