diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b3bc99ee8cc49b35541f327ae5ef0d46f77e55c6..b5121c2d3184849c106747d428b34dfc1a06234d 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6498,16 +6498,17 @@ and doExp local_env
         | Lval (Var fv, NoOffset) -> Cil.is_special_builtin fv.vname
         | _ -> false
       in
-      let init_chunk = unspecified_chunk empty in
       (* Do the arguments. In REVERSE order !!! Both GCC and MSVC do this *)
-      let rec loopArgs = function
+      let rec loopArgs
+          ?(init_chunk=unspecified_chunk empty) ?(are_ghost=false)
+        = function
         | ([], []) ->
           (match argTypes, f''.enode with
            | None, Lval (Var f,NoOffset) ->
              (* we call a function without prototype with 0 argument.
                 Hence, it really has no parameter.
              *)
-             if not isSpecialBuiltin then begin
+             if not isSpecialBuiltin && not are_ghost then begin
                warn_no_proto f;
                let typ = TFun (resType, Some [], false,attrs) in
                Cil.update_var_type f typ;
@@ -6520,11 +6521,13 @@ and doExp local_env
         | _, [] ->
           if not isSpecialBuiltin then
             Kernel.error ~once:true ~current:true
-              "Too few arguments in call to %a." Cil_printer.pp_exp f' ;
+              "Too few %s in call to %a."
+              ((if are_ghost then "ghost " else "") ^ "arguments")
+              Cil_printer.pp_exp f' ;
           (init_chunk, [])
 
         | ((_, at, _) :: atypes, a :: args) ->
-          let (ss, args') = loopArgs (atypes, args) in
+          let (ss, args') = loopArgs ~init_chunk ~are_ghost (atypes, args) in
           (* Do not cast as part of translating the argument. We let
            * the castTo do this work. This was necessary for
            * test/small1/union5, in which a transparent union is passed
@@ -6597,7 +6600,9 @@ and doExp local_env
           if not isvar && argTypes != None && not isSpecialBuiltin then
             (* Do not give a warning for functions without a prototype*)
             Kernel.error ~once:true ~current:true
-              "Too many arguments in call to %a" Cil_printer.pp_exp f';
+              "Too many %s in call to %a"
+              ((if are_ghost then "ghost " else "") ^ "arguments")
+              Cil_printer.pp_exp f';
           let rec loop = function
               [] -> (init_chunk, [])
             | a :: args ->
@@ -6646,7 +6651,15 @@ and doExp local_env
            *)
           )
       in
-      let (sargs, args') = loopArgs (argTypesList, args) in
+      let (argTypes, ghostArgTypes) = List.partition
+          (fun (_, _, a) ->
+             not (Cil.hasAttribute Cil.frama_c_ghost a) || ghost)
+          argTypesList
+      in
+      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 *)
       let s0 = unspecified_chunk empty in
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 48d16d33ede11204ea596431f60f7ee9a7872f2d..7b2bd0d30b95d3c5e381d8529c292b328a0e429e 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -873,24 +873,29 @@ class cil_printer () = object (self)
        | Lval(Var _, _) -> self#exp fmt e
        | _ -> fprintf fmt "(%a)"  self#exp e);
 
-      let must_ghost_param_list =
-        let (_, param_types, _, _) = Cil.splitFunctionType (Cil.typeOf e) in
-        let attrs = List.map (fun (_,_,a) -> a) (Cil.argsToList param_types) in
-        List.map (Cil.hasAttribute Cil.frama_c_ghost) attrs
-      in
-      let args, ghost_args =
-        let p = List.combine must_ghost_param_list args in
-        let (ghost_args, args) = List.partition
-            (fun (t, _) -> t && not is_ghost)
-            p
-        in
-        snd (List.split args) , snd (List.split ghost_args)
+      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
+        (* it means we have a va_list *)
+        | [], args ->
+          args, []
+        (* all remaining arguments are necessarily ghosts *)
+        | t :: _ , args when is_ghost_type t ->
+          [], args
+        | _ :: l , a :: args' ->
+          let (args, ghosts) = split (l, args') in
+          (a :: args, ghosts)
+        (* it could not typecheck *)
+        | _ :: _ , [] -> assert false
       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;
       (* Now the ghost arguments *)
-      Pretty_utils.pp_list ~pre:"/*@@ ghost (" ~suf:") */" self#exp fmt ghost_args;
+      Pretty_utils.pp_list ~pre:"/*@@ ghost (" ~suf:") */" self#exp fmt ghosts;
       (* Now the terminator *)
       fprintf fmt "%s" instr_terminator
     in
@@ -1904,7 +1909,7 @@ class cil_printer () = object (self)
         | None -> None, []
         | Some l ->
           let ghost_args, args = List.partition is_ghost l in
-          (match args with [] -> None | _ -> Some args), ghost_args
+          Some args, ghost_args
       in
       let pp_params fmt (args, ghost_args) pp_args =
         fprintf fmt "%t(@[%t@])" name'