From d725f018e1fe34771b70cfa75af12d92d03c381b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@inria.fr>
Date: Sat, 6 Oct 2018 16:50:42 +0200
Subject: [PATCH] Fixes issues with tests
---
src/kernel_internals/typing/cabs2cil.ml | 27 +++++++++++----
.../ast_printing/cil_printer.ml | 33 +++++++++++--------
2 files changed, 39 insertions(+), 21 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b3bc99ee8cc..b5121c2d318 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 48d16d33ede..7b2bd0d30b9 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'
--
GitLab