Merge branch 'julien/bugfix/main-precondition-mmodel' into 'master'

fix 'segfault' in the generated code when the main has a precondition depending on the memory model

See merge request frama-c/e-acsl!174

src/plugins/e-acsl/doc/Changelog

@@ -15,6 +15,9 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2017/11/27] Fix 'segmentation fault' of the generated monitor
+	        whenever the main as a precondition depending on the memory
+	        model.
 -* E-ACSL       [2017/11/27] Restore behavior of option -e-acsl-valid broken
 	        since Phosphorus (included).
 -* E-ACSL       [2017/10/25] Fix bug #2303 about unnamed formals in

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

@@ -4,11 +4,11 @@
 
 #include <string.h>
 
+/*@ requires \valid(&argc);
+  @ requires \valid(&argv); */
 int main(int argc, char **argv) {
   int i;
 
-  /*@ assert \valid(&argc) ; */
-  /*@ assert \valid(&argv) ; */
   /*@ assert \forall int k; 0 <= k && k < argc ==> \valid(argv + k) ; */
   /*@ assert \block_length(argv) == (argc+1)*sizeof(char*) ; */
 

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

@@ -7,7 +7,6 @@ int main(void);
 int __gen_e_acsl_main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   goto L1;
   L1:
   /*@ assert X ≡ 0; */
@@ -38,6 +37,7 @@ int __gen_e_acsl_main(void)
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __retres = __gen_e_acsl_main();
   __e_acsl_assert(X == 3,(char *)"Postcondition",(char *)"main",
                   (char *)"X == 3",7);

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

 /* Generated by Frama-C */
 #include "stdlib.h"
 #include "string.h"
-int main(int argc, char **argv)
+/*@ requires \valid(&argc);
+    requires \valid(&argv); */
+int main(int argc, char **argv);
+
+int __gen_e_acsl_main(int argc, char **argv)
 {
   int __retres;
   int i;
-  __e_acsl_memory_init(& argc,& argv,(size_t)8);
-  /*@ assert \valid(&argc); */
-  {
-    int __gen_e_acsl_valid;
-    __gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int),
-                                        (void *)(& argc),(void *)0);
-    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
-                    (char *)"\\valid(&argc)",10);
-  }
-  /*@ assert \valid(&argv); */
-  {
-    int __gen_e_acsl_valid_2;
-    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& argv),sizeof(char **),
-                                          (void *)(& argv),(void *)0);
-    __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",(char *)"main",
-                    (char *)"\\valid(&argv)",11);
-  }
   /*@ assert ∀ int k; 0 ≤ k < argc ⇒ \valid(argv + k); */
   {
     int __gen_e_acsl_forall;
     int __gen_e_acsl_k;
+    __e_acsl_store_block((void *)(& argv),(size_t)8);
     __gen_e_acsl_forall = 1;
     __gen_e_acsl_k = 0;
     while (1) {
       if (__gen_e_acsl_k < argc) ; else break;
       {
-        int __gen_e_acsl_valid_3;
-        __gen_e_acsl_valid_3 = __e_acsl_valid((void *)(argv + __gen_e_acsl_k),
-                                              sizeof(char *),(void *)argv,
-                                              (void *)(& argv));
-        if (__gen_e_acsl_valid_3) ;
+        int __gen_e_acsl_valid;
+        __gen_e_acsl_valid = __e_acsl_valid((void *)(argv + __gen_e_acsl_k),
+                                            sizeof(char *),(void *)argv,
+                                            (void *)(& argv));
+        if (__gen_e_acsl_valid) ;
         else {
           __gen_e_acsl_forall = 0;
           goto e_acsl_end_loop1;
@@ -86,7 +74,7 @@ int main(int argc, char **argv)
                                                     sizeof(char *));
     if (__gen_e_acsl_initialized) {
       int __gen_e_acsl_valid_read_2;
-      int __gen_e_acsl_valid_4;
+      int __gen_e_acsl_valid_2;
       __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(argv + argc),
                                                       sizeof(char *),
                                                       (void *)argv,
@@ -94,11 +82,11 @@ int main(int argc, char **argv)
       __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
                       (char *)"mem_access: \\valid_read(argv + argc)",16);
       /*@ assert Value: mem_access: \valid_read(argv + argc); */
-      __gen_e_acsl_valid_4 = __e_acsl_valid((void *)*(argv + argc),
+      __gen_e_acsl_valid_2 = __e_acsl_valid((void *)*(argv + argc),
                                             sizeof(char),
                                             (void *)*(argv + argc),
                                             (void *)(argv + argc));
-      __gen_e_acsl_and = __gen_e_acsl_valid_4;
+      __gen_e_acsl_and = __gen_e_acsl_valid_2;
     }
     else __gen_e_acsl_and = 0;
     __e_acsl_assert(! __gen_e_acsl_and,(char *)"Assertion",(char *)"main",
@@ -118,7 +106,7 @@ int main(int argc, char **argv)
                                                           sizeof(char *));
         if (__gen_e_acsl_initialized_2) {
           int __gen_e_acsl_valid_read_3;
-          int __gen_e_acsl_valid_5;
+          int __gen_e_acsl_valid_3;
           __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(argv + i),
                                                           sizeof(char *),
                                                           (void *)argv,
@@ -126,11 +114,11 @@ int main(int argc, char **argv)
           __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
                           (char *)"main",
                           (char *)"mem_access: \\valid_read(argv + i)",19);
-          __gen_e_acsl_valid_5 = __e_acsl_valid((void *)*(argv + i),
+          __gen_e_acsl_valid_3 = __e_acsl_valid((void *)*(argv + i),
                                                 sizeof(char),
                                                 (void *)*(argv + i),
                                                 (void *)(argv + i));
-          __gen_e_acsl_and_2 = __gen_e_acsl_valid_5;
+          __gen_e_acsl_and_2 = __gen_e_acsl_valid_3;
         }
         else __gen_e_acsl_and_2 = 0;
         __e_acsl_assert(__gen_e_acsl_and_2,(char *)"Assertion",
@@ -146,7 +134,7 @@ int main(int argc, char **argv)
           if (__gen_e_acsl_k_2 <= len) ; else break;
           {
             int __gen_e_acsl_valid_read_4;
-            int __gen_e_acsl_valid_6;
+            int __gen_e_acsl_valid_4;
             __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(
                                                             argv + i),
                                                             sizeof(char *),
@@ -155,11 +143,11 @@ int main(int argc, char **argv)
             __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
                             (char *)"main",
                             (char *)"mem_access: \\valid_read(argv + i)",20);
-            __gen_e_acsl_valid_6 = __e_acsl_valid((void *)(*(argv + i) + __gen_e_acsl_k_2),
+            __gen_e_acsl_valid_4 = __e_acsl_valid((void *)(*(argv + i) + __gen_e_acsl_k_2),
                                                   sizeof(char),
                                                   (void *)*(argv + i),
                                                   (void *)(argv + i));
-            if (__gen_e_acsl_valid_6) ;
+            if (__gen_e_acsl_valid_4) ;
             else {
               __gen_e_acsl_forall_2 = 0;
               goto e_acsl_end_loop2;
@@ -178,7 +166,29 @@ int main(int argc, char **argv)
   }
   __retres = 0;
   __e_acsl_delete_block((void *)(& argv));
-  __e_acsl_delete_block((void *)(& argc));
+  return __retres;
+}
+
+/*@ requires \valid(&argc);
+    requires \valid(&argv); */
+int main(int argc, char **argv)
+{
+  int __retres;
+  __e_acsl_memory_init(& argc,& argv,(size_t)8);
+  {
+    int __gen_e_acsl_valid;
+    int __gen_e_acsl_valid_2;
+    __gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int),
+                                        (void *)(& argc),(void *)0);
+    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"main",
+                    (char *)"\\valid(&argc)",7);
+    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& argv),sizeof(char **),
+                                          (void *)(& argv),(void *)0);
+    __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Precondition",
+                    (char *)"main",(char *)"\\valid(&argv)",8);
+  }
+  __retres = __gen_e_acsl_main(argc,argv);
+  __e_acsl_delete_block((void *)(& argv));
   __e_acsl_memory_clean();
   return __retres;
 }

src/plugins/e-acsl/visit.ml

@@ -370,8 +370,9 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
         vi.vghost <- false;
         Builtins.update vi.vname vi;
         (* remember that we have to remove the main later (see method
-           [vfile]) *)
-        if vi.vorig_name = Kernel.MainFunction.get () then
+           [vfile]); do not use the [vorig_name] since both [main] and
+           [__e_acsl_main] have the same [vorig_name]. *)
+        if vi.vname = Kernel.MainFunction.get () then
           main_fct <- Some fundec
       | GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
         (* do not convert extern ghost variables, because they can't be linked,