From 44eb2f6eb5ad30fcab058187ca2f0caba2f91a4b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 8 Aug 2019 17:10:46 +0200
Subject: [PATCH] [Kernel] Adds an optional parameter for varinfo creation and
simplifies ghost parameters treatment
---
src/kernel_internals/typing/cabs2cil.ml | 18 +++++++-----------
src/kernel_services/ast_queries/cil.ml | 21 ++++++++++-----------
src/kernel_services/ast_queries/cil.mli | 8 +++++---
3 files changed, 22 insertions(+), 25 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 2478228b9e2..d4964c8f039 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1178,8 +1178,7 @@ let get_temp_name ?(ghost=false) () =
let newTempVar ~ghost descr (descrpure:bool) typ =
let t' = (!typeForInsertedVar) typ in
let name = get_temp_name ~ghost () in
- let vi = makeVarinfo ~temp:true false false name t' in
- vi.vghost <- ghost;
+ let vi = makeVarinfo ~ghost ~temp:true false false name t' in
vi.vdescr <- Some descr;
vi.vdescrpure <- descrpure;
alphaConvertVarAndAddToEnv false vi
@@ -4720,12 +4719,11 @@ and makeVarInfoCabs
Kernel.error ~once:true ~current:true "inline for a non-function: %s" n;
checkRestrictQualifierDeep vtype;
(* log "Looking at %s(%b): (%a)@." n isformal d_attrlist nattr;*)
- let vi = makeVarinfo ~referenced ~temp:isgenerated isglobal isformal n vtype
+ let vi = makeVarinfo ~ghost ~referenced ~temp:isgenerated isglobal isformal n vtype
in
vi.vstorage <- sto;
vi.vattr <- nattr;
vi.vdecl <- ldecl;
- vi.vghost <- ghost;
vi.vdefined <-
not (isFunctionType vtype) && isglobal && (sto = NoStorage || sto = Static);
@@ -5079,9 +5077,6 @@ 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). *)
@@ -5160,8 +5155,10 @@ and doType (ghost:bool) isFuncArg
fixupArgumentTypes 0 argl;
let arg_type_from_vi vi =
let attrs =
- if vi.vghost then addAttribute (Attr (frama_c_ghost, [])) vi.vattr
- else vi.vattr
+ if vi.vghost then
+ cabsAddAttributes [Attr (frama_c_ghost, [])] vi.vattr
+ else
+ vi.vattr
in (vi.vname, vi.vtype, attrs)
in
Some (List.map arg_type_from_vi argl)
@@ -9015,10 +9012,9 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
(* 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
+ let f = makeVarinfo ~ghost ~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_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 8d784488115..e1466020a31 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -587,7 +587,10 @@ let rec unrollTypeSkel = function
| x -> x
(* Make a varinfo. Used mostly as a helper function below *)
-let makeVarinfo ?(source=true) ?(temp=false) ?(referenced=false) global formal name typ =
+let makeVarinfo
+ ?(source=true) ?(temp=false) ?(referenced=false) ?(ghost=false)
+ global formal name typ
+ =
let vi =
{ vorig_name = name;
vname = name;
@@ -605,7 +608,7 @@ let makeVarinfo ?(source=true) ?(temp=false) ?(referenced=false) global formal n
vreferenced = referenced;
vdescr = None;
vdescrpure = true;
- vghost = false;
+ vghost = ghost;
vsource = source;
vlogic_var_assoc = None
}
@@ -626,22 +629,18 @@ module FormalsDecl =
let selfFormalsDecl = FormalsDecl.self
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 ;
+let makeFormalsVarDecl ?ghost (n,t,a) =
+ let vi = makeVarinfo ?ghost ~temp:false false true n t in
vi.vattr <- a;
vi
let setFormalsDecl vi typ =
match unrollType typ with
| TFun(_, Some args, _, _) ->
- let args = if vi.vghost then
- let ghost_attr = Attr (frama_c_ghost, []) in
- let add_attr a = addAttribute ghost_attr a in
- List.map (fun (n,t,a) -> (n,t, add_attr a)) args
- else
- args
+ let is_ghost (_, _, a) =
+ vi.vghost || hasAttribute frama_c_ghost a
in
+ let makeFormalsVarDecl x = makeFormalsVarDecl ~ghost:(is_ghost x) x in
FormalsDecl.replace vi (List.map makeFormalsVarDecl args)
| TFun(_,None,_,_) -> ()
| _ ->
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 2a4dce08908..71b9b2795cc 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -180,7 +180,7 @@ val setMaxId: fundec -> unit
val selfFormalsDecl: State.t
(** state of the table associating formals to each prototype. *)
-val makeFormalsVarDecl: (string * typ * attributes) -> varinfo
+val makeFormalsVarDecl: ?ghost:bool -> (string * typ * attributes) -> varinfo
(** creates a new varinfo for the parameter of a prototype. *)
(** Update the formals of a function declaration from its identifier and its
@@ -655,11 +655,13 @@ val splitFunctionTypeVI:
[vsource] .
The [referenced] argument defaults to [false], and corresponds to the field
[vreferenced] .
+ The [ghost] argument defaults to [false], and corresponds to the field
+ [vghost] .
The first unnamed argument specifies whether the varinfo is for a global and
the second is for formals. *)
val makeVarinfo:
- ?source:bool -> ?temp:bool -> ?referenced:bool -> bool -> bool -> string ->
- typ -> varinfo
+ ?source:bool -> ?temp:bool -> ?referenced:bool -> ?ghost:bool -> bool -> bool
+ -> string -> typ -> varinfo
(** Make a formal variable for a function declaration. Insert it in both the
sformals and the type of the function. You can optionally specify where to
--
GitLab