[Variadic] ghost parameters taken in account

src/kernel_internals/typing/infer_annotations.ml

@@ -34,7 +34,14 @@ let assigns_from_prototype kf =
     try
       let formals = getFormalsDecl vi in
       (* Do ignore anonymous names *)
-      List.filter (fun vi -> vi.vname <> "") formals
+      let anonymous v = v.vname = "" in
+      (* Do ignore ghost if the function is not ghost *)
+      let ignorable_ghost v =
+        v.vghost && not vi.vghost in
+      let filter v =
+        not (anonymous v || ignorable_ghost v)
+      in
+      List.filter filter formals
     with Not_found -> []
     (* this may happen for function pointer used as formal parameters.*)
   in

src/plugins/variadic/extends.ml

@@ -35,6 +35,11 @@ module Typ = struct
     | TFun (_,args,_,_) -> Cil.argsToList args
     | _ -> invalid_arg "params"
 
+  let ghost_partitioned_params typ =
+    match Cil.unrollType typ with
+    | TFun (_,args,_,_) -> Cil.argsToPairOfLists args
+    | _ -> invalid_arg "params"
+
   let params_types typ =
     List.map (fun (_,typ,_) -> typ) (params typ)
 

src/plugins/variadic/extends.mli

@@ -25,6 +25,9 @@ open Cil_types
 module Typ : sig
   val attributes_less_equal : typ -> typ -> bool
   val params : typ -> (string * typ * attributes) list
+  val ghost_partitioned_params : typ ->
+    (string * typ * attributes) list *
+    (string * typ * attributes) list
   val params_types : typ -> typ list
   val params_count : typ -> int
   val is_variadic : typ -> bool

src/plugins/variadic/generic.ml

@@ -42,7 +42,9 @@ let translate_type = function
 | TFun (ret_typ, args, is_variadic, attributes) ->
     let new_args =
       if is_variadic
-      then Some (Cil.argsToList args @ [vpar])
+      then
+        let ng_args, g_args = Cil.argsToPairOfLists args in
+        Some (ng_args @ [vpar] @ g_args)
       else args
     in
     TFun (ret_typ, new_args, false, attributes)      
@@ -142,8 +144,11 @@ let translate_call ~fundec block loc mk_call callee pars =
     "Generic translation of call to variadic function.";
 
   (* Split params into static and variadic part *)
-  let static_size = List.length (Typ.params (Cil.typeOf callee)) - 1 in
-  let s_exps, v_exps = List.break static_size pars in
+  let ng_params, g_params = Typ.ghost_partitioned_params (Cil.typeOf callee) in
+  let static_size = List.length ng_params - 1 in
+  let s_exps, r_exps = List.break static_size pars in
+  let variadic_size = (List.length r_exps) - (List.length g_params) in
+  let v_exps, g_exps = List.break variadic_size r_exps in
 
   (* Create temporary variables to hold parameters *)
   let add_var i exp =
@@ -168,6 +173,6 @@ let translate_call ~fundec block loc mk_call callee pars =
   (* Translate the call *)
   let exp_vargs = Cil.mkAddrOrStartOf ~loc (Cil.var vargs) in
   let new_arg = Cil.mkCast ~force:false ~e:exp_vargs ~newt:(vpar_typ []) in
-  let new_args = s_exps @ [new_arg] in
+  let new_args = s_exps @ [new_arg] @ g_exps in
   let call = mk_call callee new_args in
   instrs @ [call]