diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 1004eaa7c5bba45939185b762d696e935a337dad..9ae6c1ec6b1d09c9b223aa3d33c3586d721ce8a1 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6372,7 +6372,6 @@ and doExp local_env
       end
 
     | A.CALL(f, args, ghost_args) ->
-      let args = args @ ghost_args in
       let (rf,sf, f', ft') =
         match (stripParen f).expr_node with
         (* Treat the VARIABLE case separate because we might be calling a
@@ -6651,7 +6650,8 @@ and doExp local_env
            *)
           )
       in
-      let (argTypes, ghostArgTypes) = List.partition
+      let (argTypes, ghostArgTypes) =
+        List.partition
           (fun (_, _, a) ->
              not (Cil.hasAttribute Cil.frama_c_ghost a) || ghost)
           argTypesList
@@ -6659,6 +6659,7 @@ and doExp local_env
       let args = if ghost then args @ ghost_args else args in
       let (sghost, ghosts') = loopArgs ~are_ghost:true (ghostArgTypes, ghost_args) in
       let (sargs, args') = loopArgs ~init_chunk:sghost (argTypes, args) in
+
       let (sargs, args') = (sargs, args' @ ghosts') in
       (* Setup some pointer to the elements of the call. We may change
        * these below *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index c661a2248ad38818ba05175783f6f5ad93a9b11b..6762429ff05cadbfeae382c06603ecc8c9d7968b 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -874,18 +874,20 @@ class cil_printer () = object (self)
        | _ -> fprintf fmt "(%a)"  self#exp e);
 
       let (_, param_ts, _, _) = Cil.splitFunctionType (Cil.typeOf e) in
-      let param_ts = Cil.argsToList param_ts in
-      let is_ghost_type (_, _, a) = Cil.hasAttribute Cil.frama_c_ghost a in
-
-      let rec split = function
-        | [], args -> args, []
-        | t :: _ , args when is_ghost_type t -> [], args
-        | _ :: l , a :: args' ->
-          let (args, ghosts) = split (l, args') in
-          (a :: args, ghosts)
-        | _ :: _ , [] -> assert false
+      let _, g_params_ts = Cil.argsToPairOfLists param_ts in
+
+      let rec break n l =
+        if n = 0 then [], l
+        else match l with
+          | [] -> assert false
+          | x :: l' -> let (f, s) = break (n-1) l' in x :: f, s
+      in
+      let args, ghosts = if is_ghost then
+          args, []
+        else
+          let n = List.length args - List.length g_params_ts in
+          break n args
       in
-      let args, ghosts = if is_ghost then args, [] else split (param_ts, args) in
 
       (* Now the arguments *)
       Pretty_utils.pp_flowlist ~left:"(" ~sep:"," ~right:")" self#exp fmt args;
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 264a2792759bf9fe718e6569b7e16ba403863c8b..c45a165d3b6d6ab51bca7066374a3855b0103f08 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -555,6 +555,20 @@ let partitionAttributes
   in
   loop ([], [], []) attrs
 
+let frama_c_ghost = "__fc_ghost"
+let () = registerAttribute frama_c_ghost (AttrName false)
+let () =
+  registerAttribute (Extlib.strip_underscore frama_c_ghost) (AttrName false)
+
+let frama_c_mutable = "__fc_mutable"
+let () = registerAttribute frama_c_mutable (AttrName false)
+let () =
+  registerAttribute (Extlib.strip_underscore frama_c_mutable) (AttrName false)
+
+let frama_c_init_obj = "__fc_initialized_object"
+let () = registerAttribute frama_c_init_obj (AttrName false)
+let () =
+  registerAttribute (Extlib.strip_underscore frama_c_init_obj) (AttrName false)
 
 let unrollType (t: typ) : typ =
   let rec withAttrs (al: attributes) (t: typ) : typ =
@@ -614,6 +628,7 @@ let () = dependency_on_ast selfFormalsDecl
 
 let makeFormalsVarDecl (n,t,a) =
   let vi = makeVarinfo ~temp:false false true n t in
+  vi.vghost <- hasAttribute frama_c_ghost a ;
   vi.vattr <- a;
   vi
 
@@ -3509,22 +3524,6 @@ let typeOf_array_elem t =
   | TArray (ty_elem, _, _, _) -> ty_elem
   | _ -> Kernel.fatal "Not an array type %a" !pp_typ_ref t
 
-
- let frama_c_ghost = "__fc_ghost"
- let () = registerAttribute frama_c_ghost (AttrName false)
- let () =
-   registerAttribute (Extlib.strip_underscore frama_c_ghost) (AttrName false)
-
-let frama_c_mutable = "__fc_mutable"
-let () = registerAttribute frama_c_mutable (AttrName false)
-let () =
-  registerAttribute (Extlib.strip_underscore frama_c_mutable) (AttrName false)
-
-let frama_c_init_obj = "__fc_initialized_object"
-let () = registerAttribute frama_c_init_obj (AttrName false)
-let () =
-  registerAttribute (Extlib.strip_underscore frama_c_init_obj) (AttrName false)
-
 let no_op_coerce typ t =
   match typ with
   | Lreal -> true