diff --git a/src/kernel_internals/typing/alpha.mli b/src/kernel_internals/typing/alpha.mli
index 607288dbdd379bc612ae30163c631bb5908a6f99..075d2f04f5ee8169510e9534c207c32e75275881 100644
--- a/src/kernel_internals/typing/alpha.mli
+++ b/src/kernel_internals/typing/alpha.mli
@@ -71,7 +71,7 @@ type 'a alphaTable =
information will be in reverse order in which the action occurred. Returns
the new name and, if different from the lookupname, the location of the
previous occurrence. This function knows about the location implicitly
- from the [(Cil_const.CurrentLoc.get ())]. *)
+ from the [(Current_loc.get ())]. *)
val newAlphaName: alphaTable: 'a alphaTable ->
undolist: 'a undoAlphaElement list ref option ->
lookupname:string -> data:'a -> string * 'a
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 0484105bdd6253bea63c469f1be1e1a92ffca63b..f88ac0ff29e83113bb3d27abd488424a59d7ce7c 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -129,7 +129,7 @@ let cabs_exp loc node = { expr_loc = loc; expr_node = node }
let abort_context ?loc msg =
let loc = match loc with
- | None -> Cil_const.CurrentLoc.get()
+ | None -> Current_loc.get()
| Some loc -> loc
in
let append fmt =
@@ -635,7 +635,7 @@ let process_pragmas_pack_align_comp_attributes loc ci cattrs =
the minimum of both is taken into account (note that, in GCC, if a field
has 2 alignment directives, it is the maximum of those that is taken). *)
let process_pragmas_pack_align_field_attributes fi fattrs cattr =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
let<> UpdatedCurrentLoc = fi.floc in
match !current_packing_pragma, align_pragma_for_struct fi.forig_name with
| None, None -> check_aligned fattrs
@@ -970,7 +970,7 @@ let declared_in_current_scope ~ghost s =
(* When you add to env, you also add it to the current scope *)
let addLocalToEnv ghost name data =
- let v = data, Cil_const.CurrentLoc.get() in
+ let v = data, Current_loc.get() in
Datatype.String.Hashtbl.add ghost_env name v;
if not ghost then Datatype.String.Hashtbl.add env name v;
(* If we are in a scope, then it means we are not at top level. Add the
@@ -990,7 +990,7 @@ let addLocalToEnv ghost name data =
let addGlobalToEnv ghost name data =
let open Datatype.String.Hashtbl in
- let v = data, Cil_const.CurrentLoc.get () in
+ let v = data, Current_loc.get () in
add ghost_env name v;
if not ghost then add env name v;
add ghost_global_env name v;
@@ -1008,7 +1008,7 @@ let alphaTable : location Alpha.alphaTable = H.create 307
let fresh_global lookupname =
fst (Alpha.newAlphaName ~alphaTable ~undolist:None ~lookupname
- ~data:(Cil_const.CurrentLoc.get ()))
+ ~data:(Current_loc.get ()))
(* To keep different name scopes different, we add prefixes to names
* specifying the kind of name: the kind can be one of "" for variables or
@@ -1065,7 +1065,7 @@ let newAlphaName
let undolist =
match undo_scope with None -> None | Some _ -> Some (ref [])
in
- let data = Cil_const.CurrentLoc.get () in
+ let data = Current_loc.get () in
let newname, oldloc =
Alpha.newAlphaName ~alphaTable ~undolist ~lookupname ~data
in
@@ -1253,7 +1253,7 @@ let constFoldToInteger e =
let get_temp_name ghost () =
let undolist = ref [] in
- let data = Cil_const.CurrentLoc.get() in
+ let data = Current_loc.get() in
let name = if ghost then "g_tmp" else "tmp" in
let name, _ =
Alpha.newAlphaName ~alphaTable ~undolist:(Some undolist) ~lookupname:name ~data
@@ -1353,13 +1353,13 @@ let findCompType ghost kind name attr =
if kind = "enum" then
let enum, isnew = createEnumInfo name ~norig:name in
if isnew then
- cabsPushGlobal (GEnumTagDecl (enum, Cil_const.CurrentLoc.get ()));
+ cabsPushGlobal (GEnumTagDecl (enum, Current_loc.get ()));
TEnum (enum, attr)
else
let iss = if kind = "struct" then true else false in
let self, isnew = createCompInfo iss name ~norig:name in
if isnew then
- cabsPushGlobal (GCompTagDecl (self, Cil_const.CurrentLoc.get ()));
+ cabsPushGlobal (GCompTagDecl (self, Current_loc.get ()));
TComp (self, attr)
in
try
@@ -2064,7 +2064,7 @@ struct
(* Make the statement *)
let loop =
mkStmt ~ghost ~valid_sid ~sattr
- (Loop (a,c2block ~ghost body, Cil_const.CurrentLoc.get (), None, None))
+ (Loop (a,c2block ~ghost body, Current_loc.get (), None, None))
in
{ stmts = [ loop,[],[],[],[] ];
cases = body.cases;
@@ -2430,8 +2430,8 @@ class gatherLabelsClass : Cabsvisit.cabsVisitor = object (self)
ChangeDoChildrenPost (blk, fun _ -> (self#removeLocalLabels blk; blk))
method! vstmt s =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = get_statementloc s in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = get_statementloc s in
(match s.stmt_node with
| LABEL (lbl,_,_) ->
(try
@@ -2442,7 +2442,7 @@ class gatherLabelsClass : Cabsvisit.cabsVisitor = object (self)
lbl Cil_printer.pp_location oldloc
| None ->
(* Mark this label as defined *)
- H.replace localLabels lbl (Some (Cil_const.CurrentLoc.get())))
+ H.replace localLabels lbl (Some (Current_loc.get())))
with Not_found -> (* lbl is not a local label *)
let newname, oldloc =
newAlphaName s.stmt_ghost false "label" lbl
@@ -2956,9 +2956,8 @@ let rec setOneInit this o preinit =
match o with
| NoOffset -> assert false
| Index({enode = Const(CInt64(i,_,_));eloc}, off) ->
- let open Cil_const.CurrentLoc.Operators in
- let<> UpdatedCurrentLoc = eloc in
- to_integer i, off
+ let i' = Current_loc.with_loc eloc to_integer i in
+ i', off
| Field (f, off) ->
(* Find the index of the field *)
let rec loop (idx: int) = function
@@ -3029,7 +3028,7 @@ let rec collectInitializer
(* parenttype is used to identify a tentative flexible array member
initialization *)
let dkey = Kernel.dkey_typing_init in
- let loc = Cil_const.CurrentLoc.get() in
+ let loc = Current_loc.get() in
if this = NoInitPre then begin
Kernel.debug ~dkey "zero-initializing object of type %a"
Cil_datatype.Typ.pretty thistype;
@@ -3277,7 +3276,7 @@ and normalSubobj (so: subobj) : unit =
so.soTyp <- bt;
so.soOff <-
addOffset
- (Index(integer ~loc:(Cil_const.CurrentLoc.get()) !current, NoOffset))
+ (Index(integer ~loc:(Current_loc.get()) !current, NoOffset))
parOff
end
@@ -3692,10 +3691,10 @@ let consLabContinue ~ghost (c: chunk) =
| While lr :: _ ->
begin
assert (!doTransformWhile);
- if !lr = "" then c else consLabel ~ghost !lr c (Cil_const.CurrentLoc.get ()) false
+ if !lr = "" then c else consLabel ~ghost !lr c (Current_loc.get ()) false
end
| NotWhile lr :: _ ->
- if !lr = "" then c else consLabel ~ghost !lr c (Cil_const.CurrentLoc.get ()) false
+ if !lr = "" then c else consLabel ~ghost !lr c (Current_loc.get ()) false
(* Was a continue instruction used inside the current loop *)
let continueUsed () =
@@ -4403,7 +4402,7 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
in
(*TODO: find a better loc*)
- let fields = loop (zero ~loc:(Cil_const.CurrentLoc.get())) eil in
+ let fields = loop (zero ~loc:(Current_loc.get())) eil in
(* Now set the right set of items *)
enum.eitems <- List.map (fun (_, x) -> x) fields;
(* Pick the enum's kind - see discussion above *)
@@ -4433,7 +4432,7 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
(* Record the enum name in the environment *)
addLocalToEnv ghost (kindPlusName "enum" n') (EnvTyp res);
(* And define the tag *)
- cabsPushGlobal (GEnumTag (enum, Cil_const.CurrentLoc.get ()));
+ cabsPushGlobal (GEnumTag (enum, Current_loc.get ()));
res
| [Cabs.TtypeofE e] ->
@@ -5327,7 +5326,7 @@ and makeCompType loc ghost (isstruct: bool)
comp.cattr <- process_pragmas_pack_align_comp_attributes loc comp a;
let res = TComp (comp, []) in
(* Create a typedef for this one *)
- cabsPushGlobal (GCompTag (comp, Cil_const.CurrentLoc.get ()));
+ cabsPushGlobal (GCompTag (comp, Current_loc.get ()));
(* There must be a self cell created for this already *)
addLocalToEnv ghost (kindPlusName kind n) (EnvTyp res);
@@ -5408,11 +5407,11 @@ and doExp local_env
(e: Cabs.expression)
(what: expAction)
=
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
let ghost = local_env.is_ghost in
let loc = e.expr_loc in
(* will be reset at the end of the compilation of current expression. *)
- let<> CurrentLocUpdated = loc in
+ let<> UpdatedCurrentLoc = loc in
let checkVoidLval e t =
if (match e.enode with Lval _ -> true | _ -> false) && isVoidType t then
abort_context "lvalue of type void: %a@\n" Cil_printer.pp_exp e
@@ -5468,7 +5467,7 @@ and doExp local_env
([], (* the reads are incorporated in the chunk. *)
((unspecified_chunk empty) @@@ (remove_reads lv se, ghost))
+++
- (mkStmtOneInstr ~ghost ~valid_sid (Set(lv, e'', Cil_const.CurrentLoc.get ())),
+ (mkStmtOneInstr ~ghost ~valid_sid (Set(lv, e'', Current_loc.get ())),
writes,writes,
List.filter (fun x -> not (LvalStructEq.equal x lv)) r @ reads),
e'', t'')
@@ -6037,7 +6036,7 @@ and doExp local_env
(se' +++
(mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
(Set(lv, snd (castTo tresult t result),
- Cil_const.CurrentLoc.get ())),[],[lv],r'))
+ Current_loc.get ())),[],[lv],r'))
e'
t
end
@@ -6078,7 +6077,7 @@ and doExp local_env
([var tmp],
local_var_chunk se' tmp +++
(mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
- (Set(var tmp, e', Cil_const.CurrentLoc.get ())),[],[],[]),
+ (Set(var tmp, e', Current_loc.get ())),[],[],[]),
(* the tmp variable should not be investigated for
unspecified writes: it occurs at the right place in
the sequence.
@@ -6092,7 +6091,7 @@ and doExp local_env
(mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
(Set(lv,
snd (castTo tresult (typeOfLval lv) opresult),
- Cil_const.CurrentLoc.get ())),
+ Current_loc.get ())),
[],[lv], r'))
result
t
@@ -7756,7 +7755,7 @@ and doCondExp local_env asconst
and compileCondExp ?(hide=false) ~ghost ce st sf =
match ce with
| CEAnd (ce1, ce2) ->
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let (duplicable, sf1, sf2) =
(* If sf is small then will copy it *)
try (true, sf, duplicateChunk sf)
@@ -7788,7 +7787,7 @@ and compileCondExp ?(hide=false) ~ghost ce st sf =
compileCondExp ~hide ~ghost ce1 st' sf'
| CEOr (ce1, ce2) ->
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let (duplicable, st1, st2) =
(* If st is small then will copy it *)
try (true, st, duplicateChunk st)
@@ -7808,7 +7807,7 @@ and compileCondExp ?(hide=false) ~ghost ce st sf =
in
let labstmt =
if sf_fall_through then
- consLabel ~ghost lab empty (Cil_const.CurrentLoc.get ()) false
+ consLabel ~ghost lab empty (Current_loc.get ()) false
else skipChunk
in
let (@@@) s1 s2 = s1 @@@ (s2, ghost) in
@@ -8460,7 +8459,7 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
* varinfo *)
and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * Cabs.attribute list))
(((n,ndt,a,cloc), inite) : Cabs.init_name) : varinfo =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
Kernel.debug ~dkey:Kernel.dkey_typing_global "createGlobal: %s" n;
(* If the global is a Frama-C builtin, set the generated flag *)
if is_stdlib_macro n && get_current_stdheader () = "" then begin
@@ -8489,7 +8488,7 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
(* Add the variable to the environment before doing the initializer
* because it might refer to the variable itself *)
if isFunctionType vi.vtype then begin
- FuncLocs.add_loc ?spec:logic_spec (Cil_const.CurrentLoc.get ()) vi_loc n;
+ FuncLocs.add_loc ?spec:logic_spec (Current_loc.get ()) vi_loc n;
if inite != Cabs.NO_INIT then
Kernel.error ~once:true ~current:true
"Function declaration with initializer (%s)\n" vi.vname;
@@ -8586,8 +8585,8 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
vi.vstorage <- NoStorage; (* equivalent and canonical *)
IH.remove mustTurnIntoDef vi.vid;
- cabsPushGlobal (GVar(vi, {init = init}, Cil_const.CurrentLoc.get ()));
- H.add alreadyDefined vi.vname (Cil_const.CurrentLoc.get ());
+ cabsPushGlobal (GVar(vi, {init = init}, Current_loc.get ()));
+ H.add alreadyDefined vi.vname (Current_loc.get ());
vi
end else begin
if not (isFunctionType vi.vtype) &&
@@ -8604,11 +8603,11 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
setFormalsDecl vi vi.vtype;
let spec, loc =
match logic_spec with
- | None -> empty_funspec (), Cil_const.CurrentLoc.get ()
+ | None -> empty_funspec (), Current_loc.get ()
| Some (spec,loc) ->
begin
- let<> CurrentLocUpdated = loc in
- let loc = Cil_const.CurrentLoc.get () in
+ let<> UpdatedCurrentLoc = loc in
+ let loc = Current_loc.get () in
let res =
try
(* it can not have old behavior names, since this is the
@@ -8626,7 +8625,7 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
cabsPushGlobal (GFunDecl (spec, vi, loc));
end
else
- cabsPushGlobal (GVarDecl (vi, Cil_const.CurrentLoc.get ()));
+ cabsPushGlobal (GVarDecl (vi, Current_loc.get ()));
vi
end else begin
Kernel.debug ~dkey:Kernel.dkey_typing_global
@@ -8634,7 +8633,6 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
(match logic_spec with
| None -> ()
| Some (spec,loc) ->
- let<> CurrentLocUpdated = loc in
let merge_spec = function
| GFunDecl(old_spec, _, oldloc) ->
let behaviors =
@@ -8652,7 +8650,7 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
Logic_utils.merge_funspec ~oldloc old_spec spec
| _ -> assert false
in
- update_fundec_in_theFile vi merge_spec
+ Current_loc.with_loc loc (update_fundec_in_theFile vi) merge_spec
);
vi
end
@@ -8812,13 +8810,13 @@ and createLocal ghost ((_, sto, _, _) as specs)
Push a prototype for the function, just in case. *)
cabsPushGlobal
(GFunDecl (empty_funspec (), !currentFunctionFDEC.svar,
- Cil_const.CurrentLoc.get ()));
+ Current_loc.get ()));
Cil.setFormalsDecl
!currentFunctionFDEC.svar !currentFunctionFDEC.svar.vtype;
Some ie'
end
in
- cabsPushGlobal (GVar(vi, {init = init}, Cil_const.CurrentLoc.get ()));
+ cabsPushGlobal (GVar(vi, {init = init}, Current_loc.get ()));
static_var_chunk empty vi
(* Maybe we have an extern declaration. Make it a global *)
@@ -8883,7 +8881,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
assert alloca_bounds: 0 < elt_size * array_size <= max_bounds
*)
(se0 +++ (
- let castloc = Cil_const.CurrentLoc.get () in
+ let castloc = Current_loc.get () in
let talloca_size =
let size = Logic_utils.expr_to_term ~coerce:true elt_size in
let tlen = Logic_utils.expr_to_term ~coerce:true len in
@@ -8915,7 +8913,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
let setlen = se0 +++
(mkStmtOneInstr ~ghost ~valid_sid
(Set(var savelen, mkCast ~newt:savelen.vtype len,
- Cil_const.CurrentLoc.get ())),
+ Current_loc.get ())),
[],[],[])
in
(* Initialize the variable *)
@@ -8945,7 +8943,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
(vi,AssignInit
(SingleInit
(mkCast ~newt:vi.vtype (new_exp ~loc (Lval(var tmp))))),
- Cil_const.CurrentLoc.get ())),
+ Current_loc.get ())),
[],[var vi],[var tmp])
end
end else empty
@@ -9046,8 +9044,8 @@ and doAliasFun ghost vtype (thisname:string) (othername:string)
(* Do one declaration *)
and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = get_definitionloc def in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = get_definitionloc def in
match def with
| Cabs.DECDEF (logic_spec, (s, nl), loc) ->
(* Do the specifiers exactly once *)
@@ -9075,13 +9073,13 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
if not (isFunctionType vtype) || local_env.is_ghost then begin
Kernel.warning ~current:true
"%a: CIL only supports attribute((alias)) for C functions."
- Cil_printer.pp_location (Cil_const.CurrentLoc.get ());
+ Cil_printer.pp_location (Current_loc.get ());
ignore (createGlobal l ghost logic_spec spec_res name)
end else
doAliasFun ghost vtype n othername (s, (n,ndt,a,l)) loc
| _ ->
Kernel.error ~once:true ~current:true
- "Bad alias attribute at %a" Cil_printer.pp_location (Cil_const.CurrentLoc.get()));
+ "Bad alias attribute at %a" Cil_printer.pp_location (Current_loc.get()));
acc
end else
acc @@@ (createLocal ghost spec_res name, ghost)
@@ -9116,7 +9114,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
doOnlyTypedef local_env.is_ghost s; empty
| Cabs.GLOBASM (s, _) when isglobal ->
- cabsPushGlobal (GAsm (s, Cil_const.CurrentLoc.get ())); empty
+ cabsPushGlobal (GAsm (s, Current_loc.get ())); empty
| Cabs.PRAGMA (a, _) when isglobal -> begin
match doAttr local_env.is_ghost ("dummy", [a]) with
@@ -9133,7 +9131,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
in
Option.iter
(fun a'' ->
- cabsPushGlobal (GPragma (a'', Cil_const.CurrentLoc.get ())))
+ cabsPushGlobal (GPragma (a'', Current_loc.get ())))
a'';
empty
@@ -9274,7 +9272,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
| [], _ -> []
| fl, [] -> (* no more locs available *)
- List.map (doFormal (Cil_const.CurrentLoc.get ())) fl
+ List.map (doFormal (Current_loc.get ())) fl
| f::fl, (_,(_,_,_,l))::ll ->
(* sfg: these lets seem to be necessary to
@@ -9369,7 +9367,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
begin
match spec with
| Some (spec,loc) ->
- let<> CurrentLocUpdated = loc in
+ let<> UpdatedCurrentLoc = loc in
(try
!currentFunctionFDEC.sspec <-
Ltyping.funspec behaviors
@@ -9464,7 +9462,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
(* A new shadow to be placed in the formals. Use
* makeTempVar to update smaxid and all others but
do not insert as a local variable of [f]. *)
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let shadow =
makeTempVar
!currentFunctionFDEC ~insert:false
@@ -9487,7 +9485,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
(* Now see whether we can fall through to the end of the function *)
if blockFallsThrough !currentFunctionFDEC.sbody then begin
let loc = endloc in
- let<> CurrentLocUpdated = endloc in
+ let<> UpdatedCurrentLoc = endloc in
let protect_return,retval =
(* Guard the [return] instructions we add with an
[\assert \false]*)
@@ -9565,7 +9563,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
List.iter
(fun decl ->
let loc = convLoc decl.Logic_ptree.decl_loc in
- let<> CurrentLocUpdated = loc in
+ let<> UpdatedCurrentLoc = loc in
try
let tdecl = Ltyping.annot decl in
let attr = fc_stdlib_attribute [] in
@@ -9573,7 +9571,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
List.fold_left
(Fun.flip Logic_utils.add_attribute_glob_annot) tdecl attr
in
- cabsPushGlobal (GAnnot(tdecl,Cil_const.CurrentLoc.get ()))
+ cabsPushGlobal (GAnnot(tdecl,Current_loc.get ()))
with LogicTypeError ((source,_),msg) ->
Kernel.warning
~wkey:Kernel.wkey_annot_error ~source
@@ -9689,7 +9687,7 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
(* Register the type. register it as local because we might be in a
* local context *)
addLocalToEnv ghost (kindPlusName "type" n) (EnvTyp namedTyp);
- cabsPushGlobal (GType (ti, Cil_const.CurrentLoc.get ()))
+ cabsPushGlobal (GType (ti, Current_loc.get ()))
end
in
List.iter createTypedef nl
@@ -9724,12 +9722,12 @@ and doOnlyTypedef ghost (specs: Cabs.spec_elem list) : unit =
ci.cattr <- cabsAddAttributes ci.cattr al;
(* The GCompTag was already added *)
end else (* Add a GCompTagDecl *)
- cabsPushGlobal (GCompTagDecl(ci, Cil_const.CurrentLoc.get ()))
+ cabsPushGlobal (GCompTagDecl(ci, Current_loc.get ()))
| TEnum(ei, al) ->
if isadef then begin
ei.eattr <- cabsAddAttributes ei.eattr al;
end else
- cabsPushGlobal (GEnumTagDecl(ei, Cil_const.CurrentLoc.get ()))
+ cabsPushGlobal (GEnumTagDecl(ei, Current_loc.get ()))
| _ ->
Kernel.warning ~current:true ~wkey:Kernel.wkey_unnamed_typedef
"Ignoring unnamed typedef that does not introduce a struct or \
@@ -9839,7 +9837,7 @@ and doBodyScope local_env blk =
enterScope (); let res = doBody local_env blk in exitScope (); res
and doStatement local_env (s : Cabs.statement) : chunk =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
let mk_loop_annot a loc =
try
List.map
@@ -9853,7 +9851,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
in
let ghost = s.stmt_ghost in
let local_env = { local_env with is_ghost = ghost } in
- let<> CurrentLocUpdated = convLoc (get_statementloc s) in
+ let<> UpdatedCurrentLoc = convLoc (get_statementloc s) in
match s.stmt_node with
| Cabs.NOP loc ->
{ empty
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index 59666e7574f1d0a52635658465e5f25d12bf242c..7da177464c06d83a1dc793427313bd23c4946af4 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -352,7 +352,7 @@ let freshLabel (base:string) =
let xform_switch_block ?(keepSwitch=false) b =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
let breaks_stack = Stack.create () in
let continues_stack = Stack.create () in
(* NB: these are two stacks of stack, as the scope of
@@ -440,7 +440,7 @@ let xform_switch_block ?(keepSwitch=false) b =
[] -> []
| s :: rest ->
begin
- let<> CurrentLocUpdated = Stmt.loc s in
+ let<> UpdatedCurrentLoc = Stmt.loc s in
if not keepSwitch then
s.labels <- List.map (fun lab -> match lab with
Label _ -> lab
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index 15ec967abf8c89d32cbed9cbd07aa15dc32d5086..5394ebbc58faf43ad2992b8e5520e0701142b6f1 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -115,7 +115,7 @@ class visitor = object(self)
method private bad_ghost_function kf =
let source = match prefered_loc with
- | None -> fst (Cil_const.CurrentLoc.get())
+ | None -> fst (Current_loc.get())
| Some l -> l
in
Error.cannot_check_ghost_call ~source ~current:true ~once:true kf
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 0f950a6eb62759451870e62e9917ad3eabf1e5bf..cca4dd7a60ff1f685d7ba89a3f76939a0b4f7a11 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -866,8 +866,8 @@ let rec global_annot_without_irrelevant_attributes ga =
| Dfun_or_pred _ | Dtype_annot _ | Dmodel_annot _ | Dinvariant _ -> ga
let rec global_annot_pass1 g =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Cil_datatype.Global_annotation.loc g in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Cil_datatype.Global_annotation.loc g in
match g with
| Dvolatile(hs,rvi,wvi,_,loc) ->
let process_term_kind (t,k as id) =
@@ -1568,7 +1568,7 @@ let remove_function_statics fdec =
) !theFile
let oneFilePass1 (f:file) : unit =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
H.add fileNames !currentFidx f.fileName;
Kernel.feedback ~dkey:Kernel.dkey_linker
"Pre-merging (%d) %a" !currentFidx Filepath.Normalized.pp_abs f.fileName ;
@@ -1583,7 +1583,7 @@ let oneFilePass1 (f:file) : unit =
* *)
let matchVarinfo ~fromGFun (vi: varinfo) (loc, _ as l) =
ignore (Alpha.registerAlphaName ~alphaTable:vtAlpha
- ~lookupname:vi.vname ~data:(Cil_const.CurrentLoc.get ()));
+ ~lookupname:vi.vname ~data:(Current_loc.get ()));
(* Make a node for it and put it in vEq *)
let vinode =
PlainMerging.mkSelfNode vEq vSyn !currentFidx vi.vname vi (Some l)
@@ -1709,7 +1709,7 @@ let oneFilePass1 (f:file) : unit =
newrep.ndata.vdecl <- newdecl
in
let iter g =
- let<> CurrentLocUpdated = Cil_datatype.Global.loc g in
+ let<> UpdatedCurrentLoc = Cil_datatype.Global.loc g in
match g with
| GVarDecl (vi, l) | GVar (vi, _, l) | GFunDecl (_, vi, l)->
incr currentDeclIdx;
@@ -2194,8 +2194,8 @@ end
let renameInlinesVisitor = new renameInlineVisitorClass
let rec logic_annot_pass2 ~in_axiomatic g a =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Cil_datatype.Global_annotation.loc a in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Cil_datatype.Global_annotation.loc a in
match a with
| Dfun_or_pred (li, _) ->
begin
@@ -2557,7 +2557,7 @@ let oneFilePass2 (f: file) =
let visited = ref Cil_datatype.Varinfo.Set.empty in
let visit vi = visited := Cil_datatype.Varinfo.Set.add vi !visited in
let processOneGlobal (g: global) : unit =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
(* Process a varinfo. Reuse an old one, or rename it if necessary *)
let processVarinfo (vi: varinfo) (vloc: location) : varinfo =
if Cil_datatype.Varinfo.Set.mem vi !visited then vi
@@ -2566,7 +2566,7 @@ let oneFilePass2 (f: file) =
if vi.vstorage = Static then begin
let newName, _ =
Alpha.newAlphaName ~alphaTable:vtAlpha ~undolist:None
- ~lookupname:vi.vname ~data:(Cil_const.CurrentLoc.get ())
+ ~lookupname:vi.vname ~data:(Current_loc.get ())
in
let formals_decl =
try Some (Cil.getFormalsDecl vi)
@@ -2605,7 +2605,7 @@ let oneFilePass2 (f: file) =
end
end
in
- let<> CurrentLocUpdated = Cil_datatype.Global.loc g in
+ let<> UpdatedCurrentLoc = Cil_datatype.Global.loc g in
match g with
| GVarDecl (vi, l) as g ->
incr currentDeclIdx;
@@ -2920,7 +2920,7 @@ let oneFilePass2 (f: file) =
in
let newname, _ =
Alpha.newAlphaName ~alphaTable:sAlpha ~undolist:None
- ~lookupname:orig_name ~data:(Cil_const.CurrentLoc.get ())
+ ~lookupname:orig_name ~data:(Current_loc.get ())
in
ci.cname <- newname;
ci.creferenced <- true;
@@ -2949,7 +2949,7 @@ let oneFilePass2 (f: file) =
in
let newname, _ =
Alpha.newAlphaName ~alphaTable:eAlpha ~undolist:None
- ~lookupname:orig_name ~data:(Cil_const.CurrentLoc.get ())
+ ~lookupname:orig_name ~data:(Current_loc.get ())
in
ei.ename <- newname;
ei.ereferenced <- true;
@@ -3002,7 +3002,7 @@ let oneFilePass2 (f: file) =
None -> (* We must rename it and keep it *)
let newname, _ =
Alpha.newAlphaName ~alphaTable:vtAlpha ~undolist:None
- ~lookupname:ti.torig_name ~data:(Cil_const.CurrentLoc.get ())
+ ~lookupname:ti.torig_name ~data:(Current_loc.get ())
in
ti.tname <- newname;
ti.treferenced <- true;
@@ -3081,7 +3081,7 @@ let merge_specs orig to_merge =
List.iter merge_one_spec to_merge
let global_merge_spec g =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
Kernel.debug ~dkey:Kernel.dkey_linker
"Merging global %a" Cil_printer.pp_global g;
let rename v spec =
@@ -3090,7 +3090,7 @@ let global_merge_spec g =
ignore (visitCilFunspec alpha spec)
with Not_found -> ()
in
- let<> CurrentLocUpdated = Cil_datatype.Global.loc g in
+ let<> UpdatedCurrentLoc = Cil_datatype.Global.loc g in
match g with
| GFun(fdec, _) ->
Kernel.debug ~dkey:Kernel.dkey_linker
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index 2a6089b41dc51bdb0b6e35990ff689635e8d9ddb..190753ee6de26af4df7fc3fd4606223db5060b05 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -198,7 +198,7 @@ let encapsulate_local_vars f =
end
let oneret ?(callback: callback option) (f: fundec) : unit =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
let fname = f.svar.vname in
(* Get the return type *)
let retTyp =
@@ -342,7 +342,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
List.rev (s::acc)
| ({skind=Return (retval, loc)} as s) :: rests ->
- let<> CurrentLocUpdated = loc in
+ let<> UpdatedCurrentLoc = loc in
(*
ignore (E.log "Fixing return(%a) at %a\n"
insert
@@ -494,8 +494,8 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
{ b with bstmts = scanStmts [] mainbody 0 b.bstmts;}
in
- (*CEA since CurrentLoc isn't set
- ignore (visitCilBlock dummyVisitor f.sbody) ; *)(* sets CurrentLoc *)
+ (*CEA since Current_loc isn't set
+ ignore (visitCilBlock dummyVisitor f.sbody) ; *)(* sets Current_loc *)
(*CEA so, [scanBlock] will set [lastloc] when necessary
lastloc := !currentLoc ; *) (* last location in the function *)
f.sbody <- scanBlock true f.sbody ;
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 23db8aaa916c987a884d21c6869fc4fe46d3a6dd..87dffa91bc7a0a0061b6c6ac39eacb15b3e0da8f 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -178,7 +178,7 @@ let categorizePragmas ast =
| _ ->
Kernel.fatal ~current:true
"Bad alias attribute at %a"
- Cil_printer.pp_location (Cil_const.CurrentLoc.get ())
+ Cil_printer.pp_location (Current_loc.get ())
end
| _ ->
()
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 7b091cdb3ceed1dcd2bf1ce036bb2f18dc8a6e21..4bc1d09e3912cfc2307e68172b2237329b35579d 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -92,7 +92,7 @@ let fresh_label =
fun ?loc ?label_name () ->
decr counter;
let loc, orig = match loc with
- | None -> Cil_const.CurrentLoc.get (), false
+ | None -> Current_loc.get (), false
| Some loc -> loc, true
and new_label_name =
let prefix = match label_name with None -> "" | Some s -> s ^ "_"
@@ -380,13 +380,13 @@ let copy_block kf switch_label_action break_continue_must_change bl =
and copy_stmtkind
switch_label_action break_continue_must_change
labelled_stmt_tbl calls_tbl stkind =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
let copy_block
?(switch_label_action = switch_label_action)
?(break_continue_must_change = break_continue_must_change) =
copy_block ~switch_label_action ~break_continue_must_change
in
- let<> CurrentLocUpdated = Cil_datatype.Stmt.loc_skind stkind in
+ let<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc_skind stkind in
match stkind with
| (Instr _ | Return _ | Throw _) as keep ->
keep,labelled_stmt_tbl,calls_tbl
@@ -569,7 +569,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
ChangeDoChildrenPost (fundec, post_goto_updater)
method! vstmt_aux s =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
match s.skind with
| Goto _ ->
gotos <- s::gotos; (* gotos that may need to be updated *)
@@ -624,7 +624,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
goes into the remaining loop. *)
(* TODO: transforms loop annotations into statement contracts
inside the unrolled parts. *)
- let<> CurrentLocUpdated = loc in
+ let<> UpdatedCurrentLoc = loc in
let break_lbl_stmt =
let break_label = fresh_label () in
let break_lbl_stmt = mkEmptyStmt () in
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 41c57d606608608028519da69e52f92a96ca6be6..c659b68b9b4d0e6497ef6d66629babb28587b07b 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -58,7 +58,7 @@ module Id = State_builder.Counter (struct let name = "Origin.Id" end)
let current kind =
let id = Id.next () in
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
Origin { kind; loc; id; }
let well = Well
@@ -153,7 +153,7 @@ let clear () = Id.reset (); History.clear ()
let is_current = function
| Unknown | Well -> false
- | Origin { loc } -> Cil_datatype.Location.equal loc (Cil_const.CurrentLoc.get ())
+ | Origin { loc } -> Cil_datatype.Location.equal loc (Current_loc.get ())
(* Returns true if the origin has never been registered and is related to the
current location. *)
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 7694db9cc38384d76902286e362694bbb9577931..44f23b221892e0c605b5edfa640ab0d283fa2858 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -34,7 +34,7 @@ type kind =
| Arith (* Arithmetic operation on addresses *)
(** Creates an origin of the given kind, associated with the current source
- location extracted from [Cil_const.CurrentLoc]. *)
+ location extracted from [Current_loc]. *)
val current: kind -> t
(** Origin for garbled mix created in the initial state of the analysis
diff --git a/src/kernel_services/analysis/dataflow2.ml b/src/kernel_services/analysis/dataflow2.ml
index 30f3adc5485f13e9b1f48df1de282c57150a72a0..48b2d20a09bccdae01c9a3d0d0f6369194d41b1a 100644
--- a/src/kernel_services/analysis/dataflow2.ml
+++ b/src/kernel_services/analysis/dataflow2.ml
@@ -332,8 +332,8 @@ module Forwards(T : ForwardsTransfer) = struct
(** Process a statement *)
let processStmt worklist (s: stmt) : unit =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Cil_datatype.Stmt.loc s in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc s in
if T.debug then
Kernel.debug "FF(%s).stmt %d at %t@\n" T.name s.sid Cil.pp_thisloc;
@@ -359,9 +359,8 @@ module Forwards(T : ForwardsTransfer) = struct
match s.skind with
| Instr i ->
- let<> CurrentLocUpdated = Cil_datatype.Instr.loc i in
- let after = T.doInstr s i curr in
- do_succs after
+ Current_loc.with_loc (Cil_datatype.Instr.loc i)
+ do_succs (T.doInstr s i curr)
| UnspecifiedSequence _
| Goto _ | Break _ | Continue _
@@ -576,13 +575,13 @@ struct
(** Process a statement and return true if the set of live return
* addresses on its entry has changed. *)
let processStmt (s: stmt) : bool =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
if T.debug then
(Kernel.debug "FF(%s).stmt %d\n" T.name s.sid);
(* Find the state before the branch *)
- let<> CurrentLocUpdated = Cil_datatype.Stmt.loc s in
+ let<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc s in
let d: T.t =
match T.doStmt s with
Done d -> d
@@ -606,7 +605,7 @@ struct
match s.skind with
| Instr i ->
begin
- let<> CurrentLocUpdated = Cil_datatype.Instr.loc i in
+ let<> UpdatedCurrentLoc = Cil_datatype.Instr.loc i in
let action = T.doInstr s i res in
match action with
| Done s' -> s'
diff --git a/src/kernel_services/analysis/dataflow2.mli b/src/kernel_services/analysis/dataflow2.mli
index 010c906c55045f89e014b8aa54e4582fc393b168..f779ca10787bd575d6deed04d8654e6e2bc52ae0 100644
--- a/src/kernel_services/analysis/dataflow2.mli
+++ b/src/kernel_services/analysis/dataflow2.mli
@@ -119,7 +119,7 @@ module type ForwardsTransfer = sig
[stmt] is the corresponding [If] statement, passed as information only. *)
val doStmt: Cil_types.stmt -> t -> t stmtaction
- (** The (forwards) transfer function for a statement. The [(Cil_const.CurrentLoc.get
+ (** The (forwards) transfer function for a statement. The [(Current_loc.get
())] * is set before calling this. The default action is to do the
instructions * in this statement, if applicable, and continue with the
successors. *)
@@ -188,14 +188,14 @@ module type BackwardsTransfer = sig
(** Take the data from two successors and combine it *)
val doStmt: Cil_types.stmt -> t action
- (** The (backwards) transfer function for a branch. The [(Cil_const.CurrentLoc.get
+ (** The (backwards) transfer function for a branch. The [(Current_loc.get
())] is set before calling this. If it returns None, then we have some
default handling. Otherwise, the returned data is the data before the
branch (not considering the exception handlers) *)
val doInstr: Cil_types.stmt -> Cil_types.instr -> t -> t action
(** The (backwards) transfer function for an instruction. The
- [(Cil_const.CurrentLoc.get ())] is set before calling this. If it returns None,
+ [(Current_loc.get ())] is set before calling this. If it returns None,
then we have some default handling. Otherwise, the returned data is the
data before the branch (not considering the exception handlers) *)
diff --git a/src/kernel_services/analysis/dataflows.ml b/src/kernel_services/analysis/dataflows.ml
index 44484e0142e242002d5e36b3015cd870ab126f97..8f0dde149788ded2fd0598e40ecd1c358760b657 100644
--- a/src/kernel_services/analysis/dataflows.ml
+++ b/src/kernel_services/analysis/dataflows.ml
@@ -486,9 +486,7 @@ struct
W.insert ord) P.init;;
let update_before (stmt, new_state) =
- let open Cil_const.CurrentLoc.Operators in
let ord = Fenv.to_ordered stmt in
- let<> CurrentLocUpdated = Cil_datatype.Stmt.loc stmt in
let join =
(* If we know that we already have to recompute before.(ord), we
can omit the inclusion testing, and only perform the join. The
@@ -503,15 +501,16 @@ struct
if not is_included then W.insert ord;
join
in
- P.set_before ord join
+ Current_loc.with_loc (Cil_datatype.Stmt.loc stmt)
+ (P.set_before ord) join
;;
let do_stmt ord =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
let cur_state = P.get_before ord in
let stmt = Fenv.to_stmt ord in
Kernel.debug ~dkey:Kernel.dkey_dataflow "forward: doing stmt %d" stmt.sid;
- let<> CurrentLocUpdated = Cil_datatype.Stmt.loc stmt in
+ let<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc stmt in
let l = P.transfer_stmt stmt cur_state in
List.iter update_before l
;;
diff --git a/src/kernel_services/analysis/stmts_graph.ml b/src/kernel_services/analysis/stmts_graph.ml
index 14a22f00e8e072cd3331cb0bca79fc2253c24b0a..7efadadef7645597e36bd50887242fa8836ec8fe 100644
--- a/src/kernel_services/analysis/stmts_graph.ml
+++ b/src/kernel_services/analysis/stmts_graph.ml
@@ -267,8 +267,6 @@ let rec get_block_stmts blk =
List.fold_left add Stmt.Set.empty blk.bstmts
and get_stmt_stmts s =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Cil_datatype.Stmt.loc s in
let compute_stmt_stmts s = match s.skind with
| Instr _ | Return _ | Throw _ -> Stmt.Set.singleton s
| Continue _ | Break _ | Goto _ -> Stmt.Set.singleton s
@@ -288,7 +286,8 @@ and get_stmt_stmts s =
| TryExcept (_, _, _, _) | TryFinally (_, _, _) ->
Kernel.not_yet_implemented ~current:true "exception handling"
in
- StmtStmts.memo compute_stmt_stmts s
+ Current_loc.with_loc (Cil_datatype.Stmt.loc s)
+ (StmtStmts.memo compute_stmt_stmts) s
(* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index 6e2dc297939069c58c79cf05b7b8033d26f421f1..a00dfdb4662fc5738fd63fb21504f599f8e3b96d 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -241,7 +241,6 @@ module Functions = struct
update_orig_name kf; kf)
let update_kf kf fundec spec =
- let open Cil_const.CurrentLoc.Operators in
let oldloc = get_location kf in
(match kf.fundec, fundec with
(* we never update a definition with a declaration (see bug 1914).
@@ -255,8 +254,8 @@ module Functions = struct
let loc =
match fundec with Definition (_,loc) | Declaration (_,_,_,loc) -> loc
in
- let<> CurrentLocUpdated = loc in
- Logic_utils.merge_funspec ~oldloc kf.spec spec
+ Current_loc.with_loc loc
+ (Logic_utils.merge_funspec ~oldloc kf.spec) spec
let replace_by_declaration s v l=
(* Kernel.feedback "replacing %a by decl" Cil_datatype.Varinfo.pretty v;*)
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index adadf1c5e633f1a4c9e67c01db586c7bcbc1e891..b9de6911561698d1a951e2be6a7ae506f4002e59 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -351,11 +351,11 @@ and print_generic_association fmt (type_exp : (specifier * decl_type) option * e
and print_expression fmt (exp: expression) = print_expression_level 0 fmt exp
and print_expression_level (lvl: int) fmt (exp : expression) =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
let (txt, lvl') = get_operator exp in
let print_expression fmt exp = print_expression_level lvl' fmt exp in
let print_exp fmt e =
- let<> CurrentLocUpdated = e.expr_loc in
+ let<> UpdatedCurrentLoc = e.expr_loc in
match e.expr_node with
NOTHING -> ()
| PAREN exp -> print_expression fmt exp
@@ -425,9 +425,9 @@ and print_for_init fmt fc =
| FC_DECL dec -> print_def fmt dec
and print_statement fmt stat =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
let loc = Cabshelper.get_statementloc stat in
- let<> CurrentLocUpdated = loc in
+ let<> UpdatedCurrentLoc = loc in
if Kernel.debug_atleast 2 then
fprintf fmt "@\n/* %a */@\n" Cil_printer.pp_location loc;
match stat.stmt_node with
@@ -582,8 +582,8 @@ and print_defs fmt defs =
defs
and print_def fmt def =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Cabshelper.get_definitionloc def in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Cabshelper.get_definitionloc def in
match def with
FUNDEF (spec, proto, body, loc, _) ->
if !printCounters then begin
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 6f7f08daa4d78f1a75e6dde81e00583415368544..f34464221c5231c47d36174cca4b45c26d555df6 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -64,12 +64,12 @@ open Cil_types
functions below. *)
let check_invariants = false
-let () = Log.set_current_source (fun () -> fst (Cil_const.CurrentLoc.get ()))
+let () = Log.set_current_source (fun () -> fst (Current_loc.get ()))
-let pp_thisloc fmt = Location.pretty fmt (Cil_const.CurrentLoc.get ())
+let pp_thisloc fmt = Location.pretty fmt (Current_loc.get ())
let abort_context msg =
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let append fmt =
Format.pp_print_newline fmt ();
Errorloc.pp_context_from_file fmt loc
@@ -1421,9 +1421,8 @@ let copy_logic_label is_copy l =
end else l
let rec visitCilTerm vis t =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = t.term_loc in
- doVisitCil vis (fun x-> x) vis#vterm childrenTerm t
+ Current_loc.with_loc t.term_loc
+ (doVisitCil vis (fun x-> x) vis#vterm childrenTerm) t
and childrenTerm vis t =
let tn' = visitCilTermNode vis t.term_node in
@@ -2075,8 +2074,8 @@ and childrenModelInfo vis m =
else begin m.mi_attr <- mi_attr; m end
and visitCilModelInfo vis m =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = m.mi_decl in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = m.mi_decl in
let m' =
doVisitCil
vis (Visitor_behavior.Memo.model_info vis#behavior) vis#vmodel_info childrenModelInfo m
@@ -2089,9 +2088,8 @@ and visitCilModelInfo vis m =
m'
and visitCilAnnotation vis a =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Global_annotation.loc a in
- doVisitCil vis id vis#vannotation childrenAnnotation a
+ Current_loc.with_loc (Global_annotation.loc a)
+ (doVisitCil vis id vis#vannotation childrenAnnotation) a
and childrenAnnotation vis a =
match a with
@@ -2202,9 +2200,9 @@ and childrenCodeAnnot vis ca =
else ca
and visitCilExpr (vis: cilVisitor) (e: exp) : exp =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = e.eloc in
- doVisitCil vis (Visitor_behavior.cexpr vis#behavior) vis#vexpr childrenExp e
+ Current_loc.with_loc (e.eloc)
+ (doVisitCil vis (Visitor_behavior.cexpr vis#behavior) vis#vexpr childrenExp)
+ e
and childrenExp (vis: cilVisitor) (e: exp) : exp =
let vExp e = visitCilExpr vis e in
@@ -2335,9 +2333,8 @@ and childrenLocal_init vi (vis: cilVisitor) li =
if f' != f || args' != args then ConsInit(f',args',k) else li
and visitCilInstr (vis: cilVisitor) (i: instr) : instr list =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Cil_datatype.Instr.loc i in
- doVisitListCil vis id vis#vinst childrenInstr i
+ Current_loc.with_loc (Cil_datatype.Instr.loc i)
+ (doVisitListCil vis id vis#vinst childrenInstr) i
and childrenInstr (vis: cilVisitor) (i: instr) : instr =
let fExp = visitCilExpr vis in
@@ -2400,8 +2397,8 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr =
(* visit all nodes in a Cil statement tree in preorder *)
and visitCilStmt (vis:cilVisitor) (s: stmt) : stmt =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Cil_datatype.Stmt.loc s in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc s in
vis#push_stmt s; (*(vis#behavior.memo_stmt s);*)
assertEmptyQueue vis;
let toPrepend : instr list ref = ref [] in (* childrenStmt may add to this *)
@@ -2653,10 +2650,9 @@ and childrenType (vis : cilVisitor) (t : typ) : typ =
(* for declarations, we visit the types inside; but for uses, *)
(* we just visit the varinfo node *)
and visitCilVarDecl (vis : cilVisitor) (v : varinfo) : varinfo =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = v.vdecl in
- doVisitCil vis (Visitor_behavior.Memo.varinfo vis#behavior)
- vis#vvdec childrenVarDecl v
+ Current_loc.with_loc v.vdecl
+ (doVisitCil vis (Visitor_behavior.Memo.varinfo vis#behavior)
+ vis#vvdec childrenVarDecl) v
and childrenVarDecl (vis : cilVisitor) (v : varinfo) : varinfo =
(* in case of refresh visitor, the associated new logic var has a different
@@ -2859,9 +2855,8 @@ let visitCilEnumInfo vis e =
doVisitCil vis (Visitor_behavior.Memo.enuminfo vis#behavior) vis#venuminfo childrenEnumInfo e
let rec visitCilGlobal (vis: cilVisitor) (g: global) : global list =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Global.loc g in
- doVisitListCil vis id vis#vglob childrenGlobal g
+ Current_loc.with_loc (Global.loc g)
+ (doVisitListCil vis id vis#vglob childrenGlobal) g
and childrenGlobal (vis: cilVisitor) (g: global) : global =
match g with
| GFun (f, l) ->
@@ -4962,10 +4957,8 @@ let compareConstant c1 c2 =
(* Iterate over all globals, including the global initializer *)
let iterGlobals (fl: file) (doone: global -> unit) : unit =
- let open Cil_const.CurrentLoc.Operators in
let doone' g =
- let<> CurrentLocUpdated = Global.loc g in
- doone g
+ Current_loc.with_loc (Global.loc g) doone g
in
List.iter doone' fl.globals;
match fl.globinit with
@@ -4974,10 +4967,8 @@ let iterGlobals (fl: file) (doone: global -> unit) : unit =
(* Fold over all globals, including the global initializer *)
let foldGlobals (fl: file) (doone: 'a -> global -> 'a) (acc: 'a) : 'a =
- let open Cil_const.CurrentLoc.Operators in
let doone' acc g =
- let<> CurrentLocUpdated = Global.loc g in
- doone acc g
+ Current_loc.with_loc (Global.loc g) (doone acc) g
in
let acc' = List.fold_left doone' acc fl.globals in
match fl.globinit with
@@ -6840,7 +6831,7 @@ let foldLeftCompound
(* Some initializers are missing. Iterate over all the indexes in
the array, and use either the supplied initializer, or a generic
zero one. *)
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let zinit = makeZeroInit ~loc bt in
let acc = ref acc in
let initl = ref initl in
@@ -7042,7 +7033,7 @@ let uniqueVarNames (f: file) : unit =
Hashtbl.add globalNames vi.vname vi.vid;
(* And register it *)
Alpha.registerAlphaName ~alphaTable:gAlphaTable
- ~lookupname:vi.vname ~data:(Cil_const.CurrentLoc.get ())
+ ~lookupname:vi.vname ~data:(Current_loc.get ())
end)
| _ -> ());
@@ -7060,7 +7051,7 @@ let uniqueVarNames (f: file) : unit =
let lookupname =
if v.vorig_name = "" then v.vname else v.vorig_name
in
- let data = Cil_const.CurrentLoc.get () in
+ let data = Current_loc.get () in
let newname, oldloc =
Alpha.newAlphaName
~alphaTable:gAlphaTable ~undolist:(Some undolist)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index b438cd0d39993f1a24f0d97c78bc02877516a8b9..aed2f84c7513a397e2e64affce3de2af76c96ac6 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2280,7 +2280,7 @@ val constFoldVisitor: bool -> cilVisitor
(** {2 Debugging support} *)
(* ************************************************************************* *)
-(** Pretty-print [(Cil_const.CurrentLoc.get ())] *)
+(** Pretty-print [(Current_loc.get ())] *)
val pp_thisloc: Format.formatter -> unit
(** @return a dummy specification *)
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index 5620c04bbffb9585dd081a4bf21e170471921373..74176389529633084c020817c49adeda2c550253 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -43,30 +43,6 @@
open Cil_types
-module CurrentLoc = struct
- include
- State_builder.Ref
- (Cil_datatype.Location)
- (struct
- let dependencies = []
- let name = "CurrentLoc"
- let default () = Cil_datatype.Location.unknown
- end)
- module Operators = struct
- type operation = CurrentLocUpdated
-
- let from_option opt =
- Option.value ~default:(get ()) opt
-
- let ( let<> ) loc f =
- let oldLoc = get () in
- let finally () = set oldLoc in
- let work () = set loc; f CurrentLocUpdated in
- Fun.protect ~finally work
- end
-
-end
-
let voidType = TVoid([])
module Vid = State_builder.SharedCounter(struct let name = "vid_counter" end)
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index b13af1036f06b7271eb4b9d8d69ded04f643c36a..47f7659a34e8c63dfc10af4537b4a585c0974f09 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -46,42 +46,6 @@ open Cil_types
val voidType: typ
-(** A reference to the current location. If you are careful to set this to
- the current location then you can use some built-in logging functions that
- will print the location.
-*)
-module CurrentLoc: sig
- include State_builder.Ref with type data = location
- module Operators : sig
-
- (** [CurrentLocUpdated] is a simple constructor which can be used as
- documentation : [let<> CurrentLocUpdated = loc in ...] or replaced with
- [_]
- *)
- type operation = CurrentLocUpdated
-
- (** Utils function, [from_option opt] will return [l] if [opt] is [Some l]
- and [CurrentLoc.get ()] if it is [None].
- *)
- val from_option : data option -> data
-
- (**
- [let<> _ = loc in ...] can be used to mimic the behavior obtained with
- [
- let oldloc = CurrentLoc.get () in
- try
- CurrentLoc.set loc;
- let res = ... in
- CurrentLoc.set oldloc;
- res
- with exn -> CurrentLoc.set oldloc; raise exn
- ].
- [let<>] syntax requires to open [CurrentLoc.Operators].
- *)
- val ( let<> ) : data -> (operation -> 'a) -> 'a
- end
-end
-
module Vid: sig val next: unit -> int end
module Sid: sig val next: unit -> int end
module Eid: sig val next: unit -> int end
diff --git a/src/kernel_services/ast_queries/current_loc.ml b/src/kernel_services/ast_queries/current_loc.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9796cd10e6cb5d7942f7b5a3bc43a41c708e2edc
--- /dev/null
+++ b/src/kernel_services/ast_queries/current_loc.ml
@@ -0,0 +1,25 @@
+include State_builder.Ref
+ (Cil_datatype.Location)
+ (struct
+ let dependencies = []
+ let name = "CurrentLoc"
+ let default () = Cil_datatype.Location.unknown
+ end)
+
+let with_loc loc f x =
+ let oldLoc = get () in
+ let finally () = set oldLoc in
+ let work () = set loc; f x in
+ Fun.protect ~finally work
+
+let with_loc_opt loc_opt f x =
+ match loc_opt with
+ | None -> f x
+ | Some loc -> with_loc loc f x
+
+module Operators = struct
+ type operation = UpdatedCurrentLoc
+
+ let ( let<> ) loc f = with_loc loc f UpdatedCurrentLoc
+ let ( let<?> ) loc_opt f = with_loc_opt loc_opt f UpdatedCurrentLoc
+end
diff --git a/src/kernel_services/ast_queries/current_loc.mli b/src/kernel_services/ast_queries/current_loc.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c54e25bb39c5ad20df31ce8a7d743bb4ce522c3c
--- /dev/null
+++ b/src/kernel_services/ast_queries/current_loc.mli
@@ -0,0 +1,37 @@
+(** A reference to the current location. If you are careful to set this to
+ the current location then you can use some built-in logging functions that
+ will print the location.
+*)
+
+include State_builder.Ref with type data = Filepath.position * Filepath.position
+
+(** [with_loc loc f x] set the current location to [loc], which can be used
+ with [CurrentLoc.get ()] or via the option [~current] in Log functions.
+ The old location is saved and set back after exectution of [f x]. If [f x]
+ raises an exception, it is caught and re-raised after setting the location
+ to its old value.
+*)
+val with_loc : data -> ('a -> 'b) -> 'a -> 'b
+
+(** Same behavior than [with_loc] but takes an location option. The location is
+ set to [loc] for [Some loc] and unchanged otherwise.
+*)
+val with_loc_opt : data option -> ('a -> 'b) -> 'a -> 'b
+
+module Operators : sig
+
+ (** [UpdatedCurrentLoc] is a simple constructor which can be used as
+ documentation : [let<> UpdatedCurrentLoc = loc in ...] or replaced with
+ [_]
+ *)
+ type operation = UpdatedCurrentLoc
+
+ (** [let<> UpdatedCurrentLoc = loc in ...] can be used to mimic the behavior
+ obtained with [with_loc loc f UpdatedCurrentLoc].
+ [let<>] syntax requires to open the module [Operators].
+ *)
+ val ( let<> ) : data -> (operation -> 'a) -> 'a
+
+ (** Same behavior than [let<>] but for [with_loc_opt] *)
+ val ( let<?> ) : data option -> (operation -> 'a) -> 'a
+end
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index be5bbf3a38870f376d5fde4da4b12e4bda281d22..caeb0bacae4e856031d7b8dd39263080b1d41052 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -60,8 +60,6 @@ let preprocess_extension = Extensions.preprocess
let preprocess_extension_block = Extensions.preprocess_block
let extension_from = Extensions.extension_from
-module CurrentLoc = Cil_const.CurrentLoc
-
let error (b,_e) fstring =
Kernel.abort
~source:b
@@ -228,7 +226,7 @@ let add_logic_function_gen is_same_profile li =
let name = li.l_var_info.lv_name in
if is_builtin_logic_function name then
error
- (Cil_const.CurrentLoc.get())
+ (Current_loc.get())
"logic function or predicate %s is built-in. You cannot redefine it"
name;
match Logic_info.find name with
@@ -237,7 +235,7 @@ let add_logic_function_gen is_same_profile li =
(fun li' ->
if is_same_profile li li' then
error
- (Cil_const.CurrentLoc.get ())
+ (Current_loc.get ())
"already declared logic function or predicate %s \
with same profile"
name)
@@ -265,14 +263,14 @@ let find_logic_type = Logic_type_info.find
let add_logic_type t infos =
if is_logic_type t
(* type variables hide type definitions on their scope *)
- then error (Cil_const.CurrentLoc.get ()) "logic type %s already declared" t
+ then error (Current_loc.get ()) "logic type %s already declared" t
else Logic_type_info.add t infos
let is_logic_ctor = Logic_ctor_info.mem
let find_logic_ctor = Logic_ctor_info.find
let add_logic_ctor c infos =
if is_logic_ctor c
- then error (Cil_const.CurrentLoc.get ()) "logic constructor %s already declared" c
+ then error (Current_loc.get ()) "logic constructor %s already declared" c
else Logic_ctor_info.add c infos
let remove_logic_ctor = Logic_ctor_info.remove
@@ -308,7 +306,7 @@ let find_model_field s typ =
let add_model_field m =
try
ignore (find_model_field m.mi_name m.mi_base_type);
- error (Cil_const.CurrentLoc.get())
+ error (Current_loc.get())
"Cannot add model field %s to type %a: it already exists."
m.mi_name Cil_datatype.Typ.pretty m.mi_base_type
with Not_found -> Model_info.add m.mi_name m
@@ -375,7 +373,7 @@ let add_builtin_logic_function_gen is_same_profile bl =
List.iter
(fun bl' ->
if is_same_profile bl bl' then
- error (Cil_const.CurrentLoc.get ())
+ error (Current_loc.get ())
"already declared builtin logic function or predicate \
%s with same profile"
bl.bl_name)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 9ef42c4aab57c5bcd39b3af84bd557075a9390b6..d1b82ba5bca85aca012627060eab778e5c30e68c 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2604,7 +2604,7 @@ struct
(match lv.lv_type with
| Ctype (TVoid _)->
if ctxt.silent then raise Backtrack;
- ctxt.error (Cil_const.CurrentLoc.get())
+ ctxt.error (Current_loc.get())
"Variable %s is bound to a predicate, not a term" x
| _ -> old_val lv)
with Not_found ->
@@ -4099,9 +4099,9 @@ struct
| TDsyn typ -> LTsyn (plain_logic_type loc env typ)
let rec annot in_axiomatic a =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
let loc = a.decl_loc in
- let<> CurrentLocUpdated = loc in
+ let<> UpdatedCurrentLoc = loc in
match a.decl_node with
| LDlogic_reads (f, labels, poly, t, p, l) ->
let env,info = logic_decl loc f labels poly ~return_type:t p in
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 5a36ce4b6a8d54c8772a723c95650afdd2917141..cd74caa5993ca4a66e9c79f9fa9ec10fd9d103d1 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -96,14 +96,14 @@ let logicCType t =
in plain_or_set logicCType t
let plain_array_to_ptr ty =
- let open Cil_const.CurrentLoc.Operators in
+ let open Current_loc.Operators in
match unroll_type ty with
| Ctype(TArray(ty,lo,attr) as tarr) ->
let length_attr =
match lo with
| None -> []
| Some e ->
- let<> CurrentLocUpdated = e.eloc in
+ let<> UpdatedCurrentLoc = e.eloc in
try
let len = Cil.bitsSizeOf tarr in
let len = try len / (Cil.bitsSizeOf ty)
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index df3d68066899b5e3ff7ad96ae9f1300315d5c567..cb75d926227697bc365f178a554ab56431e8b255 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -432,9 +432,8 @@ end = struct
new_locals
method! vcode_annot v =
- let open Cil_const.CurrentLoc.Operators in
- let loc_opt = Cil_datatype.Code_annotation.loc v in
- let<> CurrentLocUpdated = from_option loc_opt in
+ let open Current_loc.Operators in
+ let<?> UpdatedCurrentLoc = Cil_datatype.Code_annotation.loc v in
let stmt =
Visitor_behavior.Get_orig.stmt
self#behavior (Option.get self#current_stmt)
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index c5d9b67bdae67e68b7da6cf7901f1e0c0bb86a2e..fa1565aa321a9f9916861cdb87cf920619d00533 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -47,7 +47,7 @@ type 'a pretty_printer =
Frama-C.
- When [current] is [false] (default for most of the channels),
no location is output. When it is [true], the last registered location
- is used as current (see {!Cil_const.CurrentLoc}).
+ is used as current (see {!Current_loc}).
- [source] is the location to be output. If nil, [current] is used to
determine if a location should be output
- [emitwith] function which is called each time an event is processed
diff --git a/src/kernel_services/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index de08ffaffe948c902f2b3f20c64370f21a3e95fa..357a69cd0979d5996008036ed5711af71f4b44da 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -82,16 +82,10 @@ end
class nopCabsVisitor : cabsVisitor = object
method vexpr (_e:expression) = DoChildren
method vinitexpr (_e:init_expression) = DoChildren
- method vstmt (s: statement) =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = get_statementloc s in
- DoChildren
+ method vstmt (_s: statement) = DoChildren
method vblock (_b: block) = DoChildren
method vvar (s: string) = s
- method vdef (d: definition) =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = get_definitionloc d in
- DoChildren
+ method vdef (_d: definition) = DoChildren
method vtypespec (_ts: typeSpecifier) = DoChildren
method vdecltype (_dt: decl_type) = DoChildren
method vname _k (_s:specifier) (_n: name) = DoChildren
@@ -235,7 +229,8 @@ and childrenSingleName vis (k: nameKind) (sn: single_name) : single_name =
if s' != s || n' != n then (s', n') else sn
and visitCabsDefinition vis (d: definition) : definition list =
- doVisitList vis vis#vdef childrenDefinition d
+ Current_loc.with_loc (get_definitionloc d)
+ (doVisitList vis vis#vdef childrenDefinition) d
and childrenDefinition vis d =
match d with
FUNDEF (spec,sn, b, l, lend) ->
@@ -280,7 +275,8 @@ and childrenBlock vis (b: block) : block =
else
b
and visitCabsStatement vis (s: statement) : statement list =
- doVisitList vis vis#vstmt childrenStatement s
+ Current_loc.with_loc (get_statementloc s)
+ (doVisitList vis vis#vstmt childrenStatement) s
and childrenStatement vis s =
let ve e = visitCabsExpression vis e in
let vs l s = match visitCabsStatement vis s with
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index 2e6c599f820346d4745ec6c3393e40a6ad14ad05..3214c3b5596c782eb65988eed90070d9015c7458 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -962,8 +962,8 @@ let filter_init_state restrict initial map acc =
with Not_found -> acc
let backward_analysis_aux stack kf ret_state =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Kernel_function.get_location kf in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Kernel_function.get_location kf in
if Data_for_aorai.isIgnoredFunction kf then
Aorai_option.fatal
"Call backward analysis on ignored function %a" Kernel_function.pretty kf
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 455c9d5724deb9dab6b0894dd68eae2606fec41e..73ffd560c652f480073875c191ca29376bd6748a 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -698,7 +698,7 @@ let add_gvar ?init vi =
set_varinfo vi.vname vi
let add_gvar_zeroinit vi =
- add_gvar ~init:(Cil.makeZeroInit ~loc:(Cil_const.CurrentLoc.get()) vi.vtype) vi
+ add_gvar ~init:(Cil.makeZeroInit ~loc:(Current_loc.get()) vi.vtype) vi
let mk_gvar ?init ~ty name =
(* See if the variable is already declared *)
@@ -720,7 +720,7 @@ let mk_gvar_scalar ~init ?(ty = Cil.typeOf init) name =
mk_gvar ~init:(SingleInit init) ~ty name
let mk_integer value =
- Cil.integer ~loc:(Cil_const.CurrentLoc.get()) value
+ Cil.integer ~loc:(Current_loc.get()) value
(* Utilities for global enumerations *)
let mk_global_c_enum_type_tagged name elements_l =
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 779d3b15749f1e61f3f42496fadfef51fae2a771..1064d178b6650c453f0fa10ca28e3d9152f84dfd 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -681,7 +681,7 @@ end
= struct
let process_quantif ~loc p =
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
match p.pred_content with
| Pforall(bound_vars, ({ pred_content = Pimplies(_, _) } as goal)) ->
compute_guards loc ~is_forall:true p bound_vars goal
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index ffff95dddfecbf946ab51280c5aecce68b1dc121..11cf5f2420a856a6f737b59f10d5a41aed664029 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -444,7 +444,7 @@ module rec Transfer
(* let l = Globals.Vars.fold_in_file_order (fun v i l -> (v, i) :: l) [] in
List.fold_left (fun state (v, i) -> do_one v i state) state l*)
- (** The (backwards) transfer function for a branch. The [(Cil_const.CurrentLoc.get
+ (** The (backwards) transfer function for a branch. The [(Current_loc.get
())] is set before calling this. If it returns None, then we have some
default handling. Otherwise, the returned data is the data before the
branch (not considering the exception handlers) *)
@@ -584,7 +584,7 @@ module rec Transfer
(** The (backwards) transfer function for an instruction. The
- [(Cil_const.CurrentLoc.get ())] is set before calling this. If it returns
+ [(Current_loc.get ())] is set before calling this. If it returns
None, then we have some default handling. Otherwise, the returned data is
the data before the branch (not considering the exception handlers) *)
let doInstr _stmt instr state =
@@ -734,7 +734,7 @@ let consolidated_must_monitor_vi vi =
let concurrent_function_ref = ref None
let abort_because_of_concurrent ~loc vi =
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
Options.abort
~current:true
"Found concurrent function %a and monitored memory properties.\n\
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 11c543584513b50589f6adf7c7bb1682cb4f0d1f..03099a4257c405daff073bae29cb0d2750186529 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -355,7 +355,7 @@ let rec type_term
mk_ctx ~use_gmp_opt:true (ty_of_interv i)
in
let infer t =
- Cil_const.CurrentLoc.set t.term_loc;
+ Current_loc.set t.term_loc;
(* this pattern matching implements the formal rules of the JFLA's paper
(and of course also covers the missing cases). Also enforce the invariant
that every subterm is typed, even if it is not an integer. *)
@@ -777,7 +777,7 @@ and type_predicate ~profile p =
do_both f g = (try f() with e -> try g(); raise e with | _ -> raise e); g()
in
let p = Logic_normalizer.get_pred p in
- Cil_const.CurrentLoc.set p.pred_loc;
+ Current_loc.set p.pred_loc;
(* this pattern matching also follows the formal rules of the JFLA's paper *)
match p.pred_content with
| Pfalse | Ptrue -> ()
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index c98db1aa6f22e880b5c3743c7d6927c3f4c14ee1..2a1ddf027d43aae44b508699f8cc324ca69dd36b 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -243,7 +243,7 @@ let setup_assumes kf env contract =
else
let assumes = assumes_predicate env b.b_assumes in
let loc = assumes.pred_loc in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
let idx = get_bhvr_idx contract b.b_name in
Rtl_call.set_assumes ~loc env kf contract_e idx assumes
with exn ->
@@ -321,7 +321,7 @@ let check_default_requires kf env contract =
(Property.ip_of_requires kf kinstr b ip_requires) then
let tp_requires = ip_requires.ip_content in
let loc = tp_requires.tp_statement.pred_loc in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
Translate_predicates.do_it kf env tp_requires
else
env)
@@ -355,7 +355,7 @@ let check_other_requires kf env contract =
| Assert | Check ->
let requires = tp_requires.tp_statement in
let loc = requires.pred_loc in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
(* Prepend the name of the behavior *)
let requires =
{ requires with pred_name = b.b_name :: requires.pred_name }
@@ -406,7 +406,7 @@ let check_other_requires kf env contract =
(* Generate a predicate that will retrieve and test the
already computed assumes value for the behavior *)
let loc = assumes.pred_loc in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
let assumes_vi, assumes_e, env =
get_or_create_assumes_var ~loc env
in
@@ -439,7 +439,7 @@ type translate_ppt =
let check_active_behaviors ~ppt_to_translate ~get_or_create_var kf env contract clauses =
let kinstr = Env.get_kinstr env in
let loc = contract.location in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
let do_clause env bhvrs =
let bhvrs_list = Datatype.String.Set.elements bhvrs in
let active = [] in (* TODO: 'for' behaviors, e-acsl#109 *)
@@ -612,7 +612,7 @@ let check_complete_and_disjoint kf env contract =
let env = check_bhvrs env Disjoint disjoints in
env
else begin
- Cil_const.CurrentLoc.set contract.location;
+ Current_loc.set contract.location;
Options.warning
~current:true
"@[Some assumes clauses could not be translated.@ Ignoring complete and \
@@ -645,7 +645,7 @@ let check_post_conds kf env contract =
(Property.ip_of_ensures kf kinstr b tp) then
let tp_post_cond = ip_post_cond.ip_content in
let loc = tp_post_cond.tp_statement.pred_loc in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
match termination with
| Normal ->
(* If translating the default behavior, directly translate the
@@ -674,7 +674,7 @@ let check_post_conds kf env contract =
| Assert | Check -> begin
let post_cond = tp_post_cond.tp_statement in
let loc = post_cond.pred_loc in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
match termination with
| Normal ->
(* Prepend the name of the behavior *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index c19bba9db6284681011910e9c13cd3495539edee..d573f59a1e77cca72c6a4ef38fb804fb7500641b 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -48,7 +48,7 @@ let pre_funspec kf env funspec =
env
in
let loc = Kernel_function.get_location kf in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
let env = convert_unsupported_clauses env in
let contract = Contract.create ~loc funspec in
Env.with_params
diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
index a638d2d3dc93d781458c6ccc36d14c059b1f86ea..a1fe17a9c9f8d6ed658fcfb018a7419b815b4186 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -73,7 +73,7 @@ let relation_to_binop = function
let rec predicate_content_to_exp ~adata ?(inplace=false) ?name kf env p =
let loc = p.pred_loc in
let logic_env = Env.Logic_env.get env in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
match p.pred_content with
| Pfalse -> Cil.zero ~loc, adata, env
| Ptrue -> Cil.one ~loc, adata, env
diff --git a/src/plugins/eva/alarmset.ml b/src/plugins/eva/alarmset.ml
index 1c0c437560145558a66bdd2b9e70c5f32db09e6f..426b1850d42a3e8517e1318c23c324c47da1b2d2 100644
--- a/src/plugins/eva/alarmset.ml
+++ b/src/plugins/eva/alarmset.ml
@@ -266,7 +266,7 @@ let loc = function
| Cil_types.Kglobal -> (* can occur in case of obscure bugs (already happened)
with wacky initializers. Module Initial_state of
value analysis correctly positions the loc *)
- Cil_const.CurrentLoc.get ()
+ Current_loc.get ()
| Cil_types.Kstmt s -> Cil_datatype.Stmt.loc s
let report_alarm ki annot msg =
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index bbbf2f4a33a8e1ecae1b7dc4fa5777bbe3f542db..8e68e2198b4c4e8e7467b127b80c648bf42d1a83 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -234,7 +234,7 @@ let type_from_nb_elems tsize =
if Int.equal Int.one nb
then typ
else
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let esize_arr = Cil.kinteger64 ~loc nb in (* [nb] fits in size_t *)
TArray (typ, Some esize_arr, [])
diff --git a/src/plugins/eva/domains/cvalue/cvalue_init.ml b/src/plugins/eva/domains/cvalue/cvalue_init.ml
index f247da4541edd0198b4dab0efcff7e5cc79454f5..084207175c47eb387a7bf5f9bf7020b487e4383e 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_init.ml
@@ -111,7 +111,7 @@ let reject_empty_struct b offset typ =
(** [initialize_var_using_type varinfo state] uses the type of [varinfo]
to create an initial value in [state]. *)
let initialize_var_using_type varinfo state =
- Cil_const.CurrentLoc.set varinfo.vdecl;
+ Current_loc.set varinfo.vdecl;
let rec add_offsetmap depth b name_desc name typ offset_orig typ_orig state =
let typ = Cil.unrollType typ in
let loc = lazy (loc_of_typoffset b typ_orig offset_orig) in
diff --git a/src/plugins/eva/engine/initialization.ml b/src/plugins/eva/engine/initialization.ml
index 1781b9ae54cfd2aee24ce197e0f56888b8d0608f..ab92b750abfc54e237b933696e174df6fa7a73a0 100644
--- a/src/plugins/eva/engine/initialization.ml
+++ b/src/plugins/eva/engine/initialization.ml
@@ -309,7 +309,7 @@ module Make
with Initialization_failed -> `Bottom
let initialize_global_variable ~lib_entry vi init state =
- Cil_const.CurrentLoc.set vi.vdecl;
+ Current_loc.set vi.vdecl;
let state = Domain.enter_scope Abstract_domain.Global [vi] state in
let state = if vi.vsource then
let initialize =
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 1cb544ed57f277c2eb7f07680bb343d6b3bef024..6629af3bd03dec32a60e02d233fe3829a086f138 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/src/plugins/eva/engine/iterator.ml
@@ -441,7 +441,7 @@ module Make_Dataflow
Async.yield ();
check_signals ();
current_ki := kinstr;
- Cil_const.CurrentLoc.set e.edge_loc;
+ Current_loc.set e.edge_loc;
let flow = Partitioning.transfer (transfer_transition transition) flow in
let flow = process_partitioning_transitions v1 v2 transition flow in
if not (Partitioning.is_empty_flow flow) then
@@ -466,7 +466,7 @@ module Make_Dataflow
(* Set location *)
current_ki := Kstmt stmt;
let current_loc = Cil_datatype.Stmt.loc stmt in
- Cil_const.CurrentLoc.set current_loc
+ Current_loc.set current_loc
| None -> ()
end;
(* Get vertex store *)
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 3251816fc30ab265e638097a017c9e0a916ea693..2579ca24f8ae0dd9644b455e45ec8a18232cdb4b 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -311,7 +311,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let cleanup () =
Eva_utils.pop_call_stack ();
(* Changed by compute_call_ref, called from process_call *)
- Cil_const.CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
+ Current_loc.set (Cil_datatype.Stmt.loc stmt);
in
let process () =
let domain_valuation = Eval.to_domain_valuation valuation in
@@ -686,7 +686,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let file = Format.sprintf "%s_%d" name n in
let ch = open_out file in
let fmt = Format.formatter_of_out_channel ch in
- let l = fst (Cil_const.CurrentLoc.get ()) in
+ let l = fst (Current_loc.get ()) in
Self.feedback ~current:true "Dumping state in file '%s'%t"
file Eva_utils.pp_callstack;
Format.fprintf fmt "DUMPING STATE at file %a line %d@."
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index 390d92e9ec3efaeb189855c6ba5dfba883f9529a..37ec8affc0c29d1e43717ada741b316f796b50a5 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -612,7 +612,7 @@ module Make (X: Analysis.S) = struct
In this case, nothing is displayed by the GUI. *)
| `Bottom -> [], [] (* Bottom case: nothing is displayed either. *)
| `Value before ->
- Cil_const.CurrentLoc.set (gui_loc_loc loc);
+ Current_loc.set (gui_loc_loc loc);
clear_caches ();
make_data_all_callstacks_from_states ev ~before ~after:states_after v
end
diff --git a/src/plugins/eva/legacy/eval_annots.ml b/src/plugins/eva/legacy/eval_annots.ml
index 641b53e225963cfbed5d753bbc32a180b05dca4f..bb5de81d88d7abd1cce065869a7c21407075ea29 100644
--- a/src/plugins/eva/legacy/eval_annots.ml
+++ b/src/plugins/eva/legacy/eval_annots.ml
@@ -164,14 +164,14 @@ end
let contains_c_at ca =
let vis = new contains_c_at in
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let r =
try
ignore (Visitor.visitFramacCodeAnnotation vis ca);
false
with Exit -> true
in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
r
(* Re-evaluate all alarms, and see if we can put a 'green' or 'red' status,
@@ -187,7 +187,7 @@ let mark_green_and_red () =
| AAssert (_, p) | AInvariant (_, true, p) ->
let p = p.tp_statement in
let loc = code_annotation_loc ca stmt in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
let kf = Kernel_function.find_englobing_kf stmt in
let ip = Property.ip_of_code_annot_single kf stmt ca in
(* This status is exact: we are _not_ refining the statuses previously
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index c0b060785599ad02184ea29bac779822ac1ad837..456ad09c557c483fe70e79de050673b9c2918281 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -169,7 +169,7 @@ class postconditions_mention_result = object
end
let postconditions_mention_result spec =
(* We save the current location because the visitor modifies it. *)
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let vis = new postconditions_mention_result in
let aux_bhv bhv =
let aux (_, post) = ignore (Visitor.visitFramacIdPredicate vis post) in
@@ -181,7 +181,7 @@ let postconditions_mention_result spec =
false
with Exit -> true
in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
res
let conv_comp op =
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index f96ca40c87e7dab7a8ad7152a5f348717b704607..32bde5c8b84894d1e2610bb4f3f26fe376f6cb04 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -200,14 +200,14 @@ struct
is redundant with the work done by Value -- hence the use of [\nothing].*)
let bind_locals m b =
let aux_local acc vi =
- Cil_const.CurrentLoc.set vi.vdecl;
+ Current_loc.set vi.vdecl;
(* Consider that local are initialized to a constant value *)
From_memory.bind_var vi Eva.Deps.bottom acc
in
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let r = List.fold_left aux_local m b.blocals in
- Cil_const.CurrentLoc.set loc;
+ Current_loc.set loc;
r
let unbind_locals m b =
@@ -631,7 +631,7 @@ struct
compute_using_prototype_for_state state kf assigns
let compute_and_return kf =
- let call_site_loc = Cil_const.CurrentLoc.get () in
+ let call_site_loc = Current_loc.get () in
From_parameters.feedback
"Computing for function %a%s"
Kernel_function.pretty kf
@@ -651,7 +651,7 @@ struct
From_parameters.feedback
"Done for function %a" Kernel_function.pretty kf;
Async.yield ();
- Cil_const.CurrentLoc.set call_site_loc;
+ Current_loc.set call_site_loc;
result
let compute kf =
diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml
index b87e02c581e8824dea93da98bdb9f27d49341b5e..48b2f08ee23fae975c0d7e64b8e6ccc9d066a0fe 100644
--- a/src/plugins/instantiate/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -55,7 +55,7 @@ class transformer = object(self)
method! vfile _ =
let post f =
- f.globals <- (Global_context.globals (Cil_const.CurrentLoc.get())) @ f.globals ;
+ f.globals <- (Global_context.globals (Current_loc.get())) @ f.globals ;
Ast.mark_as_changed () ;
Ast.mark_as_grown () ;
f
@@ -64,7 +64,7 @@ class transformer = object(self)
method! vglob_aux _ =
let post g =
- let loc = Cil_const.CurrentLoc.get() in
+ let loc = Current_loc.get() in
let folding l fd =
if VISet.mem fd.svar !introduced_instantiators then l
else begin
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index b80327338f365a7ba553d53a8311de6399ae6c43..b6d09702f5186bdd3ad6945ca2a44a9b15b9bab7 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -361,7 +361,7 @@ module Store(* (B:sig *)
end
let mu (f:(t -> t)) (value,conds,stmt) =
- Cil_const.CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
+ Current_loc.set (Cil_datatype.Stmt.loc stmt);
let (result,final_conds,_) = f (init stmt) in
(* Induction variables is a map from each Varinfo to its increment. *)
diff --git a/src/plugins/metrics/metrics_coverage.ml b/src/plugins/metrics/metrics_coverage.ml
index cd02401cb8eeff83e238844199de98d95ac27595..d74cf7809b8e40b0697ce7de52c4cf87add4e061 100644
--- a/src/plugins/metrics/metrics_coverage.ml
+++ b/src/plugins/metrics/metrics_coverage.ml
@@ -156,7 +156,7 @@ class deadCallsVisitor fmt ~libc cov_metrics =
Format.fprintf fmt
"@[<h>%s referenced by an ACSL specification (at %a)@]@ "
vi.vname
- Location.pretty (Cil_const.CurrentLoc.get ())
+ Location.pretty (Current_loc.get ())
| Some vinit ->
Format.fprintf fmt
"@[<h>Initializer of %s references %s (at %t)@]@ "
@@ -177,7 +177,7 @@ class deadCallsVisitor fmt ~libc cov_metrics =
Format.fprintf fmt
"@[<h>Function %a %s %s (at %a)@]@ "
Kernel_function.pretty f mess vi.vname
- Location.pretty (Cil_const.CurrentLoc.get ())
+ Location.pretty (Current_loc.get ())
method! vvrbl vi =
if Cil.isFunctionType vi.vtype then self#reached_fun vi;
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index e1b8e39f3f764dcf8b2cb91b943d61868e69cb6f..62f57e9b0f6e803af70465abfec31c0730329b4e 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -304,7 +304,7 @@ class full_visitor = object(self)
inherit Cil.nopCilVisitor
val mutable cur_func = None
method add ?func ?node ?names domain =
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let func = if func <> None && func <> Some "" then func else cur_func in
add_entry ?func ?node ?names loc domain
method add_code ?func ?names node =
@@ -411,7 +411,7 @@ class code_annot_visitor = object(self)
inherit Cil.nopCilVisitor
method add_annot ?(names=[]) node =
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let func = !ca_visitor_cur_func in
let plugin = !ca_visitor_cur_emitter in
let domain = Syntax Annotation in
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 7bc8b0b99a42d19e49dc0031b4225c2cc5aa46de..4c0f87877560305e994cc46260d9e84f18911022 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -129,7 +129,7 @@ let compute kf =
R.debug ~level:1 "computing for function %a" Kernel_function.pretty kf;
let f = Kernel_function.get_definition kf in
let do_stmt lmap s =
- Cil_const.CurrentLoc.set (Cil_datatype.Stmt.loc s);
+ Current_loc.set (Cil_datatype.Stmt.loc s);
if Eva.Results.is_reachable s
then register_modified_zones lmap s
else lmap
diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index b915951538a16f609f154fcda14b5f392a06e752..df85da95bfd739a9db2ed4c29d477d83b9c43898 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -412,9 +412,9 @@ struct
(* --- BootStrapping --- *)
(* -------------------------------------------------------------------------- *)
- let exp env e = Context.with_current_loc e.eloc (exp_protected env) e
- let cond env e = Context.with_current_loc e.eloc (cond_node env) e
- let call env e = Context.with_current_loc e.eloc (call_node env) e
+ let exp env e = Current_loc.with_loc e.eloc (exp_protected env) e
+ let cond env e = Current_loc.with_loc e.eloc (cond_node env) e
+ let call env e = Current_loc.with_loc e.eloc (call_node env) e
let result env tr = function
| R_var x -> F.e_var x
| R_loc l -> cval (M.load env (Ctypes.object_of tr) l)
diff --git a/src/plugins/wp/Context.ml b/src/plugins/wp/Context.ml
index 2259bab622de04625ddff6665de4866a66dd8cd3..7125d3e988e48332bbd990bdb07ed58f14bb5223 100644
--- a/src/plugins/wp/Context.ml
+++ b/src/plugins/wp/Context.ml
@@ -20,15 +20,6 @@
(* *)
(**************************************************************************)
-(* -------------------------------------------------------------------------- *)
-(* --- Location --- *)
-(* -------------------------------------------------------------------------- *)
-
-let with_current_loc loc phi x =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = loc in
- phi x
-
(* -------------------------------------------------------------------------- *)
(* --- Local Context --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Context.mli b/src/plugins/wp/Context.mli
index 28917aeb740de9ecb03fdb3c9f278d19c94ad42d..73d3baa335a6eed325939e67b217d0f115a3866f 100644
--- a/src/plugins/wp/Context.mli
+++ b/src/plugins/wp/Context.mli
@@ -20,10 +20,6 @@
(* *)
(**************************************************************************)
-(** Current Loc *)
-
-val with_current_loc : Cil_types.location -> ('a -> 'b) -> 'a -> 'b
-
(** Contextual Values *)
type 'a value
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index cad0d5b3b9382e7bfaac02125ea1c4c4f06aefb9..e1ae3720d5110f20b5fae379864311994aad9221 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -998,13 +998,13 @@ struct
p
let pred polarity env p =
- Context.with_current_loc p.pred_loc (pred_trigger polarity env) p
+ Current_loc.with_loc p.pred_loc (pred_trigger polarity env) p
let logic env t =
- Context.with_current_loc t.term_loc (term_trigger env) t
+ Current_loc.with_loc t.term_loc (term_trigger env) t
let region env t =
- Context.with_current_loc t.term_loc (assignable env) t
+ Current_loc.with_loc t.term_loc (assignable env) t
let () = C.bootstrap_pred pred
let () = C.bootstrap_term term
diff --git a/src/plugins/wp/Warning.ml b/src/plugins/wp/Warning.ml
index 8bc11d14545d00167c5530840aba3088e886dea5..47b66a0fd02cacd110e443e6d3d593f3e4dd7367 100644
--- a/src/plugins/wp/Warning.ml
+++ b/src/plugins/wp/Warning.ml
@@ -122,7 +122,7 @@ let kprintf phi ?(log=true) ?(severe=false) ?source ~effect message =
(fun fmt ->
Format.pp_print_flush fmt () ;
let text = Buffer.contents buffer in
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
if log then
Wp_parameters.warning ~source:(fst loc) "%s" text ~once:true ;
phi {
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 693f5220ecdcac2dc8ecb90b17c954901edbbc6d..798c3ab58876636f1236e8f28679ebf014091023 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -204,7 +204,7 @@ struct
let rec wp (env:env) (a:vertex) : W.t_prop =
match Vhash.find env.wp a with
- | None -> raise (NonNaturalLoop (Cil_const.CurrentLoc.get()));
+ | None -> raise (NonNaturalLoop (Current_loc.get()));
| Some pi -> pi
| exception Not_found ->
(* cut circularities *)
@@ -216,8 +216,8 @@ struct
(* Compute a stmt node *)
and stmt env a (s: stmt) : W.t_prop =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Stmt.loc s in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Stmt.loc s in
let smoking = is_default_bhv env.mode && env.dead s in
let cas = CfgAnnot.get_code_assertions ~smoking env.mode.kf s in
let opt_fold f = Option.fold ~none:Fun.id ~some:f in
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index c8f382f35fc7a26c77d7c562de755038906cf189..9c922d48a981cdb2933f826d7729d1968a04f039 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -423,8 +423,8 @@ let loop_contract_pids kf stmt =
| _ -> []
let compile Key.{ kf ; smoking ; bhv ; prop } =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = Kernel_function.get_location kf in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Kernel_function.get_location kf in
let body, checkpath, reachability =
if Kernel_function.has_definition kf then
let cfg = Cfg.get_automaton kf in
diff --git a/src/plugins/wp/cfgInit.ml b/src/plugins/wp/cfgInit.ml
index d27c05a33281725356cc3654019a0c0ce1c7aa87..69fcd7338a1561b35afe325f5ae04dc9b7d74687 100644
--- a/src/plugins/wp/cfgInit.ml
+++ b/src/plugins/wp/cfgInit.ml
@@ -34,10 +34,9 @@ struct
| `All -> true
| `InitConst -> Cil.isGlobalInitConst var
in if not do_init then obj
- else let old_loc = Cil_const.CurrentLoc.get () in
- Cil_const.CurrentLoc.set var.vdecl ;
- let obj = W.init wenv var initinfo.init obj in
- Cil_const.CurrentLoc.set old_loc ; obj
+ else
+ Current_loc.with_loc var.vdecl
+ (W.init wenv var initinfo.init) obj
) obj
let process_global_const wenv obj =
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index f69fa373646ecb3c1a221576bb9eb7df4c88e2c9..1a9cdb55c93ad75e184f55c754b96cf284e48e2f 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -236,8 +236,8 @@ let f_name = f_memo (Pretty_utils.to_string pp_float)
let char c = Integer.to_int64_exn (Cil.charConstToInt c)
let constant e =
- let open Cil_const.CurrentLoc.Operators in
- let<> CurrentLocUpdated = e.eloc in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = e.eloc in
match (Cil.constFold true e).enode with
| Const(CInt64(k,_,_)) ->
begin
diff --git a/tests/cil/change_to_instr.ml b/tests/cil/change_to_instr.ml
index 5e5feec4db005ba1ce2fbe7ae4f1c6ce7991d851..05654da724120b715419038bb077344a6669554b 100644
--- a/tests/cil/change_to_instr.ml
+++ b/tests/cil/change_to_instr.ml
@@ -7,7 +7,7 @@ class add_skip = object(_)
method! vinst i =
let open Cil_types in
- Cil.ChangeTo [ Skip(Cil_const.CurrentLoc.get()) ; i ]
+ Cil.ChangeTo [ Skip(Current_loc.get()) ; i ]
end
let run () =
diff --git a/tests/cil/queue_ghost_instr.ml b/tests/cil/queue_ghost_instr.ml
index fe07856fe8cd9da743d158668310f457cadd2494..6af2f351546c24d93b84cce519c133c80e456347 100644
--- a/tests/cil/queue_ghost_instr.ml
+++ b/tests/cil/queue_ghost_instr.ml
@@ -9,14 +9,14 @@ class add_skip = object(this)
let open Cil_types in
begin match s.skind with
| If(_) ->
- this#queueInstr([Skip(Cil_const.CurrentLoc.get())])
+ this#queueInstr([Skip(Current_loc.get())])
| _ -> ()
end ;
Cil.DoChildren
method! vinst _ =
let open Cil_types in
- this#queueInstr([Skip(Cil_const.CurrentLoc.get())]) ;
+ this#queueInstr([Skip(Current_loc.get())]) ;
Cil.DoChildren
end
diff --git a/tests/misc/my_visitor.ml b/tests/misc/my_visitor.ml
index 9100b04510d8feefab788784d4c011fb4026402f..b3cdee5f5e3b4c4a9e74282d1fc3197e6e5d3979 100644
--- a/tests/misc/my_visitor.ml
+++ b/tests/misc/my_visitor.ml
@@ -54,7 +54,7 @@ class foo = object (self)
inherit Visitor.frama_c_inplace
method! vstmt_aux stmt =
- let loc = Cil_const.CurrentLoc.get () in
+ let loc = Current_loc.get () in
add_assert loc (Option.get self#current_kf) stmt;
DoChildren
diff --git a/tests/syntax/ghost_cv_var_decl.ml b/tests/syntax/ghost_cv_var_decl.ml
index cba08161892c133911c3bc4eec6211d18afde777..d9c6c4dfae38297193968bee5a669a3139bcb209 100644
--- a/tests/syntax/ghost_cv_var_decl.ml
+++ b/tests/syntax/ghost_cv_var_decl.ml
@@ -14,12 +14,12 @@ let rec ghost_status fmt lval =
Format.fprintf fmt " -> %a" comp_ghost_status lval
| _ -> ()
and pointed_ghost_status fmt lval =
- let loc = Cil_const.CurrentLoc.get() in
+ let loc = Current_loc.get() in
let exp = Cil.new_exp (Lval lval) ~loc in
let lval = Mem(exp), NoOffset in
Format.fprintf fmt "%a" ghost_status lval
and in_array_ghost_status fmt lval =
- let loc = Cil_const.CurrentLoc.get() in
+ let loc = Current_loc.get() in
let lval = Cil.addOffsetLval (Index((Cil.zero ~loc), NoOffset)) lval in
Format.fprintf fmt "%a" ghost_status lval
and comp_ghost_status fmt lval =
@@ -38,7 +38,7 @@ class visitor = object(_)
method! vvdec v =
Kernel.feedback "%a@. %a: %a"
- Cil_datatype.Location.pretty (Cil_const.CurrentLoc.get())
+ Cil_datatype.Location.pretty (Current_loc.get())
Cil_datatype.Varinfo.pretty v
ghost_status (Cil.var v) ;
Cil.DoChildren