diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 6ac931fa6235534239245b8a59f12c954eae6fe2..939a425daf524f8108c78c2d2306e3c0df4bc91c 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1178,7 +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 ~decl:loc false false name t' in + let vi = makeVarinfo ~ghost ~temp:true ~loc false false name t' in vi.vdescr <- Some descr; vi.vdescrpure <- descrpure; alphaConvertVarAndAddToEnv false vi @@ -4720,7 +4720,7 @@ 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 ~decl:ldecl isglobal isformal n vtype + let vi = makeVarinfo ~ghost ~referenced ~temp:isgenerated ~loc:ldecl isglobal isformal n vtype in vi.vstorage <- sto; vi.vattr <- nattr; @@ -9038,7 +9038,7 @@ 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 ~decl:loc false true fn ft in + let f = makeVarinfo ~ghost ~temp:false ~loc false true fn ft in (f.vattr <- fa; alphaConvertVarAndAddToEnv true f) in diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml index 9c657eab2c4640ecf81013b15a8b3b40398b6b5f..d90fd7e2f48de72252b615b24978ee2cced72fdb 100644 --- a/src/kernel_internals/typing/oneret.ml +++ b/src/kernel_internals/typing/oneret.ml @@ -197,11 +197,12 @@ 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 decl -> + fun loc -> match !retVar with Some rv -> rv | None -> begin - let rv = makeLocalVar ~decl f "__retres" retTyp in (* don't collide *) + let rv = makeLocalVar ~loc 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 82c100e20d027f9f0b3b9526bfcd8566ad772dea..924ce6b3312eb3ca4ef719345d7ee2d22a087794 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) ?(decl=Location.unknown) + ?(source=true) ?(temp=false) ?(referenced=false) ?(ghost=false) ?(loc=Location.unknown) global formal name typ = let vi = @@ -613,7 +613,7 @@ let makeVarinfo vformal = formal; vtemp = temp; vtype = typ; - vdecl = decl; + vdecl = loc; vinline = false; vattr = []; vstorage = NoStorage; @@ -5228,17 +5228,16 @@ 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) ?(decl=Location.unknown) fdec name typ = +let makeLocal ?(temp=false) ?referenced ?ghost ?(formal=false) ?loc fdec name typ = (* a helper function *) let name = findUniqueName fdec name in fdec.smaxid <- 1 + fdec.smaxid; - let vi = makeVarinfo ~temp ?referenced ?ghost ~decl false formal name typ in + let vi = makeVarinfo ~temp ?referenced ?ghost ?loc 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) - ?(decl=Location.unknown) name typ = - let vi = makeLocal ~temp ?referenced ~decl fdec name typ in +let makeLocalVar fdec ?scope ?(temp=false) ?referenced ?(insert=true) ?loc name typ = + let vi = makeLocal ~temp ?referenced ?loc fdec name typ in refresh_local_name fdec vi; if insert then begin @@ -5252,9 +5251,8 @@ let makeLocalVar fdec ?scope ?(temp=false) ?referenced ?(insert=true) end; vi -let makeTempVar fdec ?insert ?(name = "__cil_tmp") ?descr ?(descrpure = true) - ?(decl=Location.unknown) typ : varinfo = - let vi = makeLocalVar fdec ~temp:true ?insert ~decl name typ in +let makeTempVar fdec ?insert ?(name = "__cil_tmp") ?descr ?(descrpure = true) ?loc typ : varinfo = + let vi = makeLocalVar fdec ~temp:true ?insert ?loc name typ in vi.vdescr <- descr; vi.vdescrpure <- descrpure; vi @@ -5303,10 +5301,10 @@ let setMaxId (f: fundec) = * this one. If where = "^" then it is inserted first. If where = "$" then * it is inserted last. Otherwise where must be the name of a formal after * which to insert this. By default it is inserted at the end. *) -let makeFormalVar fdec ?(ghost=fdec.svar.vghost) ?(where = "$") name typ : varinfo = +let makeFormalVar fdec ?(ghost=fdec.svar.vghost) ?(where = "$") ?loc name typ : varinfo = assert ((not fdec.svar.vghost) || ghost) ; let makeit name = - let vi = makeLocal ~ghost ~formal:true fdec name typ in + let vi = makeLocal ~ghost ?loc ~formal:true fdec name typ in if ghost && not fdec.svar.vghost then vi.vattr <- addAttribute (Attr(frama_c_ghost_formal, [])) vi.vattr ; vi @@ -5340,14 +5338,14 @@ let makeFormalVar fdec ?(ghost=fdec.svar.vghost) ?(where = "$") name typ : varin (* Make a global variable. Your responsibility to make sure that the name * is unique *) -let makeGlobalVar ?source ?temp ?referenced name typ = - makeVarinfo ?source ?temp ?referenced true false name typ +let makeGlobalVar ?source ?temp ?referenced ?loc name typ = + makeVarinfo ?source ?temp ?referenced ?loc true false name typ let mkPureExprInstr ~fundec ~scope ?loc e = let loc = match loc with None -> e.eloc | Some l -> l in let typ = typeOf e in let descr = Format.asprintf "%a" !pp_exp_ref e in - let tmp = makeLocalVar ~temp:true ~scope fundec "tmp" typ in + let tmp = makeLocalVar ~temp:true ~scope ~loc fundec "tmp" typ in tmp.vdescr <- Some descr; tmp.vdefined <- true; Local_init(tmp, AssignInit (SingleInit e), loc) diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index a9887e7c132e40669f5ba1b2f25bbf6171ced70c..38039b32d1f24f359acf784da5d35d5bc1a8628d 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -660,14 +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 + The [loc] 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 -> ?decl:Location.t -> bool -> bool + ?source:bool -> ?temp:bool -> ?referenced:bool -> ?ghost:bool -> ?loc:Location.t -> bool -> bool -> string -> typ -> varinfo (** Make a formal variable for a function declaration. Insert it in both the @@ -686,7 +686,7 @@ val makeVarinfo: @modify 19.0-Potassium adds the optional ghost parameter *) -val makeFormalVar: fundec -> ?ghost:bool -> ?where:string -> string -> typ -> varinfo +val makeFormalVar: fundec -> ?ghost:bool -> ?where:string -> ?loc:Location.t -> string -> typ -> varinfo (** Make a local variable and add it to a function's slocals and to the given block (only if insert = true, which is the default). @@ -700,7 +700,7 @@ val makeFormalVar: fundec -> ?ghost:bool -> ?where:string -> string -> typ -> va *) val makeLocalVar: fundec -> ?scope:block -> ?temp:bool -> ?referenced:bool -> ?insert:bool -> - ?decl:Location.t -> string -> typ -> varinfo + ?loc: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. @@ -720,11 +720,11 @@ val refresh_local_name: fundec -> varinfo -> unit only be changed if you are completely sure this is not useful. *) val makeTempVar: fundec -> ?insert:bool -> ?name:string -> ?descr:string -> - ?descrpure:bool -> ?decl:Location.t -> typ -> varinfo + ?descrpure:bool -> ?loc: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].*) -val makeGlobalVar: ?source:bool -> ?temp:bool -> ?referenced:bool -> string -> +val makeGlobalVar: ?source:bool -> ?temp:bool -> ?referenced:bool -> ?loc:Location.t -> string -> typ -> varinfo (** Make a shallow copy of a [varinfo] and assign a new identifier.