diff --git a/src/plugins/e-acsl/src/code_generator/visit.ml b/src/plugins/e-acsl/src/code_generator/visit.ml
index 24a2372bf75a27e1869d40ad7da49b9fb2fe3c31..93874cf54d70b93973d5148cfda0a832c38cd746 100644
--- a/src/plugins/e-acsl/src/code_generator/visit.ml
+++ b/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 ();
diff --git a/src/plugins/e-acsl/tests/memory/ghost_parameters.i b/src/plugins/e-acsl/tests/memory/ghost_parameters.i
new file mode 100644
index 0000000000000000000000000000000000000000..a3577b57397f410c825ff1529b6166fbb4d2a52b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/ghost_parameters.i
@@ -0,0 +1,17 @@
+/* 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) */;
+}
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
new file mode 100644
index 0000000000000000000000000000000000000000..21e0d8d49e93362922685b0c1538a1026d24bedf
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
@@ -0,0 +1,22 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/ghost_parameters.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ghost_parameters.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/ghost_parameters.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".