diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index bbb74a087c08d4657e53ffa2b68ccd63d558588a..b3bc99ee8cc49b35541f327ae5ef0d46f77e55c6 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5026,7 +5026,7 @@ and doType (ghost:bool) isFuncArg
function argument";
doDeclType (TArray(bt, lo, empty_size_cache (), al')) acc d
- | A.PROTO (d, args, _, isva) ->
+ | A.PROTO (d, args, ghost_args, isva) ->
(* Start a scope for the parameter names *)
enterScope ();
(* Intercept the old-style use of varargs.h. On GCC this means that
@@ -5055,7 +5055,8 @@ and doType (ghost:bool) isFuncArg
in
let argl_length = List.length args' in
(* Make the argument as for a formal *)
- let doOneArg (s, (n, ndt, a, cloc)) : varinfo =
+ let doOneArg is_ghost (s, (n, ndt, a, cloc)) : varinfo =
+ let ghost = is_ghost || ghost in
let s' = doSpecList ghost n s in
let vi = makeVarInfoCabs ~ghost ~isformal:true ~isglobal:false
(convLoc cloc) s' (n,ndt,a) in
@@ -5067,14 +5068,22 @@ and doType (ghost:bool) isFuncArg
Kernel.error ~once:true ~current:true
"named parameter '%s' has void type" vi.vname
end;
+ if is_ghost then begin
+ vi.vattr <- Cil.addAttribute (Attr (Cil.frama_c_ghost, [])) vi.vattr
+ end ;
(* Add the formal to the environment, so it can be referenced by
other formals (e.g. in an array type, although that will be
changed to a pointer later, or though typeof). *)
addLocalToEnv vi.vname (EnvVar vi);
vi
in
+ let make_noopt_targs ghost args =
+ List.map (doOneArg ghost) args
+ in
+ let noopt_targs = make_noopt_targs false args' in
+ let noopt_ghost_targs = make_noopt_targs true ghost_args in
let targs : varinfo list option =
- match List.map doOneArg args' with
+ match noopt_targs @ noopt_ghost_targs with
| [] -> None (* No argument list *)
| [t] when isVoidType t.vtype ->
Some []
@@ -6362,10 +6371,9 @@ and doExp local_env
intType
end
- | A.CALL(f, args,_args_ghost) ->
-(* Format.printf "Length param %i@." (List.length args);
- Format.printf "Length param %i@." (List.length args_ghost);*)
- let (rf,sf, f', ft') =
+ | 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
* function that does not have a prototype. In that case assume it
@@ -8973,9 +8981,11 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
(* Create the formals and add them to the environment. *)
(* sfg: extract tsets for the formals from dt *)
let doFormal (loc : location) (fn, ft, fa) =
+ let ghost = Cil.hasAttribute Cil.frama_c_ghost fa in
let f = makeVarinfo ~temp:false false true fn ft in
(f.vdecl <- loc;
f.vattr <- fa;
+ f.vghost <- ghost;
alphaConvertVarAndAddToEnv true f)
in
let rec doFormals fl' ll' =
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 6479d91058ce2e71434004ae60e703564459f648..48d16d33ede11204ea596431f60f7ee9a7872f2d 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -65,6 +65,7 @@ let register_shallow_attribute s =
reserved_attributes:=
(Extlib.strip_underscore s)::!reserved_attributes
+let () = register_shallow_attribute Cil.frama_c_ghost
let () = register_shallow_attribute Cil.frama_c_mutable
let () = register_shallow_attribute Cil.frama_c_init_obj
@@ -871,12 +872,25 @@ class cil_printer () = object (self)
(match e.enode with
| 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)
+ in
+
(* Now the arguments *)
Pretty_utils.pp_flowlist ~left:"(" ~sep:"," ~right:")" self#exp fmt args;
(* Now the ghost arguments *)
- Format.fprintf fmt "%t ghost " (fun fmt -> self#pp_open_annotation fmt);
- Pretty_utils.pp_flowlist ~left:"(" ~sep:"," ~right:")" self#exp fmt [] ;
- Format.fprintf fmt "@ %t" (fun fmt -> self#pp_close_annotation fmt);
+ Pretty_utils.pp_list ~pre:"/*@@ ghost (" ~suf:") */" self#exp fmt ghost_args;
(* Now the terminator *)
fprintf fmt "%s" instr_terminator
in
@@ -1885,7 +1899,14 @@ class cil_printer () = object (self)
else if nameOpt = None then printAttributes fmt a
else fprintf fmt "(%a%a)" printAttributes a pname (a <> [])
in
- let pp_params fmt args pp_args =
+ let partition_ghosts is_ghost args =
+ match args with
+ | None -> None, []
+ | Some l ->
+ let ghost_args, args = List.partition is_ghost l in
+ (match args with [] -> None | _ -> Some args), ghost_args
+ in
+ let pp_params fmt (args, ghost_args) pp_args =
fprintf fmt "%t(@[%t@])" name'
(fun fmt ->
match args with
@@ -1896,9 +1917,8 @@ class cil_printer () = object (self)
Pretty_utils.pp_list ~sep:",@ " pp_args fmt args;
if isvararg then fprintf fmt "@ , ...")
;
- Format.fprintf fmt "%t ghost (" (fun fmt -> self#pp_open_annotation fmt);
- Pretty_utils.pp_list ~sep:",@ " pp_args fmt [] ;
- Format.fprintf fmt ")@ %t" (fun fmt -> self#pp_close_annotation fmt);
+ Pretty_utils.pp_list ~pre:"/*@@ ghost (" ~suf:") */"
+ pp_args fmt ghost_args
in
let pp_params fmt = match fundecl with
| None ->
@@ -1910,12 +1930,20 @@ class cil_printer () = object (self)
(self#typ (Some (fun fmt -> fprintf fmt "%s" aname))) atype
self#attributes rest
in
- pp_params fmt args pp_args
+ let p = partition_ghosts
+ (fun (_,_,a) -> Cil.hasAttribute Cil.frama_c_ghost a)
+ args
+ in
+ pp_params fmt p pp_args
| Some fundecl ->
let args =
try Some (Cil.getFormalsDecl fundecl) with Not_found -> None
in
- pp_params fmt args self#vdecl
+ let p = partition_ghosts
+ (fun vi -> Cil.hasAttribute Cil.frama_c_ghost vi.vattr)
+ args
+ in
+ pp_params fmt p self#vdecl
in
self#typ (Some pp_params) fmt restyp
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index ef22afcb87bfa37c7133f9e6fdfc8bc8e5ccc7bf..d9fb06581ffd7420efd94ec695753b346845dfd7 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3510,6 +3510,11 @@ let typeOf_array_elem t =
| _ -> 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 () =
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 2c60334fc5ed4d032a1d2c3e885049b7ae99a9d2..6767491fb0fcc095770f75667bc6e8039d338e96 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1171,6 +1171,8 @@ val dropAttribute: string -> attributes -> attributes
* Maintains the attributes in sorted order *)
val dropAttributes: string list -> attributes -> attributes
+val frama_c_ghost: string
+
(** a field struct marked with this attribute is known to be mutable, i.e.
it can be modified even on a const object.