Merge branch 'kostyantyn/bugfix/stdstream' into 'master'

Add stdin, stderr and stdout to safe locations

See merge request !117

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

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);

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 {{{ */

src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c

 /* 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;
 }

src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle

 [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.

src/plugins/e-acsl/tests/runtime/stdout.c

 /* 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;
 }