diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 3b5d8650f347264b008925e1ed2201afce0a935f..6ac931fa6235534239245b8a59f12c954eae6fe2 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 loc descr (descrpure:bool) typ = let t' = (!typeForInsertedVar) typ in let name = get_temp_name ~ghost () in - let vi = makeVarinfo ~ghost ~temp:true false false name t' in - vi.vdecl <- loc; + let vi = makeVarinfo ~ghost ~temp:true ~decl:loc false false name t' in vi.vdescr <- Some descr; vi.vdescrpure <- descrpure; alphaConvertVarAndAddToEnv false vi @@ -4721,11 +4720,10 @@ 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 ~ghost ~referenced ~temp:isgenerated isglobal isformal n vtype + let vi = makeVarinfo ~ghost ~referenced ~temp:isgenerated ~decl:ldecl isglobal isformal n vtype in vi.vstorage <- sto; vi.vattr <- nattr; - vi.vdecl <- ldecl; vi.vdefined <- not (isFunctionType vtype) && isglobal && (sto = NoStorage || sto = Static); @@ -9040,9 +9038,8 @@ 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) as fd) = let ghost = ghost || isGhostFormalVarDecl fd in - let f = makeVarinfo ~ghost ~temp:false false true fn ft in - (f.vdecl <- loc; - f.vattr <- fa; + let f = makeVarinfo ~ghost ~temp:false ~decl:loc false true fn ft in + (f.vattr <- fa; alphaConvertVarAndAddToEnv true f) in let rec doFormals fl' ll' = diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml index eb1304e67086d9d2da413bb90e67b3dbeb56838c..9c657eab2c4640ecf81013b15a8b3b40398b6b5f 100644 --- a/src/kernel_internals/typing/oneret.ml +++ b/src/kernel_internals/typing/oneret.ml @@ -197,12 +197,11 @@ let oneret ?(callback: callback option) (f: fundec) : unit = let lastloc = ref Cil_datatype.Location.unknown in let getRetVar = let retVar : varinfo option ref = ref None in - fun loc -> + fun decl -> match !retVar with Some rv -> rv | None -> begin - let rv = makeLocalVar f "__retres" retTyp in (* don't collide *) - rv.vdecl <- loc; + let rv = makeLocalVar ~decl f "__retres" retTyp in (* don't collide *) retVar := Some rv; rv end diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index d0c3ac7a37378cb563dcb907b26abac3bb43ced6..82c100e20d027f9f0b3b9526bfcd8566ad772dea 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -601,7 +601,7 @@ let rec unrollTypeSkel = function (* Make a varinfo. Used mostly as a helper function below *) let makeVarinfo - ?(source=true) ?(temp=false) ?(referenced=false) ?(ghost=false) + ?(source=true) ?(temp=false) ?(referenced=false) ?(ghost=false) ?(decl=Location.unknown) global formal name typ = let vi = @@ -613,7 +613,7 @@ let makeVarinfo vformal = formal; vtemp = temp; vtype = typ; - vdecl = Location.unknown; + vdecl = decl; vinline = false; vattr = []; vstorage = NoStorage; @@ -5228,16 +5228,17 @@ let rec findUniqueName ?(suffix="") fdec name = let refresh_local_name fdec vi = let new_name = findUniqueName fdec vi.vname in vi.vname <- new_name -let makeLocal ?(temp=false) ?referenced ?ghost ?(formal=false) fdec name typ = +let makeLocal ?(temp=false) ?referenced ?ghost ?(formal=false) ?(decl=Location.unknown) fdec name typ = (* a helper function *) let name = findUniqueName fdec name in fdec.smaxid <- 1 + fdec.smaxid; - let vi = makeVarinfo ~temp ?referenced ?ghost false formal name typ in + let vi = makeVarinfo ~temp ?referenced ?ghost ~decl false formal name typ in vi (* Make a local variable and add it to a function *) -let makeLocalVar fdec ?scope ?(temp=false) ?referenced ?(insert = true) name typ = - let vi = makeLocal ~temp ?referenced fdec name typ in +let makeLocalVar fdec ?scope ?(temp=false) ?referenced ?(insert=true) + ?(decl=Location.unknown) name typ = + let vi = makeLocal ~temp ?referenced ~decl fdec name typ in refresh_local_name fdec vi; if insert then begin @@ -5252,8 +5253,8 @@ let makeLocalVar fdec ?scope ?(temp=false) ?referenced ?(insert = true) name typ vi let makeTempVar fdec ?insert ?(name = "__cil_tmp") ?descr ?(descrpure = true) - typ : varinfo = - let vi = makeLocalVar fdec ~temp:true ?insert name typ in + ?(decl=Location.unknown) typ : varinfo = + let vi = makeLocalVar fdec ~temp:true ?insert ~decl name typ in vi.vdescr <- descr; vi.vdescrpure <- descrpure; vi diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index ac0127f5508893459f4947bb479043bdddf631c1..a9887e7c132e40669f5ba1b2f25bbf6171ced70c 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -660,12 +660,14 @@ val splitFunctionTypeVI: [vreferenced] . The [ghost] argument defaults to [false], and corresponds to the field [vghost] . + The [decl] argument defaults to [Location.unknown], and corresponds to the field + [vdecl] . The first unnamed argument specifies whether the varinfo is for a global and the second is for formals. @modify 19.0-Potassium adds an optional ghost parameter *) val makeVarinfo: - ?source:bool -> ?temp:bool -> ?referenced:bool -> ?ghost:bool -> bool -> bool + ?source:bool -> ?temp:bool -> ?referenced:bool -> ?ghost:bool -> ?decl:Location.t -> bool -> bool -> string -> typ -> varinfo (** Make a formal variable for a function declaration. Insert it in both the @@ -697,8 +699,8 @@ val makeFormalVar: fundec -> ?ghost:bool -> ?where:string -> string -> typ -> va @modify Chlorine-20180501 the name of the variable is guaranteed to be fresh. *) val makeLocalVar: - fundec -> ?scope:block -> ?temp:bool -> ?referenced:bool -> ?insert:bool - -> string -> typ -> varinfo + fundec -> ?scope:block -> ?temp:bool -> ?referenced:bool -> ?insert:bool -> + ?decl:Location.t -> string -> typ -> varinfo (** if needed, rename the given varinfo so that its [vname] does not clash with the one of a local or formal variable of the given function. @@ -710,14 +712,15 @@ val refresh_local_name: fundec -> varinfo -> unit (** Make a temporary variable and add it to a function's slocals. The name of the temporary variable will be generated based on the given name hint so that to avoid conflicts with other locals. - Optionally, you can give the variable a description of its contents. + Optionally, you can give the variable a description of its contents and + its location. Temporary variables are always considered as generated variables. If [insert] is true (the default), the variable will be inserted among other locals of the function. The value for [insert] should only be changed if you are completely sure this is not useful. *) val makeTempVar: fundec -> ?insert:bool -> ?name:string -> ?descr:string -> - ?descrpure:bool -> typ -> varinfo + ?descrpure:bool -> ?decl:Location.t -> typ -> varinfo (** Make a global variable. Your responsibility to make sure that the name is unique. [source] defaults to [true]. [temp] defaults to [false].*)