Merge branch 'feature/blanchard/parsing_ghost_parameters/e-acsl' into 'stable/calcium'

Better support for ghost parameters in E-ACSL

See merge request frama-c/frama-c!2461

src/plugins/e-acsl/src/code_generator/visit.ml

@@ -487,11 +487,22 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
   | g when Misc.is_library_loc (Global.loc g) ->
     if generate then Cil.JustCopy else Cil.SkipChildren
   | g ->
+    let unghost_vi vi =
+      vi.vghost <- false ;
+      vi.vtype <- match vi.vtype with
+        | TFun(res, Some l, va, attr) ->
+          let retype (n, t, a) =
+	    (n, t, Cil.dropAttribute Cil.frama_c_ghost_formal a)
+          in
+          TFun(res, Some (List.map retype l), va, attr)
+        | _ ->
+          vi.vtype
+    in
     let do_it = function
       | GVar(vi, _, _) ->
-        vi.vghost <- false
+        unghost_vi vi
       | GFun({ svar = vi } as fundec, _) ->
-        vi.vghost <- false;
+        unghost_vi vi ;
         Builtins.update vi.vname vi;
         (* remember that we have to remove the main later (see method
            [vfile]); do not use the [vorig_name] since both [main] and
@@ -502,7 +513,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
         (* do not convert extern ghost variables, because they can't be linked,
            see bts #1392 *)
         if vi.vstorage <> Extern then
-          vi.vghost <- false
+          unghost_vi vi
       | _ ->
         ()
     in
@@ -594,7 +605,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
       if Functions.instrument kf then Exit_points.generate f;
       Options.feedback ~dkey ~level:2 "entering in function %a."
         Kernel_function.pretty kf;
+      let unghost_formal vi =
+        vi.vghost <- false ;
+        vi.vattr <- Cil.dropAttribute Cil.frama_c_ghost_formal vi.vattr
+      in
       List.iter (fun vi -> vi.vghost <- false) f.slocals;
+      List.iter unghost_formal f.sformals;
       Cil.DoChildrenPost
         (fun f ->
           Exit_points.clear ();

src/plugins/e-acsl/tests/memory/ghost_parameters.i

+/* run.config
+   COMMENT: ghost parameters
+   STDOPT:
+*/
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+int main(void){
+  int w = 0 ;
+  int x = 1 ;
+  //@ ghost int y = 2 ;
+  //@ ghost int z = 3 ;
+
+  function(w, x) /*@ ghost(y, z) */;
+}

src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+void function(int a, int b, int c, int d)
+{
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  int w = 0;
+  int x = 1;
+  int y = 2;
+  int z = 3;
+  function(w,x,y,z);
+  __retres = 0;
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/memory/oracle_ci/ghost_parameters.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".