diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index c45a165d3b6d6ab51bca7066374a3855b0103f08..8d78448811531844f34e139d5e8f4c770cf55480 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -635,6 +635,13 @@ let makeFormalsVarDecl (n,t,a) =
 let setFormalsDecl vi typ =
   match unrollType typ with
   | TFun(_, Some args, _, _) ->
+    let args = if vi.vghost then
+      let ghost_attr = Attr (frama_c_ghost, []) in
+      let add_attr a = addAttribute ghost_attr a in
+      List.map (fun (n,t,a) -> (n,t, add_attr a)) args
+    else
+      args
+    in
     FormalsDecl.replace vi (List.map makeFormalsVarDecl args)
   | TFun(_,None,_,_) -> ()
   | _ ->