From c7ac3907ad274f85a27fbec4824d8cf08a082d9f Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 7 Feb 2024 16:28:49 +0100
Subject: [PATCH] CurrentLoc at toplevel, define with_loc(_opt) and let<?>
---
src/kernel_internals/typing/alpha.mli | 2 +-
src/kernel_internals/typing/cabs2cil.ml | 126 +++++++++---------
src/kernel_internals/typing/cfg.ml | 4 +-
src/kernel_internals/typing/ghost_accesses.ml | 2 +-
src/kernel_internals/typing/mergecil.ml | 30 ++---
src/kernel_internals/typing/oneret.ml | 8 +-
src/kernel_internals/typing/rmtmps.ml | 2 +-
src/kernel_internals/typing/unroll_loops.ml | 10 +-
src/kernel_services/abstract_interp/origin.ml | 4 +-
.../abstract_interp/origin.mli | 2 +-
src/kernel_services/analysis/dataflow2.ml | 15 +--
src/kernel_services/analysis/dataflow2.mli | 6 +-
src/kernel_services/analysis/dataflows.ml | 9 +-
src/kernel_services/analysis/stmts_graph.ml | 5 +-
src/kernel_services/ast_data/globals.ml | 5 +-
src/kernel_services/ast_printing/cprint.ml | 12 +-
src/kernel_services/ast_queries/cil.ml | 61 ++++-----
src/kernel_services/ast_queries/cil.mli | 2 +-
src/kernel_services/ast_queries/cil_const.ml | 24 ----
src/kernel_services/ast_queries/cil_const.mli | 36 -----
.../ast_queries/current_loc.ml | 25 ++++
.../ast_queries/current_loc.mli | 37 +++++
src/kernel_services/ast_queries/logic_env.ml | 14 +-
.../ast_queries/logic_typing.ml | 6 +-
.../ast_queries/logic_utils.ml | 4 +-
.../ast_transformations/filter.ml | 5 +-
.../plugin_entry_points/log.mli | 2 +-
src/kernel_services/visitors/cabsvisit.ml | 16 +--
src/plugins/aorai/aorai_dataflow.ml | 4 +-
src/plugins/aorai/aorai_utils.ml | 4 +-
.../e-acsl/src/analyses/bound_variables.ml | 2 +-
.../e-acsl/src/analyses/memory_tracking.ml | 6 +-
src/plugins/e-acsl/src/analyses/typing.ml | 4 +-
.../e-acsl/src/code_generator/contract.ml | 16 +--
.../src/code_generator/translate_annots.ml | 2 +-
.../code_generator/translate_predicates.ml | 2 +-
src/plugins/eva/alarmset.ml | 2 +-
.../eva/domains/cvalue/builtins_malloc.ml | 2 +-
src/plugins/eva/domains/cvalue/cvalue_init.ml | 2 +-
src/plugins/eva/engine/initialization.ml | 2 +-
src/plugins/eva/engine/iterator.ml | 4 +-
src/plugins/eva/engine/transfer_stmt.ml | 4 +-
src/plugins/eva/gui/gui_eval.ml | 2 +-
src/plugins/eva/legacy/eval_annots.ml | 6 +-
src/plugins/eva/utils/eva_utils.ml | 4 +-
src/plugins/from/from_compute.ml | 10 +-
src/plugins/instantiate/transform.ml | 4 +-
src/plugins/loop_analysis/loop_analysis.ml | 2 +-
src/plugins/metrics/metrics_coverage.ml | 4 +-
src/plugins/metrics/metrics_pivot.ml | 4 +-
src/plugins/scope/datascope.ml | 2 +-
src/plugins/wp/CodeSemantics.ml | 6 +-
src/plugins/wp/Context.ml | 9 --
src/plugins/wp/Context.mli | 4 -
src/plugins/wp/LogicSemantics.ml | 6 +-
src/plugins/wp/Warning.ml | 2 +-
src/plugins/wp/cfgCalculus.ml | 6 +-
src/plugins/wp/cfgInfos.ml | 4 +-
src/plugins/wp/cfgInit.ml | 7 +-
src/plugins/wp/ctypes.ml | 4 +-
tests/cil/change_to_instr.ml | 2 +-
tests/cil/queue_ghost_instr.ml | 4 +-
tests/misc/my_visitor.ml | 2 +-
tests/syntax/ghost_cv_var_decl.ml | 6 +-
64 files changed, 298 insertions(+), 332 deletions(-)
create mode 100644 src/kernel_services/ast_queries/current_loc.ml
create mode 100644 src/kernel_services/ast_queries/current_loc.mli
diff --git a/src/kernel_internals/typing/alpha.mli b/src/kernel_internals/typing/alpha.mli
index 607288dbdd3..075d2f04f5e 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 0484105bdd6..f88ac0ff29e 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 59666e7574f..7da177464c0 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 15ec967abf8..5394ebbc58f 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 0f950a6eb62..cca4dd7a60f 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 2a6089b41dc..190753ee6de 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 23db8aaa916..87dffa91bc7 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 7b091cdb3ce..4bc1d09e391 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 41c57d60660..c659b68b9b4 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 7694db9cc38..44f23b22189 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 30f3adc5485..48b2d20a09b 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 010c906c550..f779ca10787 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 44484e0142e..8f0dde14978 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 14a22f00e8e..7efadadef76 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 6e2dc297939..a00dfdb4662 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 adadf1c5e63..b9de6911561 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 6f7f08daa4d..f34464221c5 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 b438cd0d399..aed2f84c751 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 5620c04bbff..74176389529 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 b13af1036f0..47f7659a34e 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 00000000000..9796cd10e6c
--- /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 00000000000..c54e25bb39c
--- /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 be5bbf3a388..caeb0bacae4 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 9ef42c4aab5..d1b82ba5bca 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 5a36ce4b6a8..cd74caa5993 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 df3d6806689..cb75d926227 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 c5d9b67bdae..fa1565aa321 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 de08ffaffe9..357a69cd097 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 2e6c599f820..3214c3b5596 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 455c9d5724d..73ffd560c65 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 779d3b15749..1064d178b66 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 ffff95dddfe..11cf5f2420a 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 11c54358451..03099a4257c 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 c98db1aa6f2..2a1ddf027d4 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 c19bba9db62..d573f59a1e7 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 a638d2d3dc9..a1fe17a9c9f 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 1c0c4375601..426b1850d42 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 bbbf2f4a33a..8e68e2198b4 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 f247da4541e..084207175c4 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 1781b9ae54c..ab92b750abf 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 1cb544ed57f..6629af3bd03 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 3251816fc30..2579ca24f8a 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 390d92e9ec3..37ec8affc0c 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 641b53e2259..bb5de81d88d 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 c0b06078559..456ad09c557 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 f96ca40c87e..32bde5c8b84 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 b87e02c581e..48b2f08ee23 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 b80327338f3..b6d09702f51 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 cd02401cb8e..d74cf7809b8 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 e1b8e39f3f7..62f57e9b0f6 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 7bc8b0b99a4..4c0f8787756 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 b915951538a..df85da95bfd 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 2259bab622d..7125d3e988e 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 28917aeb740..73d3baa335a 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 cad0d5b3b93..e1ae3720d51 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 8bc11d14545..47b66a0fd02 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 693f5220ecd..798c3ab5887 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 c8f382f35fc..9c922d48a98 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 d27c05a3328..69fcd7338a1 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 f69fa373646..1a9cdb55c93 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 5e5feec4db0..05654da7241 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 fe07856fe8c..6af2f351546 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 9100b04510d..b3cdee5f5e3 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 cba08161892..d9c6c4dfae3 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
--
GitLab