diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 8b2f40e98002ef86ee6ff19b3815ff0a2aa7001b..4121a7a37fcc3cbb81adebaec1de5c57e0f08cef 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -1383,11 +1383,57 @@ specify a source location, either specifically or by using the current
location of an \texttt{AST} visitor.
\lstset{style=frama-c-style}
\begin{itemize}
-\item[] \lstinline{~source:$s$} use the source location $s$ (see \texttt{Log.mli})
-\item[] \lstinline{~current:true} use the current source location
- managed by \texttt{Cil.CurrentLoc}.
+\item[] \lstinline{~source:$s$} use the source position $s$ (see \texttt{Log.mli})
+\item[] \lstinline{~current:true} use the source location
+ managed by \texttt{Current\_loc} (see below).
\end{itemize}
+\codeidxdef{Current\_loc}The \texttt{Current\_loc} module is used to
+manage the code location that is currently under focus.
+The current location must be set, either by \framac's kernel or by
+the plug-in themselves. In particular, \texttt{Cil} visitors update this
+location when visiting each node.
+
+\begin{example}
+The code samples below show how to use and set the current location.
+ \scodeidx{Current\_loc}{let-bindings}
+ \scodeidx{Current\_loc}{with\_loc\_opt}
+ \scodeidx{Current\_loc}{with\_loc}
+ \sscodeidx{Boot}{Main}{extend}
+ \begin{ocamlcode}
+ (* [Current_loc.get()] returns the last location set in Current_loc *)
+ let print_current_loc () =
+ Format.printf "%a@." Cil_datatype.Location.pretty (Current_loc.get ())
+
+ (* [with_loc loc f x] set the current location to loc, executes [f x] and set
+ the location to its old value before returning the result of [f x]. Raised
+ exceptions inside [f] will be caught and re-raised after resetting the
+ location to its previous value. *)
+ let apply_stmt f stmt =
+ Current_loc.with_loc (Cil_datatype.Stmt.loc s) f stmt
+
+ (* [with_loc_opt opt_loc f x] behaves like [with_loc] if [loc_opt] is
+ [Some loc], and does not update the current location if it is [None].*)
+ let apply_code_annot f ca =
+ Current_loc.with_loc_opt (Cil_datatype.Code_annotation.loc ca) f ca
+
+ (* Current_loc defines 2 let-binding operators which call [with_loc] and
+ [with_loc_opt]. Here is a function that set the current location to the
+ expr location, and reset it after the match. *)
+ let do_expr e =
+ let open Current_loc.Operators in
+ let$<>$ UpdatedCurrentLoc = e.eloc in
+ match e.enode with
+ | ...
+
+ (* When we only have a [loc option], we can use the $<?>$ operator *)
+ let do_code_annot f ca =
+ let open Current_loc.Operators in
+ let <?> UpdatedCurrentLoc = Cil_datatype.Code_annotation.loc ca in
+ f ca
+ \end{ocamlcode}
+ \end{example}
+
\paragraph{Emission Options.} By default, a message is echoed to the
user \emph{after} its construction, and it is sent to registered
callbacks when emitted. See Section~\ref{adv:log:events} below for
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index a5767954867ead16b224f920b07110216516c8d1..3ec55d7756b1b2de403ed7bd430516c7916396a8 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -7,6 +7,7 @@ This chapter summarizes the major changes in this documentation between each
\section*{Frama-C+dev}
\begin{itemize}
+\item \textbf{Logging Services}: Document new \texttt{Current\_loc} module
\item There is no more \texttt{Db} module:
\begin{itemize}
\item Whole document: \texttt{Db.Main.extend} is now \texttt{Boot.Main.extend}
diff --git a/src/kernel_internals/typing/alpha.mli b/src/kernel_internals/typing/alpha.mli
index 8fa804cd35c17b855bac7e29f89b0f0660149263..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.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 613d5ee148de1b13ebb7fb05591c2b75dff9b1a7..d9a861b8f4ef4c125c1a6fa7db079a063c06192f 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.CurrentLoc.get()
+ | None -> Current_loc.get()
| Some loc -> loc
in
let append fmt =
@@ -635,7 +635,8 @@ 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 =
- Cil.CurrentLoc.set fi.floc;
+ 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
| Some n, apragma ->
@@ -969,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, 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
@@ -989,7 +990,7 @@ let addLocalToEnv ghost name data =
let addGlobalToEnv ghost name data =
let open Datatype.String.Hashtbl in
- let v = data, 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;
@@ -1007,7 +1008,7 @@ let alphaTable : location Alpha.alphaTable = H.create 307
let fresh_global lookupname =
fst (Alpha.newAlphaName ~alphaTable ~undolist:None ~lookupname
- ~data:(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
@@ -1064,7 +1065,7 @@ let newAlphaName
let undolist =
match undo_scope with None -> None | Some _ -> Some (ref [])
in
- let data = CurrentLoc.get () in
+ let data = Current_loc.get () in
let newname, oldloc =
Alpha.newAlphaName ~alphaTable ~undolist ~lookupname ~data
in
@@ -1252,7 +1253,7 @@ let constFoldToInteger e =
let get_temp_name ghost () =
let undolist = ref [] in
- let data = 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
@@ -1352,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, 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, CurrentLoc.get ()));
+ cabsPushGlobal (GCompTagDecl (self, Current_loc.get ()));
TComp (self, attr)
in
try
@@ -2063,7 +2064,7 @@ struct
(* Make the statement *)
let loop =
mkStmt ~ghost ~valid_sid ~sattr
- (Loop (a,c2block ~ghost body, CurrentLoc.get (), None, None))
+ (Loop (a,c2block ~ghost body, Current_loc.get (), None, None))
in
{ stmts = [ loop,[],[],[],[] ];
cases = body.cases;
@@ -2429,7 +2430,8 @@ class gatherLabelsClass : Cabsvisit.cabsVisitor = object (self)
ChangeDoChildrenPost (blk, fun _ -> (self#removeLocalLabels blk; blk))
method! vstmt s =
- CurrentLoc.set (get_statementloc s);
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = get_statementloc s in
(match s.stmt_node with
| LABEL (lbl,_,_) ->
(try
@@ -2440,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 (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
@@ -2946,6 +2948,12 @@ let empty_preinit() =
(* Set an initializer *)
let rec setOneInit this o preinit =
+ let open Current_loc.Operators in
+ let<?> UpdatedCurrentLoc =
+ match o with
+ | Index (e, _) -> Some e.eloc
+ | _ -> None
+ in
match o with
| NoOffset -> preinit
| _ ->
@@ -2954,8 +2962,8 @@ let rec setOneInit this o preinit =
match o with
| NoOffset -> assert false
| Index({enode = Const(CInt64(i,_,_));eloc}, off) ->
- CurrentLoc.set eloc;
- 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
@@ -2972,8 +2980,7 @@ let rec setOneInit this o preinit =
in
loop 0 (Option.value ~default:[] f.fcomp.cfields), off
| Index({ eloc },_) ->
- CurrentLoc.set eloc;
- abort_context "setOneInit: non-constant index"
+ abort_context ~loc:eloc "setOneInit: non-constant index"
in
let pMaxIdx, pArray =
match this with
@@ -3026,7 +3033,7 @@ let rec collectInitializer
(* parenttype is used to identify a tentative flexible array member
initialization *)
let dkey = Kernel.dkey_typing_init in
- let loc = 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;
@@ -3274,7 +3281,7 @@ and normalSubobj (so: subobj) : unit =
so.soTyp <- bt;
so.soOff <-
addOffset
- (Index(integer ~loc:(CurrentLoc.get()) !current, NoOffset))
+ (Index(integer ~loc:(Current_loc.get()) !current, NoOffset))
parOff
end
@@ -3374,8 +3381,7 @@ let integerArrayLength (leno: exp option) : int =
try lenOfArray leno
with
| LenOfArray cause ->
- Cil.CurrentLoc.set len.eloc;
- abort_context
+ abort_context ~loc:len.eloc
"Array length %a is %a: no explicit initializer allowed."
Cil_printer.pp_exp len Cil.pp_incorrect_array_length cause
@@ -3689,10 +3695,10 @@ let consLabContinue ~ghost (c: chunk) =
| While lr :: _ ->
begin
assert (!doTransformWhile);
- if !lr = "" then c else consLabel ~ghost !lr c (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 (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 () =
@@ -4400,7 +4406,7 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
in
(*TODO: find a better loc*)
- let fields = loop (zero ~loc:(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 *)
@@ -4430,7 +4436,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, CurrentLoc.get ()));
+ cabsPushGlobal (GEnumTag (enum, Current_loc.get ()));
res
| [Cabs.TtypeofE e] ->
@@ -5095,9 +5101,10 @@ and makeCompType loc ghost (isstruct: bool)
let addFieldGroup ~last:last_group (flds : fieldinfo list)
((s: Cabs.spec_elem list), (nl: (Cabs.name * Cabs.expression option) list)) =
+ let open Current_loc.Operators in
(* Do the specifiers exactly once *)
let sugg,loc = match nl with
- | [] -> "",CurrentLoc.get()
+ | [] -> "", Current_loc.get()
| ((n, _, _, loc), _) :: _ -> n,loc
in
let bt, sto, inl, attrs = doSpecList loc ghost sugg s in
@@ -5106,7 +5113,7 @@ and makeCompType loc ghost (isstruct: bool)
(((n,ndt,a,cloc) : Cabs.name), (widtho : Cabs.expression option))
: fieldinfo list =
let source = fst cloc in
- Cil.CurrentLoc.set cloc;
+ let<> UpdatedCurrentLoc = cloc in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~source "Storage or inline not allowed for fields";
let allowZeroSizeArrays = Cil.gccMode () || Cil.msvcMode () in
@@ -5324,7 +5331,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, 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);
@@ -5405,11 +5412,11 @@ and doExp local_env
(e: Cabs.expression)
(what: expAction)
=
+ 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 oldLoc = CurrentLoc.get() in
- CurrentLoc.set loc;
+ 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
@@ -5465,7 +5472,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'', 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'')
@@ -6034,7 +6041,7 @@ and doExp local_env
(se' +++
(mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
(Set(lv, snd (castTo tresult t result),
- CurrentLoc.get ())),[],[lv],r'))
+ Current_loc.get ())),[],[lv],r'))
e'
t
end
@@ -6075,7 +6082,7 @@ and doExp local_env
([var tmp],
local_var_chunk se' tmp +++
(mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
- (Set(var tmp, e', 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.
@@ -6089,7 +6096,7 @@ and doExp local_env
(mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
(Set(lv,
snd (castTo tresult (typeOfLval lv) opresult),
- CurrentLoc.get ())),
+ Current_loc.get ())),
[],[lv], r'))
result
t
@@ -7446,7 +7453,6 @@ and doExp local_env
Cprint.print_expression e;
Format.eprintf "@.";
Format.eprintf "Got: chunk:'%a'@." d_chunk b;*)
- CurrentLoc.set oldLoc;
result
and normalize_unop unop action asconst local_env e what =
@@ -7754,7 +7760,7 @@ and doCondExp local_env asconst
and compileCondExp ?(hide=false) ~ghost ce st sf =
match ce with
| CEAnd (ce1, ce2) ->
- let loc = 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)
@@ -7786,7 +7792,7 @@ and compileCondExp ?(hide=false) ~ghost ce st sf =
compileCondExp ~hide ~ghost ce1 st' sf'
| CEOr (ce1, ce2) ->
- let loc = 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)
@@ -7806,7 +7812,7 @@ and compileCondExp ?(hide=false) ~ghost ce st sf =
in
let labstmt =
if sf_fall_through then
- consLabel ~ghost lab empty (CurrentLoc.get ()) false
+ consLabel ~ghost lab empty (Current_loc.get ()) false
else skipChunk
in
let (@@@) s1 s2 = s1 @@@ (s2, ghost) in
@@ -7973,7 +7979,8 @@ and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
– the list of unused initializers if any (should be empty most of the time)
*)
and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
- CurrentLoc.set loc;
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = loc in
let source = fst loc in
let ghost = local_env.is_ghost in
let whoami fmt = Cil_printer.pp_lval fmt (Var so.host, so.soOff) in
@@ -8362,7 +8369,7 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
end
| Cabs.ATINDEX_INIT(idx, whatnext) -> begin
- CurrentLoc.set idx.expr_loc;
+ let<> UpdatedCurrentLoc = idx.expr_loc in
match unrollType so.soTyp with
| TArray (bt, leno, _) ->
let ilen = integerArrayLength leno in
@@ -8417,7 +8424,7 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
in
let doidxs = add_reads ~ghost idxs'.eloc rs doidxs in
let doidxe = add_reads ~ghost idxe'.eloc re doidxe in
- Cil.CurrentLoc.set (fst idxs'.eloc, snd idxe'.eloc);
+ let<> UpdatedCurrentLoc = (fst idxs'.eloc, snd idxe'.eloc) in
if isNotEmpty doidxs || isNotEmpty doidxe then
abort_context "Range designators are not constants";
let first, last =
@@ -8458,6 +8465,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 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
@@ -8486,7 +8494,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 (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;
@@ -8583,8 +8591,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}, CurrentLoc.get ()));
- H.add alreadyDefined vi.vname (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) &&
@@ -8599,27 +8607,31 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
if isFunctionType vi.vtype then begin
if not vi.vdefined then
setFormalsDecl vi vi.vtype;
- let spec =
+ let spec, loc =
match logic_spec with
- | None -> empty_funspec ()
+ | None -> empty_funspec (), Current_loc.get ()
| Some (spec,loc) ->
begin
- CurrentLoc.set loc;
- try
- (* it can not have old behavior names, since this is the
- first time we see the declaration.
- *)
- Ltyping.funspec [] vi None vi.vtype spec
- with LogicTypeError ((source,_),msg) ->
- Kernel.warning ~wkey:Kernel.wkey_annot_error ~source
- "%s. Ignoring specification of function %s" msg vi.vname;
- empty_funspec ()
+ let<> UpdatedCurrentLoc = loc in
+ let loc = Current_loc.get () in
+ let res =
+ try
+ (* it can not have old behavior names, since this is the
+ first time we see the declaration.
+ *)
+ Ltyping.funspec [] vi None vi.vtype spec
+ with LogicTypeError ((source,_),msg) ->
+ Kernel.warning ~wkey:Kernel.wkey_annot_error ~source
+ "%s. Ignoring specification of function %s" msg vi.vname;
+ empty_funspec ()
+ in
+ res, loc
end
in
- cabsPushGlobal (GFunDecl (spec, vi, CurrentLoc.get ()));
+ cabsPushGlobal (GFunDecl (spec, vi, loc));
end
else
- cabsPushGlobal (GVarDecl (vi, CurrentLoc.get ()));
+ cabsPushGlobal (GVarDecl (vi, Current_loc.get ()));
vi
end else begin
Kernel.debug ~dkey:Kernel.dkey_typing_global
@@ -8627,7 +8639,6 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
(match logic_spec with
| None -> ()
| Some (spec,loc) ->
- CurrentLoc.set loc;
let merge_spec = function
| GFunDecl(old_spec, _, oldloc) ->
let behaviors =
@@ -8645,7 +8656,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
@@ -8805,13 +8816,13 @@ and createLocal ghost ((_, sto, _, _) as specs)
Push a prototype for the function, just in case. *)
cabsPushGlobal
(GFunDecl (empty_funspec (), !currentFunctionFDEC.svar,
- CurrentLoc.get ()));
+ Current_loc.get ()));
Cil.setFormalsDecl
!currentFunctionFDEC.svar !currentFunctionFDEC.svar.vtype;
Some ie'
end
in
- cabsPushGlobal (GVar(vi, {init = init}, 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 *)
@@ -8876,7 +8887,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
assert alloca_bounds: 0 < elt_size * array_size <= max_bounds
*)
(se0 +++ (
- let castloc = 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
@@ -8908,7 +8919,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
let setlen = se0 +++
(mkStmtOneInstr ~ghost ~valid_sid
(Set(var savelen, mkCast ~newt:savelen.vtype len,
- CurrentLoc.get ())),
+ Current_loc.get ())),
[],[],[])
in
(* Initialize the variable *)
@@ -8938,7 +8949,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
(vi,AssignInit
(SingleInit
(mkCast ~newt:vi.vtype (new_exp ~loc (Lval(var tmp))))),
- CurrentLoc.get ())),
+ Current_loc.get ())),
[],[var vi],[var tmp])
end
end else empty
@@ -9038,10 +9049,11 @@ and doAliasFun ghost vtype (thisname:string) (othername:string)
(* Do one declaration *)
-and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
+and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = get_definitionloc def in
+ match def with
| Cabs.DECDEF (logic_spec, (s, nl), loc) ->
- let cloc = convLoc loc in
- CurrentLoc.set cloc;
(* Do the specifiers exactly once *)
let sugg =
match nl with
@@ -9049,11 +9061,11 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
| ((n, _, _, _), _) :: _ -> n
in
let ghost = local_env.is_ghost in
- let spec_res = doSpecList cloc ghost sugg s in
+ let spec_res = doSpecList loc ghost sugg s in
(* Do all the variables and concatenate the resulting statements *)
let doOneDeclarator (acc: chunk) (name: init_name) =
let (n,ndt,a,l),_ = name in
- CurrentLoc.set l;
+ let<> UpdatedCurrentLoc = l in
if isglobal then begin
let bt,_,_,attrs = spec_res in
let vtype, nattr =
@@ -9067,13 +9079,13 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
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 (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 (CurrentLoc.get()));
+ "Bad alias attribute at %a" Cil_printer.pp_location (Current_loc.get()));
acc
end else
acc @@@ (createLocal ghost spec_res name, ghost)
@@ -9101,18 +9113,16 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
res
end
end
- | Cabs.TYPEDEF (ng, loc) ->
- CurrentLoc.set (convLoc loc); doTypedef local_env.is_ghost ng; empty
+ | Cabs.TYPEDEF (ng, _) ->
+ doTypedef local_env.is_ghost ng; empty
- | Cabs.ONLYTYPEDEF (s, loc) ->
- CurrentLoc.set (convLoc loc); doOnlyTypedef local_env.is_ghost s; empty
+ | Cabs.ONLYTYPEDEF (s, _) ->
+ doOnlyTypedef local_env.is_ghost s; empty
- | Cabs.GLOBASM (s,loc) when isglobal ->
- CurrentLoc.set (convLoc loc);
- cabsPushGlobal (GAsm (s, CurrentLoc.get ())); empty
+ | Cabs.GLOBASM (s, _) when isglobal ->
+ cabsPushGlobal (GAsm (s, Current_loc.get ())); empty
- | Cabs.PRAGMA (a, loc) when isglobal -> begin
- CurrentLoc.set (convLoc loc);
+ | Cabs.PRAGMA (a, _) when isglobal -> begin
match doAttr local_env.is_ghost ("dummy", [a]) with
| [Attr("dummy", [a'])] ->
let a'' =
@@ -9127,15 +9137,14 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
in
Option.iter
(fun a'' ->
- cabsPushGlobal (GPragma (a'', CurrentLoc.get ())))
+ cabsPushGlobal (GPragma (a'', Current_loc.get ())))
a'';
empty
| _ -> abort_context "Too many attributes in pragma"
end
- | Cabs.STATIC_ASSERT (e, s, loc) -> begin
- CurrentLoc.set (convLoc loc);
+ | Cabs.STATIC_ASSERT (e, s, _) -> begin
let (_, _, cond_exp, _) = doExp local_env CConst e ADrop in
begin
match Cil.constFoldToInt ~machdep:true cond_exp with
@@ -9162,7 +9171,6 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
let endloc = loc2 in
Kernel.debug ~dkey:Kernel.dkey_typing_global
"Definition of %s at %a\n" n Cil_printer.pp_location idloc;
- CurrentLoc.set idloc;
FuncLocs.add_loc ?spec loc1 endloc n;
IH.clear callTempVars;
@@ -9186,12 +9194,11 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
* they need alpha-conv *)
enterScope (); (* Start the scope *)
ignore (Cabsvisit.visitCabsBlock (new gatherLabelsClass) body);
- CurrentLoc.set idloc;
+
IH.clear varSizeArrays;
(* Enter all the function's labels into the alpha conversion table *)
ignore (Cabsvisit.visitCabsBlock (new registerLabelsVisitor) body);
- CurrentLoc.set idloc;
(* Do not process transparent unions in function definitions.
* We'll do it later *)
@@ -9271,7 +9278,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
| [], _ -> []
| fl, [] -> (* no more locs available *)
- List.map (doFormal (CurrentLoc.get ())) fl
+ List.map (doFormal (Current_loc.get ())) fl
| f::fl, (_,(_,_,_,l))::ll ->
(* sfg: these lets seem to be necessary to
@@ -9347,10 +9354,26 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
in
let behaviors = find_existing_behaviors !currentFunctionFDEC.svar in
(******* Now do the spec *******)
+ let merge_spec () =
+ (* Merge pre-existing spec if needed. *)
+ if has_decl then begin
+ let merge_spec = function
+ | GFunDecl(old_spec,_,oldloc) as g ->
+ if not (Cil.is_empty_funspec old_spec) then begin
+ rename_spec g;
+ Logic_utils.merge_funspec ~oldloc
+ !currentFunctionFDEC.sspec old_spec;
+ Logic_utils.clear_funspec old_spec;
+ end;
+ | _ -> assert false
+ in
+ update_fundec_in_theFile !currentFunctionFDEC.svar merge_spec
+ end
+ in
begin
match spec with
| Some (spec,loc) ->
- CurrentLoc.set loc;
+ let<> UpdatedCurrentLoc = loc in
(try
!currentFunctionFDEC.sspec <-
Ltyping.funspec behaviors
@@ -9360,22 +9383,9 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
with LogicTypeError ((source,_),msg) ->
Kernel.warning ~wkey:Kernel.wkey_annot_error ~source
"%s. Ignoring logic specification of function %s"
- msg !currentFunctionFDEC.svar.vname)
- | None -> ()
- end;
- (* Merge pre-existing spec if needed. *)
- if has_decl then begin
- let merge_spec = function
- | GFunDecl(old_spec,_,oldloc) as g ->
- if not (Cil.is_empty_funspec old_spec) then begin
- rename_spec g;
- Logic_utils.merge_funspec ~oldloc
- !currentFunctionFDEC.sspec old_spec;
- Logic_utils.clear_funspec old_spec;
- end
- | _ -> assert false
- in
- update_fundec_in_theFile !currentFunctionFDEC.svar merge_spec
+ msg !currentFunctionFDEC.svar.vname);
+ merge_spec ()
+ | None -> merge_spec ()
end;
(********** Now do the BODY *************)
let _ =
@@ -9458,7 +9468,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
(* 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 = CurrentLoc.get () in
+ let loc = Current_loc.get () in
let shadow =
makeTempVar
!currentFunctionFDEC ~insert:false
@@ -9481,6 +9491,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
(* Now see whether we can fall through to the end of the function *)
if blockFallsThrough !currentFunctionFDEC.sbody then begin
let loc = endloc in
+ let<> UpdatedCurrentLoc = endloc in
let protect_return,retval =
(* Guard the [return] instructions we add with an
[\assert \false]*)
@@ -9537,8 +9548,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
empty
end (* FUNDEF *)
- | LINKAGE (n, loc, dl) ->
- CurrentLoc.set (convLoc loc);
+ | LINKAGE (n, _, dl) ->
if n <> "C" then
Kernel.warning ~current:true
"Encountered linkage specification \"%s\"" n;
@@ -9559,7 +9569,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
List.iter
(fun decl ->
let loc = convLoc decl.Logic_ptree.decl_loc in
- CurrentLoc.set loc;
+ let<> UpdatedCurrentLoc = loc in
try
let tdecl = Ltyping.annot decl in
let attr = fc_stdlib_attribute [] in
@@ -9567,11 +9577,12 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
List.fold_left
(Fun.flip Logic_utils.add_attribute_glob_annot) tdecl attr
in
- cabsPushGlobal (GAnnot(tdecl,CurrentLoc.get ()))
+ cabsPushGlobal (GAnnot(tdecl,Current_loc.get ()))
with LogicTypeError ((source,_),msg) ->
Kernel.warning
~wkey:Kernel.wkey_annot_error ~source
- "%s. Ignoring global annotation" msg)
+ "%s. Ignoring global annotation" msg
+ )
decl;
end;
empty
@@ -9588,7 +9599,7 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
trying to convert it to a global-level typedef.@ \
Note that this may lead to incoherent error messages.";
let bt, sto, inl, attrs =
- doSpecList (CurrentLoc.get()) ghost (suggestAnonName nl) specs
+ doSpecList (Current_loc.get()) ghost (suggestAnonName nl) specs
in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true
@@ -9682,14 +9693,14 @@ 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, CurrentLoc.get ()))
+ cabsPushGlobal (GType (ti, Current_loc.get ()))
end
in
List.iter createTypedef nl
and doOnlyTypedef ghost (specs: Cabs.spec_elem list) : unit =
let bt, sto, inl, attrs =
- doSpecList (CurrentLoc.get()) ghost "" specs
+ doSpecList (Current_loc.get()) ghost "" specs
in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true
@@ -9717,12 +9728,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, 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, 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 \
@@ -9832,6 +9843,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 Current_loc.Operators in
let mk_loop_annot a loc =
try
List.map
@@ -9845,12 +9857,12 @@ 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<> UpdatedCurrentLoc = convLoc (get_statementloc s) in
match s.stmt_node with
| Cabs.NOP loc ->
{ empty
with stmts = [mkEmptyStmt ~ghost ~valid_sid ~loc (), [],[],[],[]]}
| Cabs.COMPUTATION (e, loc) ->
- CurrentLoc.set (convLoc loc);
let (lasts, data) = !gnu_body_result in
if lasts == s then begin (* This is the last in a GNU_BODY *)
let (s', e', t') = doFullExp local_env CNoConst e (AExp None) in
@@ -9873,8 +9885,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
s'
end
- | Cabs.BLOCK (b, loc,_) ->
- CurrentLoc.set (convLoc loc);
+ | Cabs.BLOCK (b, _, _) ->
let c = doBodyScope local_env b in
let b = c2block ~ghost c in
b.battrs <- addAttributes [Attr(frama_c_keep_block,[])] b.battrs;
@@ -9886,10 +9897,9 @@ and doStatement local_env (s : Cabs.statement) : chunk =
let c2 = doStatement local_env s2 in
c1 @@@ (c2, ghost)
- | Cabs.IF(e,st,sf,loc) ->
+ | Cabs.IF(e, st, sf, _) ->
let st' = doStatement local_env st in
let sf' = doStatement local_env sf in
- CurrentLoc.set (convLoc loc);
doCondition ~is_loop:false local_env CNoConst e st' sf'
| Cabs.WHILE(a,e,s,loc) ->
@@ -9904,7 +9914,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
let loc' = convLoc loc in
let break_cond = breakChunk ~ghost loc' in
exitLoop ();
- CurrentLoc.set loc';
loopChunk ~ghost ~sattr:[Attr("while",[])] a
((doCondition ~is_loop:true local_env CNoConst e skipChunk break_cond)
@@@ (s', ghost))
@@ -9914,7 +9923,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
let a = mk_loop_annot a loc in
let s' = doStatement local_env s in
let loc' = convLoc loc in
- CurrentLoc.set loc';
(* No 'break' instruction can exit the chunk *)
let no_break chunk =
List.for_all (fun (s, _, _, _, _) -> not (stmtCanBreak s)) chunk.stmts
@@ -9945,7 +9953,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Cabs.FOR(a,fc1,e2,e3,s,loc) -> begin
let loc' = convLoc loc in
- CurrentLoc.set loc';
enterScope (); (* Just in case we have a declaration *)
ForLoopHook.apply (fc1,e2,e3,s);
let (se1, _, _) , has_decl =
@@ -9959,7 +9966,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
let a = mk_loop_annot a loc in
let s' = doStatement local_env s in
(*Kernel.debug "Loop body : %a" d_chunk s';*)
- CurrentLoc.set loc';
let s'' = consLabContinue ~ghost se3 in
let break_cond = breakChunk ~ghost loc' in
exitLoop ();
@@ -9982,17 +9988,14 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Cabs.BREAK loc ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
breakChunk ~ghost loc'
| Cabs.CONTINUE loc ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
continueOrLabelChunk ~ghost loc'
| Cabs.RETURN ({ expr_node = Cabs.NOTHING}, loc) ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
if not (isVoidType !currentReturnType) then
Kernel.error ~current:true
"Return statement without a value in function returning %a\n"
@@ -10001,7 +10004,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Cabs.RETURN (e, loc) ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
(* Sometimes we return the result of a void function call *)
if isVoidType !currentReturnType then begin
Kernel.error ~current:true
@@ -10020,7 +10022,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Cabs.SWITCH (e, s, loc) ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
let (se, e', et) = doFullExp local_env CNoConst e (AExp None) in
if not (Cil.isIntegralType et) then
Kernel.error ~once:true ~current:true "Switch on a non-integer expression.";
@@ -10033,7 +10034,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Cabs.CASE (e, s, loc) ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
let (se, e', _) = doFullExp local_env CConst e (AExp None) in
if isNotEmpty se || not (Cil.isIntegerConstant e') then
Kernel.error ~once:true ~current:true
@@ -10049,7 +10049,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Cabs.CASERANGE (el, eh, s, loc) ->
let loc' = convLoc loc in
- CurrentLoc.set loc;
let (sel, el', _) = doFullExp local_env CNoConst el (AExp None) in
let (seh, eh', _) = doFullExp local_env CNoConst eh (AExp None) in
if isNotEmpty sel || isNotEmpty seh then
@@ -10073,11 +10072,9 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Cabs.DEFAULT (s, loc) ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
defaultChunk ~ghost loc' (doStatement local_env s)
| Cabs.LABEL (l, s, loc) ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
add_label_env l;
C_logic_env.add_current_label l;
(* Lookup the label because it might have been locally defined *)
@@ -10088,13 +10085,11 @@ and doStatement local_env (s : Cabs.statement) : chunk =
| Cabs.GOTO (l, loc) ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
(* Maybe we need to rename this label *)
gotoChunk ~ghost (lookupLabel ghost l) loc'
| Cabs.COMPGOTO (e, loc) -> begin
let loc' = convLoc loc in
- CurrentLoc.set loc';
(* Do the expression *)
let se, e', _ =
doFullExp local_env CNoConst e (AExp (Some voidPtrType))
@@ -10148,7 +10143,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
(* Make sure all the outs are variables *)
let loc' = convLoc loc in
let attr' = doAttributes local_env.is_ghost asmattr in
- CurrentLoc.set loc';
let stmts : chunk ref = ref empty in
let ext_asm =
match details with
@@ -10200,7 +10194,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
ghost)
| THROW (e,loc) ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
(match e with
| None -> s2c (mkStmt ~ghost ~valid_sid (Throw (None,loc')))
| Some e ->
@@ -10209,7 +10202,6 @@ and doStatement local_env (s : Cabs.statement) : chunk =
(s2c (mkStmt ~ghost ~valid_sid (Throw (Some (e,t),loc'))),ghost))
| TRY_CATCH(stry,l,loc) ->
let loc' = convLoc loc in
- CurrentLoc.set loc';
let chunk_try = doStatement local_env stry in
let type_one_catch (var,scatch) =
enterScope();
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index 8b0194251b24916a55f9511cf2bac97d2b97c126..7da177464c06d83a1dc793427313bd23c4946af4 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -352,6 +352,7 @@ let freshLabel (base:string) =
let xform_switch_block ?(keepSwitch=false) b =
+ 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
@@ -439,7 +440,7 @@ let xform_switch_block ?(keepSwitch=false) b =
[] -> []
| s :: rest ->
begin
- CurrentLoc.set (Stmt.loc s);
+ 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 3d017490d7d37b0099814ee2fd6e4e67ef584c78..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 (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 ebfddbe38cf7c713ae56f44d57c075a73e07c962..cca4dd7a60ff1f685d7ba89a3f76939a0b4f7a11 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -865,9 +865,11 @@ let rec global_annot_without_irrelevant_attributes ga =
Dextended(ext, drop_attributes_for_merge attr, loc)
| Dfun_or_pred _ | Dtype_annot _ | Dmodel_annot _ | Dinvariant _ -> ga
-let rec global_annot_pass1 g = match g with
+let rec global_annot_pass1 g =
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Cil_datatype.Global_annotation.loc g in
+ match g with
| Dvolatile(hs,rvi,wvi,_,loc) ->
- CurrentLoc.set loc;
let process_term_kind (t,k as id) =
let node =
VolatileMerging.getNode
@@ -890,12 +892,10 @@ let rec global_annot_pass1 g = match g with
if Option.is_some wvi then process_term_kind (x,W))
hs
| Daxiomatic(id,decls,_,l) ->
- CurrentLoc.set l;
ignore (PlainMerging.getNode laEq laSyn !currentFidx id (id,decls)
(Some (l,!currentDeclIdx)));
List.iter global_annot_pass1 decls
| Dfun_or_pred (li,l) ->
- CurrentLoc.set l;
let mynode =
LogicMerging.getNode
lfEq lfSyn !currentFidx li li None
@@ -906,32 +906,26 @@ let rec global_annot_pass1 g = match g with
(LogicMerging.getNode lfEq lfSyn !currentFidx li li
(Some (l, !currentDeclIdx)))
| Dtype_annot (pi,l) ->
- CurrentLoc.set l;
ignore (LogicMerging.getNode
lfEq lfSyn !currentFidx pi pi
(Some (l, !currentDeclIdx)))
| Dmodel_annot (mfi,l) ->
- CurrentLoc.set l;
ignore (ModelMerging.getNode
mfEq mfSyn !currentFidx (mfi.mi_name,mfi.mi_base_type) mfi
(Some (l, !currentDeclIdx)))
| Dinvariant (pi,l) ->
- CurrentLoc.set l;
ignore (LogicMerging.getNode
lfEq lfSyn !currentFidx pi pi
(Some (l, !currentDeclIdx)))
| Dtype (info,l) ->
- CurrentLoc.set l;
ignore (PlainMerging.getNode ltEq ltSyn !currentFidx info.lt_name info
(Some (l, !currentDeclIdx)))
| Dlemma (n,labs,typs,st,attr,l) ->
- CurrentLoc.set l;
ignore (PlainMerging.getNode
llEq llSyn !currentFidx n (n,(labs,typs,st,attr,l))
(Some (l, !currentDeclIdx)))
| Dextended(ext,_,l) ->
- CurrentLoc.set l;
ignore
(ExtMerging.getNode extEq extSyn !currentFidx
ext ext (Some (l,!currentDeclIdx)))
@@ -1099,8 +1093,6 @@ let matchCompInfoGen (combineF : combineFunction)
let old_len = List.length oldfields in
let len = List.length fields in
if old_len <> len then begin
- let curLoc = CurrentLoc.get () in (* d_global blows this away.. *)
- CurrentLoc.set curLoc;
let aggregate_name = if cstruct then "struct" else "union" in
let msg = Printf.sprintf
"different number of fields in %s %s and %s %s: %d != %d."
@@ -1576,6 +1568,7 @@ let remove_function_statics fdec =
) !theFile
let oneFilePass1 (f:file) : unit =
+ 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 ;
@@ -1590,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:(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)
@@ -1715,86 +1708,85 @@ let oneFilePass1 (f:file) : unit =
newrep.ndata.vattr <- addAttributes oldvi.vattr vi.vattr;
newrep.ndata.vdecl <- newdecl
in
- List.iter
- (function
- | GVarDecl (vi, l) | GVar (vi, _, l) | GFunDecl (_, vi, l)->
- CurrentLoc.set l;
- incr currentDeclIdx;
- if vi.vstorage <> Static then begin
- matchVarinfo ~fromGFun:false vi (l, !currentDeclIdx);
- end
-
- | GFun (fdec, l) ->
- CurrentLoc.set l;
- incr currentDeclIdx;
- (* Save the names of the formal arguments *)
- let _, args, _, _ = splitFunctionTypeVI fdec.svar in
- H.add formalNames (!currentFidx, fdec.svar.vname)
- (List.map (fun (n,_,_) -> n) (argsToList args));
- (* Force inline functions to be static. *)
- (* GN: This turns out to be wrong. inline functions are external,
- * unless specified to be static. *)
- (*
- if fdec.svar.vinline && fdec.svar.vstorage = NoStorage then
- fdec.svar.vstorage <- Static;
- *)
- if fdec.svar.vstorage <> Static then begin
- matchVarinfo ~fromGFun:true fdec.svar (l, !currentDeclIdx)
- end else begin
- if fdec.svar.vinline && mergeInlines then
- (* Just create the nodes for inline functions *)
- ignore (PlainMerging.getNode iEq iSyn !currentFidx
- fdec.svar.vname fdec.svar (Some (l, !currentDeclIdx)))
- end
- (* Make nodes for the defined type and structure tags *)
- | GType (t, l) ->
- incr currentDeclIdx;
- t.treferenced <- false;
- if t.tname <> "" then (* The empty names are just for introducing
- * undefined comp tags *)
- ignore (PlainMerging.getNode tEq tSyn !currentFidx t.tname t
- (Some (l, !currentDeclIdx)))
- else begin (* Go inside and clean the referenced flag for the
- * declared tags *)
- match t.ttype with
- TComp (ci, _ ) ->
- ci.creferenced <- false;
- (* Create a node for it *)
- ignore
- (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci None)
-
- | TEnum (ei, _) ->
- ei.ereferenced <- false;
- ignore
- (EnumMerging.getNode eEq eSyn !currentFidx ei ei None)
-
- | _ -> (Kernel.fatal "Anonymous Gtype is not TComp")
- end
+ let iter g =
+ let<> UpdatedCurrentLoc = Cil_datatype.Global.loc g in
+ match g with
+ | GVarDecl (vi, l) | GVar (vi, _, l) | GFunDecl (_, vi, l)->
+ incr currentDeclIdx;
+ if vi.vstorage <> Static then begin
+ matchVarinfo ~fromGFun:false vi (l, !currentDeclIdx);
+ end
- | GCompTag (ci, l) ->
- incr currentDeclIdx;
- ci.creferenced <- false;
- ignore (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci
+ | GFun (fdec, l) ->
+ incr currentDeclIdx;
+ (* Save the names of the formal arguments *)
+ let _, args, _, _ = splitFunctionTypeVI fdec.svar in
+ H.add formalNames (!currentFidx, fdec.svar.vname)
+ (List.map (fun (n,_,_) -> n) (argsToList args));
+ (* Force inline functions to be static. *)
+ (* GN: This turns out to be wrong. inline functions are external,
+ * unless specified to be static. *)
+ (*
+ if fdec.svar.vinline && fdec.svar.vstorage = NoStorage then
+ fdec.svar.vstorage <- Static;
+ *)
+ if fdec.svar.vstorage <> Static then begin
+ matchVarinfo ~fromGFun:true fdec.svar (l, !currentDeclIdx)
+ end else begin
+ if fdec.svar.vinline && mergeInlines then
+ (* Just create the nodes for inline functions *)
+ ignore (PlainMerging.getNode iEq iSyn !currentFidx
+ fdec.svar.vname fdec.svar (Some (l, !currentDeclIdx)))
+ end
+ (* Make nodes for the defined type and structure tags *)
+ | GType (t, l) ->
+ incr currentDeclIdx;
+ t.treferenced <- false;
+ if t.tname <> "" then (* The empty names are just for introducing
+ * undefined comp tags *)
+ ignore (PlainMerging.getNode tEq tSyn !currentFidx t.tname t
(Some (l, !currentDeclIdx)))
- | GCompTagDecl (ci,_) -> ci.creferenced <- false
- | GEnumTagDecl (ei,_) -> ei.ereferenced <- false
- | GEnumTag (ei, l) ->
- incr currentDeclIdx;
- let orig_name =
- if ei.eorig_name = "" then ei.ename else ei.eorig_name
- in
- ignore (Alpha.newAlphaName ~alphaTable:aeAlpha ~undolist:None
- ~lookupname:orig_name ~data:l);
- ei.ereferenced <- false;
- ignore
- (EnumMerging.getNode eEq eSyn !currentFidx ei ei
- (Some (l, !currentDeclIdx)))
- | GAnnot (gannot,l) ->
- CurrentLoc.set l;
- incr currentDeclIdx;
- global_annot_pass1 gannot
- | GText _ | GPragma _ | GAsm _ -> ())
- f.globals
+ else begin (* Go inside and clean the referenced flag for the
+ * declared tags *)
+ match t.ttype with
+ TComp (ci, _ ) ->
+ ci.creferenced <- false;
+ (* Create a node for it *)
+ ignore
+ (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci None)
+
+ | TEnum (ei, _) ->
+ ei.ereferenced <- false;
+ ignore
+ (EnumMerging.getNode eEq eSyn !currentFidx ei ei None)
+
+ | _ -> (Kernel.fatal "Anonymous Gtype is not TComp")
+ end
+
+ | GCompTag (ci, l) ->
+ incr currentDeclIdx;
+ ci.creferenced <- false;
+ ignore (PlainMerging.getNode sEq sSyn !currentFidx ci.cname ci
+ (Some (l, !currentDeclIdx)))
+ | GCompTagDecl (ci,_) -> ci.creferenced <- false
+ | GEnumTagDecl (ei,_) -> ei.ereferenced <- false
+ | GEnumTag (ei, l) ->
+ incr currentDeclIdx;
+ let orig_name =
+ if ei.eorig_name = "" then ei.ename else ei.eorig_name
+ in
+ ignore (Alpha.newAlphaName ~alphaTable:aeAlpha ~undolist:None
+ ~lookupname:orig_name ~data:l);
+ ei.ereferenced <- false;
+ ignore
+ (EnumMerging.getNode eEq eSyn !currentFidx ei ei
+ (Some (l, !currentDeclIdx)))
+ | GAnnot (gannot, _) ->
+ incr currentDeclIdx;
+ global_annot_pass1 gannot
+ | GText _ | GPragma _ | GAsm _ -> ()
+ in
+ List.iter iter f.globals
let matchInlines (oldfidx: int) (oldi: varinfo)
(fidx: int) (i: varinfo) =
@@ -2202,10 +2194,11 @@ end
let renameInlinesVisitor = new renameInlineVisitorClass
let rec logic_annot_pass2 ~in_axiomatic g a =
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Cil_datatype.Global_annotation.loc a in
match a with
- | Dfun_or_pred (li,l) ->
+ | Dfun_or_pred (li, _) ->
begin
- CurrentLoc.set l;
match LogicMerging.findReplacement true lfEq !currentFidx li with
| None ->
if not in_axiomatic then
@@ -2213,11 +2206,10 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
Logic_utils.add_logic_function li;
| Some _ -> ()
(* FIXME: should we perform same actions
- as the case Dlogic_reads above ? *)
+ as the case Dlogic_reads above ? *)
end
- | Dtype (t,l) ->
+ | Dtype (t, _) ->
begin
- CurrentLoc.set l;
match PlainMerging.findReplacement true ltEq !currentFidx t.lt_name with
| None ->
if not in_axiomatic then
@@ -2234,9 +2226,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
)
| Some _ -> ()
end
- | Dinvariant (li,l) ->
+ | Dinvariant (li, _) ->
begin
- CurrentLoc.set l;
match LogicMerging.findReplacement true lfEq !currentFidx li with
| None ->
if in_axiomatic then Kernel.abort ~current:true
@@ -2246,9 +2237,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
(LogicMerging.find_eq_table lfEq (!currentFidx,li)).ndata
| Some _ -> ()
end
- | Dtype_annot (n,l) ->
+ | Dtype_annot (n, _) ->
begin
- CurrentLoc.set l;
match LogicMerging.findReplacement true lfEq !currentFidx n with
| None ->
let g = visitCilGlobal renameVisitor g in
@@ -2258,9 +2248,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
(LogicMerging.find_eq_table lfEq (!currentFidx,n)).ndata
| Some _ -> ()
end
- | Dmodel_annot (mf,l) ->
+ | Dmodel_annot (mf, l) ->
begin
- CurrentLoc.set l;
match
ModelMerging.findReplacement
true mfEq !currentFidx (mf.mi_name,mf.mi_base_type)
@@ -2273,8 +2262,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
mfEq (!currentFidx,(mf'.mi_name,mf'.mi_base_type))
in
(* Adds a new representative. Do not replace directly
- my_node, as there might be some pointers to it from
- other files.
+ my_node, as there might be some pointers to it from
+ other files.
*)
let my_node' = { my_node with ndata = mf' } in
my_node.nrep <- my_node'; (* my_node' represents my_node *)
@@ -2293,16 +2282,15 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
mfEq (!currentFidx,(mf'.mi_name,mf'.mi_base_type))).ndata;
| Some _ -> ()
end
- | Dlemma (n,_,_,_,_,l) ->
+ | Dlemma (n, _, _, _, _, _) ->
begin
- CurrentLoc.set l;
match PlainMerging.findReplacement true llEq !currentFidx n with
None ->
if not in_axiomatic then
mergePushGlobals (visitCilGlobal renameVisitor g)
| Some _ -> ()
end
- | Dvolatile(vi,rd,wr,attr,loc) ->
+ | Dvolatile(vi, rd, wr, attr, loc) ->
let is_representative id =
Option.is_none
(VolatileMerging.findReplacement true lvEq !currentFidx id)
@@ -2315,7 +2303,6 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
mergePushGlobals
(visitCilGlobal renameVisitor (GAnnot (annot,loc)))
in
- CurrentLoc.set loc;
(* check whether some volatile location clashes with a previous
annotation. Warnings about that have been generated during pass 1
*)
@@ -2353,9 +2340,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
if Option.is_some rd then push_volatile only_reads rd None;
if Option.is_some wr then push_volatile only_writes None wr
end
- | Daxiomatic(n,l,_,loc) ->
+ | Daxiomatic(n, l, _, _) ->
begin
- CurrentLoc.set loc;
match PlainMerging.findReplacement true laEq !currentFidx n with
None ->
if in_axiomatic then Kernel.abort ~current:true
@@ -2364,9 +2350,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
List.iter (logic_annot_pass2 ~in_axiomatic:true g) l
| Some _ -> ()
end
- | Dextended(ext,_,loc) ->
- (CurrentLoc.set loc;
- match ExtMerging.findReplacement true extEq !currentFidx ext with
+ | Dextended(ext, _, _) ->
+ (match ExtMerging.findReplacement true extEq !currentFidx ext with
| None -> mergePushGlobals (visitCilGlobal renameVisitor g);
| Some _ -> ())
@@ -2572,6 +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 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
@@ -2580,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:(CurrentLoc.get ())
+ ~lookupname:vi.vname ~data:(Current_loc.get ())
in
let formals_decl =
try Some (Cil.getFormalsDecl vi)
@@ -2619,9 +2605,9 @@ let oneFilePass2 (f: file) =
end
end
in
+ let<> UpdatedCurrentLoc = Cil_datatype.Global.loc g in
match g with
| GVarDecl (vi, l) as g ->
- CurrentLoc.set l;
incr currentDeclIdx;
let vi' = processVarinfo vi l in
if vi == vi' && not (H.mem emittedVarDecls vi'.vname) then begin
@@ -2631,7 +2617,6 @@ let oneFilePass2 (f: file) =
end
| GFunDecl (spec,vi, l) as g ->
- CurrentLoc.set l;
incr currentDeclIdx;
let vi' = processVarinfo vi l in
let spec' = visitCilFunspec renameVisitor spec in
@@ -2653,7 +2638,6 @@ let oneFilePass2 (f: file) =
end
| GVar (vi, init, l) ->
- CurrentLoc.set l;
incr currentDeclIdx;
if not (is_ignored_vi vi) then begin
let vi' = processVarinfo vi l in
@@ -2693,7 +2677,6 @@ let oneFilePass2 (f: file) =
end
| GFun (fdec, l) as g ->
- CurrentLoc.set l;
incr currentDeclIdx;
if not (is_ignored_vi fdec.svar) then begin
(* We apply the renaming *)
@@ -2908,8 +2891,7 @@ let oneFilePass2 (f: file) =
end
end
- | GCompTag (ci, l) as g -> begin
- CurrentLoc.set l;
+ | GCompTag (ci, _) as g -> begin
incr currentDeclIdx;
if ci.creferenced then
()
@@ -2938,7 +2920,7 @@ let oneFilePass2 (f: file) =
in
let newname, _ =
Alpha.newAlphaName ~alphaTable:sAlpha ~undolist:None
- ~lookupname:orig_name ~data:(CurrentLoc.get ())
+ ~lookupname:orig_name ~data:(Current_loc.get ())
in
ci.cname <- newname;
ci.creferenced <- true;
@@ -2953,8 +2935,7 @@ let oneFilePass2 (f: file) =
end
end
end
- | GEnumTag (ei, l) as g -> begin
- CurrentLoc.set l;
+ | GEnumTag (ei, _) as g -> begin
incr currentDeclIdx;
if ei.ereferenced then
()
@@ -2968,7 +2949,7 @@ let oneFilePass2 (f: file) =
in
let newname, _ =
Alpha.newAlphaName ~alphaTable:eAlpha ~undolist:None
- ~lookupname:orig_name ~data:(CurrentLoc.get ())
+ ~lookupname:orig_name ~data:(Current_loc.get ())
in
ei.ename <- newname;
ei.ereferenced <- true;
@@ -2988,10 +2969,10 @@ let oneFilePass2 (f: file) =
()
end
end
- | GCompTagDecl (ci, l) -> begin
- CurrentLoc.set l; (* This is here just to introduce an undefined
- * structure. But maybe the structure was defined
- * already. *)
+ | GCompTagDecl (ci, _) -> begin
+ (* This is here just to introduce an undefined
+ * structure. But maybe the structure was defined
+ * already. *)
(* Do not increment currentDeclIdx because it is not incremented in
* pass 1*)
if H.mem emittedCompDecls ci.cname then
@@ -3003,16 +2984,14 @@ let oneFilePass2 (f: file) =
end
end
- | GEnumTagDecl (_ei, l) ->
- CurrentLoc.set l;
+ | GEnumTagDecl (_ei, _) ->
(* Do not increment currentDeclIdx because it is not incremented in
* pass 1*)
(* Keep it as a declaration *)
mergePushGlobal g
- | GType (ti, l) as g -> begin
- CurrentLoc.set l;
+ | GType (ti, _) as g -> begin
incr currentDeclIdx;
if ti.treferenced then
()
@@ -3023,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:(CurrentLoc.get ())
+ ~lookupname:ti.torig_name ~data:(Current_loc.get ())
in
ti.tname <- newname;
ti.treferenced <- true;
@@ -3033,8 +3012,7 @@ let oneFilePass2 (f: file) =
()
end
end
- | GAnnot (a, l) as g ->
- CurrentLoc.set l;
+ | GAnnot (a, _) as g ->
incr currentDeclIdx;
global_annot_pass2 g a
| g -> mergePushGlobals (visitCilGlobal renameVisitor g)
@@ -3103,6 +3081,7 @@ let merge_specs orig to_merge =
List.iter merge_one_spec to_merge
let global_merge_spec g =
+ let open Current_loc.Operators in
Kernel.debug ~dkey:Kernel.dkey_linker
"Merging global %a" Cil_printer.pp_global g;
let rename v spec =
@@ -3111,8 +3090,9 @@ let global_merge_spec g =
ignore (visitCilFunspec alpha spec)
with Not_found -> ()
in
+ let<> UpdatedCurrentLoc = Cil_datatype.Global.loc g in
match g with
- | GFun(fdec,loc) ->
+ | GFun(fdec, _) ->
Kernel.debug ~dkey:Kernel.dkey_linker
"Merging global definition %a" Cil_printer.pp_global g;
(match Cil_datatype.Varinfo.Hashtbl.find_opt spec_to_merge fdec.svar with
@@ -3130,11 +3110,10 @@ let global_merge_spec g =
specs;
Kernel.debug ~dkey:Kernel.dkey_linker
"Merging with %a" Cil_printer.pp_funspec fdec.sspec ;
- Cil.CurrentLoc.set loc;
rename fdec.svar fdec.sspec;
merge_specs fdec.sspec specs
)
- | GFunDecl(spec,v,loc) ->
+ | GFunDecl(spec, v, _) ->
Kernel.debug ~dkey:Kernel.dkey_linker
"Merging global declaration %a" Cil_printer.pp_global g;
(match Cil_datatype.Varinfo.Hashtbl.find_opt spec_to_merge v with
@@ -3157,7 +3136,6 @@ let global_merge_spec g =
List.iter (rename v) specs;
Kernel.debug ~dkey:Kernel.dkey_linker
"Renamed to %a" Cil_printer.pp_funspec spec;
- Cil.CurrentLoc.set loc;
merge_specs spec specs;
Kernel.debug ~dkey:Kernel.dkey_linker
"Merged into %a" Cil_printer.pp_funspec spec ;
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index 14e608a65c8d91c938fdcee8aea4103833077df3..190753ee6de26af4df7fc3fd4606223db5060b05 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -198,6 +198,7 @@ let encapsulate_local_vars f =
end
let oneret ?(callback: callback option) (f: fundec) : unit =
+ let open Current_loc.Operators in
let fname = f.svar.vname in
(* Get the return type *)
let retTyp =
@@ -341,7 +342,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
List.rev (s::acc)
| ({skind=Return (retval, loc)} as s) :: rests ->
- Cil.CurrentLoc.set loc;
+ let<> UpdatedCurrentLoc = loc in
(*
ignore (E.log "Fixing return(%a) at %a\n"
insert
@@ -493,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 b0ec828c38801bf80244443cb277776f1e883755..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 (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 99d340404d6171cd4b9e704637e1134382b75433..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 -> 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,17 +380,18 @@ 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 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<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc_skind stkind in
match stkind with
| (Instr _ | Return _ | Throw _) as keep ->
keep,labelled_stmt_tbl,calls_tbl
| Goto (stmt_ref, loc) -> Goto (ref !stmt_ref, loc),labelled_stmt_tbl,calls_tbl
| If (exp,bl1,bl2,loc) ->
- CurrentLoc.set loc;
let new_block1,labelled_stmt_tbl,calls_tbl =
copy_block labelled_stmt_tbl calls_tbl bl1
in
@@ -399,7 +400,6 @@ let copy_block kf switch_label_action break_continue_must_change bl =
in
If(exp,new_block1,new_block2,loc),labelled_stmt_tbl,calls_tbl
| Loop (a,bl,loc,_,_) ->
- CurrentLoc.set loc;
let new_block,labelled_stmt_tbl,calls_tbl =
copy_block
(* from now on break and continue can be kept *)
@@ -568,7 +568,9 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
id) in
ChangeDoChildrenPost (fundec, post_goto_updater)
- method! vstmt_aux s = match s.skind with
+ method! vstmt_aux s =
+ let open Current_loc.Operators in
+ match s.skind with
| Goto _ ->
gotos <- s::gotos; (* gotos that may need to be updated *)
DoChildren
@@ -622,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. *)
- CurrentLoc.set loc;
+ let<> UpdatedCurrentLoc = loc in
let break_lbl_stmt =
let break_label = fresh_label () in
let break_lbl_stmt = mkEmptyStmt () in
@@ -670,7 +672,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
Cil_datatype.Stmt.Hashtbl.add moved_labels sloop snew;
snew.labels <- sloop.labels;
sloop.labels <- [];
- snew;
+ snew
in
new_stmt
| _ -> assert false
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 495429175fba6d65763439b519f770e8cbd82a15..eb11a9658de4bed9ccd8704920547c42902d6a2e 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.CurrentLoc.get () in
+ let loc = Current_loc.get () in
Origin { kind; loc; id; }
let well = Well
@@ -153,13 +153,13 @@ let clear () = Id.reset (); History.clear ()
let is_current = function
| Unknown | Well -> false
- | Origin { loc } -> Cil_datatype.Location.equal loc (Cil.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. *)
let register_write bases t =
if is_unknown t then false else
- let current_loc = Cil.CurrentLoc.get () in
+ let current_loc = Current_loc.get () in
let is_new = not (History.mem t) in
let change (w, r, b) =
LocSet.add current_loc w, r, Base.SetLattice.join b bases
@@ -171,7 +171,7 @@ let register_write bases t =
(* Registers a read only if the current location is not that of the origin. *)
let register_read bases t =
if not (is_unknown t || is_current t) then
- let current_loc = Cil.CurrentLoc.get () in
+ let current_loc = Current_loc.get () in
let change (w, r, b) =
w, LocSet.add current_loc r, Base.SetLattice.join b bases
in
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index bb8cdc57192bd5ebf3e2932f41bbb66f10f855ad..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.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 b19f0472066216ea847fcf3fcb34a9bcacd47038..48b2d20a09bccdae01c9a3d0d0f6369194d41b1a 100644
--- a/src/kernel_services/analysis/dataflow2.ml
+++ b/src/kernel_services/analysis/dataflow2.ml
@@ -332,7 +332,8 @@ module Forwards(T : ForwardsTransfer) = struct
(** Process a statement *)
let processStmt worklist (s: stmt) : unit =
- CurrentLoc.set (Cil_datatype.Stmt.loc s);
+ 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;
@@ -356,12 +357,10 @@ module Forwards(T : ForwardsTransfer) = struct
List.iter (fun s' -> reachedStatement worklist s s' state) s.succs
in
- CurrentLoc.set (Cil_datatype.Stmt.loc s);
match s.skind with
| Instr i ->
- CurrentLoc.set (Cil_datatype.Instr.loc i);
- 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,12 +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 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 *)
- CurrentLoc.set (Cil_datatype.Stmt.loc s);
+ let<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc s in
let d: T.t =
match T.doStmt s with
Done d -> d
@@ -605,7 +605,7 @@ struct
match s.skind with
| Instr i ->
begin
- CurrentLoc.set (Cil_datatype.Instr.loc i);
+ 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 4b1a5a6433793beb88e1159d99df9c4c7a3f1556..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.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.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.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 72b33b6425c7a4a8eff13b0b37d721f60f1bd043..8f0dde149788ded2fd0598e40ecd1c358760b657 100644
--- a/src/kernel_services/analysis/dataflows.ml
+++ b/src/kernel_services/analysis/dataflows.ml
@@ -359,8 +359,6 @@ module type JOIN_SEMILATTICE = sig
end
-module CurrentLoc = Cil_const.CurrentLoc;;
-
(****************************************************************)
@@ -489,7 +487,6 @@ struct
let update_before (stmt, new_state) =
let ord = Fenv.to_ordered stmt in
- CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
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
@@ -504,14 +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 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;
- CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
+ 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 a4b8cee2cb9399811c91cc019f8038eea63a5304..7efadadef7645597e36bd50887242fa8836ec8fe 100644
--- a/src/kernel_services/analysis/stmts_graph.ml
+++ b/src/kernel_services/analysis/stmts_graph.ml
@@ -267,7 +267,6 @@ let rec get_block_stmts blk =
List.fold_left add Stmt.Set.empty blk.bstmts
and get_stmt_stmts s =
- let () = CurrentLoc.set (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
@@ -287,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 ef6d471b155acd4567379df9895081df24e9f4c4..a00dfdb4662fc5738fd63fb21504f599f8e3b96d 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -251,9 +251,11 @@ module Functions = struct
| _ -> kf.fundec <- fundec);
(* Kernel.feedback "UPDATE Spec of function %a (%a)"
Cil_datatype.Kf.pretty kf Printer.pp_funspec spec;*)
- (match fundec with
- | Definition(_,loc) | Declaration(_,_,_,loc) -> CurrentLoc.set loc);
- Logic_utils.merge_funspec ~oldloc kf.spec spec
+ let loc =
+ match fundec with Definition (_,loc) | Declaration (_,_,_,loc) -> loc
+ in
+ 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 e611e6cd33fc0aedf51735c54b961355f6fbdf11..b9de6911561698d1a951e2be6a7ae506f4002e59 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -351,10 +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 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 =
- Cil_const.CurrentLoc.set e.expr_loc;
+ let<> UpdatedCurrentLoc = e.expr_loc in
match e.expr_node with
NOTHING -> ()
| PAREN exp -> print_expression fmt exp
@@ -424,12 +425,13 @@ and print_for_init fmt fc =
| FC_DECL dec -> print_def fmt dec
and print_statement fmt stat =
+ let open Current_loc.Operators in
let loc = Cabshelper.get_statementloc stat in
- Cil_const.CurrentLoc.set loc;
+ 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
- NOP _ -> pp_print_string fmt ";"
+ | NOP _ -> pp_print_string fmt ";"
| COMPUTATION (exp,_) -> fprintf fmt "%a;" print_expression exp
| BLOCK (blk, _,_) -> print_block fmt blk
| SEQUENCE (s1, s2,_) ->
@@ -580,7 +582,8 @@ and print_defs fmt defs =
defs
and print_def fmt def =
- Cil_const.CurrentLoc.set (Cabshelper.get_definitionloc def);
+ 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 c25b28616c1630da8af6b913405f86babc1d7b08..0b407312c002d8a823f6676a417178926cca7a28 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -64,14 +64,10 @@ open Cil_types
functions below. *)
let check_invariants = false
-(* A reference to the current location *)
-module CurrentLoc = Cil_const.CurrentLoc
-let () = Log.set_current_source (fun () -> fst (CurrentLoc.get ()))
-
-let pp_thisloc fmt = Location.pretty fmt (CurrentLoc.get ())
+let pp_thisloc fmt = Location.pretty fmt (Current_loc.get ())
let abort_context msg =
- let loc = CurrentLoc.get () in
+ let loc = Current_loc.get () in
let append fmt =
Format.pp_print_newline fmt ();
Errorloc.pp_context_from_file fmt loc
@@ -1423,10 +1419,8 @@ let copy_logic_label is_copy l =
end else l
let rec visitCilTerm vis t =
- let oldloc = CurrentLoc.get () in
- CurrentLoc.set t.term_loc;
- let res = doVisitCil vis (fun x-> x) vis#vterm childrenTerm t in
- CurrentLoc.set oldloc; res
+ 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
@@ -2078,13 +2072,12 @@ and childrenModelInfo vis m =
else begin m.mi_attr <- mi_attr; m end
and visitCilModelInfo vis m =
- let oldloc = CurrentLoc.get () in
- CurrentLoc.set m.mi_decl;
+ 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
in
- CurrentLoc.set oldloc;
if m' != m then begin
(* reflect changes in the behavior tables for copy visitor. *)
Visitor_behavior.Set.model_info vis#behavior m m';
@@ -2093,11 +2086,8 @@ and visitCilModelInfo vis m =
m'
and visitCilAnnotation vis a =
- let oldloc = CurrentLoc.get () in
- CurrentLoc.set (Global_annotation.loc a);
- let res = doVisitCil vis id vis#vannotation childrenAnnotation a in
- CurrentLoc.set oldloc;
- res
+ Current_loc.with_loc (Global_annotation.loc a)
+ (doVisitCil vis id vis#vannotation childrenAnnotation) a
and childrenAnnotation vis a =
match a with
@@ -2208,10 +2198,9 @@ and childrenCodeAnnot vis ca =
else ca
and visitCilExpr (vis: cilVisitor) (e: exp) : exp =
- let oldLoc = CurrentLoc.get () in
- CurrentLoc.set e.eloc;
- let res = doVisitCil vis (Visitor_behavior.cexpr vis#behavior) vis#vexpr childrenExp e in
- CurrentLoc.set oldLoc; res
+ 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
@@ -2342,12 +2331,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 oldloc = CurrentLoc.get () in
- CurrentLoc.set (Cil_datatype.Instr.loc i);
- let res =
- doVisitListCil vis id vis#vinst childrenInstr i in
- CurrentLoc.set oldloc;
- res
+ 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
@@ -2410,31 +2395,26 @@ 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 oldloc = CurrentLoc.get () in
- CurrentLoc.set (Stmt.loc s) ;
+ 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 *)
let res =
doVisitCil vis
(Visitor_behavior.Memo.stmt vis#behavior) vis#vstmt (childrenStmt toPrepend) s in
- let ghost = res.ghost in
(* Now see if we have saved some instructions *)
toPrepend := !toPrepend @ vis#unqueueInstr ();
- (match !toPrepend with
- [] -> () (* Return the same statement *)
- | _ ->
- let b =
- mkBlockNonScoping
- ((List.map (fun i -> mkStmt ~ghost (Instr i)) !toPrepend)
- @ [mkStmt ~ghost res.skind])
- in
- b.battrs <- addAttribute (Attr (vis_tmp_attr, [])) b.battrs;
- (* Make our statement contain the instructions to prepend *)
- res.skind <- Block b);
- CurrentLoc.set oldloc;
- vis#pop_stmt s;
- res
+ match !toPrepend with
+ [] -> vis#pop_stmt s; res (* Return the same statement *)
+ | _ :: _ as instr_list ->
+ let make i = mkStmt ~ghost:res.ghost (Instr i) in
+ let last = mkStmt ~ghost:res.ghost res.skind in
+ let block = mkBlockNonScoping (List.map make instr_list @ [ last ]) in
+ block.battrs <- addAttribute (Attr (vis_tmp_attr, [])) block.battrs;
+ (* Make our statement contain the instructions to prepend *)
+ res.skind <- Block block;
+ vis#pop_stmt s; res
and childrenStmt (toPrepend: instr list ref) (vis:cilVisitor) (s:stmt): stmt =
let fExp e = (visitCilExpr vis e) in
@@ -2668,12 +2648,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 oldloc = CurrentLoc.get () in
- CurrentLoc.set v.vdecl;
- let res =
- doVisitCil vis (Visitor_behavior.Memo.varinfo vis#behavior)
- vis#vvdec childrenVarDecl v
- in CurrentLoc.set oldloc; res
+ 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
@@ -2876,12 +2853,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 oldloc = CurrentLoc.get () in
- CurrentLoc.set (Global.loc g) ;
- let res =
- doVisitListCil vis id vis#vglob childrenGlobal g in
- CurrentLoc.set oldloc;
- res
+ 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) ->
@@ -4983,8 +4956,7 @@ let compareConstant c1 c2 =
(* Iterate over all globals, including the global initializer *)
let iterGlobals (fl: file) (doone: global -> unit) : unit =
let doone' g =
- CurrentLoc.set (Global.loc g);
- doone g
+ Current_loc.with_loc (Global.loc g) doone g
in
List.iter doone' fl.globals;
match fl.globinit with
@@ -4994,8 +4966,7 @@ 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 doone' acc g =
- CurrentLoc.set (Global.loc g);
- 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
@@ -6858,7 +6829,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 = 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
@@ -7060,15 +7031,14 @@ let uniqueVarNames (f: file) : unit =
Hashtbl.add globalNames vi.vname vi.vid;
(* And register it *)
Alpha.registerAlphaName ~alphaTable:gAlphaTable
- ~lookupname:vi.vname ~data:(CurrentLoc.get ())
+ ~lookupname:vi.vname ~data:(Current_loc.get ())
end)
| _ -> ());
(* Now we must scan the function bodies and rename the locals *)
iterGlobals f
(function
- GFun(fdec, l) -> begin
- CurrentLoc.set l;
+ GFun(fdec, _) -> begin
(* Setup an undo list to be able to revert the changes to the
* global alpha table *)
let undolist = ref [] in
@@ -7079,7 +7049,7 @@ let uniqueVarNames (f: file) : unit =
let lookupname =
if v.vorig_name = "" then v.vname else v.vorig_name
in
- let data = 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 a57aac7d024644b8b33d52eb95e53582b2a03da8..aed2f84c7513a397e2e64affce3de2af76c96ac6 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2280,12 +2280,7 @@ val constFoldVisitor: bool -> cilVisitor
(** {2 Debugging support} *)
(* ************************************************************************* *)
-(** 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: State_builder.Ref with type data = location
-
-(** Pretty-print [(Cil.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 41ad002c8f3c36694caca652b57ee54f08b310b7..74176389529633084c020817c49adeda2c550253 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -43,15 +43,6 @@
open Cil_types
-module CurrentLoc =
- State_builder.Ref
- (Cil_datatype.Location)
- (struct
- let dependencies = []
- let name = "CurrentLoc"
- let default () = Cil_datatype.Location.unknown
- 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 ff5c455d9a7dd4af62a63aa59d3ad991ac3aef30..47f7659a34e8c63dfc10af4537b4a585c0974f09 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -46,9 +46,6 @@ open Cil_types
val voidType: typ
-(** forward reference to current location (see {!Cil.CurrentLoc})*)
-module CurrentLoc: State_builder.Ref with type data = location
-
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/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index e0ec107637898d4245ade58eff2fa24e337e131c..871b05809f5fec3455b2b9793486372047fa1637 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -242,6 +242,7 @@ module Stmt: sig
and type 'a map = 'a Hptmap.Shape(Stmt_Id).t
val self: State.t
end
+ val loc_skind: stmtkind -> location
val loc: t -> location
val pretty_sid: Format.formatter -> t -> unit
(** Pretty print the sid of the statement
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..c3c8dcbe115c7585068fab0375f7161982a2eac5
--- /dev/null
+++ b/src/kernel_services/ast_queries/current_loc.ml
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include State_builder.Ref
+ (Cil_datatype.Location)
+ (struct
+ let dependencies = []
+ let name = "Current_loc"
+ let default () = Cil_datatype.Location.unknown
+ end)
+
+let () = Log.set_current_source (fun () -> fst (get ()))
+
+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..824f0b08719284da1162565e6ccd77cd16abd328
--- /dev/null
+++ b/src/kernel_services/ast_queries/current_loc.mli
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** 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 [Current_loc.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 4e39e5d43042239d4f15fe6d499bc20c6df37ede..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
- (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
- (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 (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 (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 (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 (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 1eac2474cd76980f80c8a23c14fb9abb5533fc10..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 (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,8 +4099,9 @@ struct
| TDsyn typ -> LTsyn (plain_logic_type loc env typ)
let rec annot in_axiomatic a =
+ let open Current_loc.Operators in
let loc = a.decl_loc in
- Cil.CurrentLoc.set loc;
+ 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 976d4f69902446793d8abf72bb75bdb15cd283fb..cd74caa5993ca4a66e9c79f9fa9ec10fd9d103d1 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -96,12 +96,14 @@ let logicCType t =
in plain_or_set logicCType t
let plain_array_to_ptr ty =
+ 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 _ ->
+ | Some e ->
+ 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 2542d8938c1255addaca43f7014357a57a8ebe8a..cb75d926227697bc365f178a554ab56431e8b255 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -432,7 +432,8 @@ end = struct
new_locals
method! vcode_annot v =
- Option.iter Cil.CurrentLoc.set (Cil_datatype.Code_annotation.loc v);
+ 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/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 773ad748a0c8c9b56107bf18c0084644a9ac284a..8e8e2ab803457bdb2cd380f0d9b8947e776e19e4 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -598,16 +598,9 @@ let inliner curr_label inline =
}
let inline_term ~inline ?(current = BuiltinLabel Here) term =
- let current_loc = Cil_const.CurrentLoc.get () in
try Some (Visitor.visitFramacTerm (inliner current inline) term)
- with CannotInline ->
- (* The visitor changes and resets the reference to the current location.
- If an exception is raised during the visit, the current location must be
- reset by the caller. *)
- Cil_const.CurrentLoc.set current_loc;
- None
+ with CannotInline -> None
let inline_predicate ~inline ?(current = BuiltinLabel Here) pred =
- let current_loc = Cil_const.CurrentLoc.get () in
try Some (Visitor.visitFramacPredicate (inliner current inline) pred)
- with CannotInline -> Cil_const.CurrentLoc.set current_loc; None
+ with CannotInline -> None
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 cd08b5e4e508a32ccc9167ab19888309bdd9d8f9..357a69cd0979d5996008036ed5711af71f4b44da 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -82,14 +82,10 @@ end
class nopCabsVisitor : cabsVisitor = object
method vexpr (_e:expression) = DoChildren
method vinitexpr (_e:init_expression) = DoChildren
- method vstmt (s: statement) =
- CurrentLoc.set (get_statementloc s);
- DoChildren
+ method vstmt (_s: statement) = DoChildren
method vblock (_b: block) = DoChildren
method vvar (s: string) = s
- method vdef (d: definition) =
- CurrentLoc.set (get_definitionloc d);
- 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
@@ -233,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) ->
@@ -278,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 b44b715ecd4f3ee957426eb5dddf4fb77e1191f7..3214c3b5596c782eb65988eed90070d9015c7458 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -962,6 +962,8 @@ let filter_init_state restrict initial map acc =
with Not_found -> acc
let backward_analysis_aux stack kf ret_state =
+ 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 395295a390427ea1ae2f7abc419d173fab87871f..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:(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:(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/aorai/tests/ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
index ec532e726817a743ecc4be2a80e39ea3e94ebfbb..3d2eb83f556185e56f64e9b1f384528772864500 100644
--- a/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/monostate.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing monostate.i (no preprocessing)
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[aorai] monostate.i:10: Warning:
+[aorai] monostate.i:9: Warning:
Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing TMPDIR/aorai_monostate_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 7bf460e21c6454077bd009589977b7f54afdee22..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.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 ccaa156f127213cbb15761efade516299d97c848..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.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.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.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 3dbec883bfe28d2c7ae0cf87067016cef93b8dba..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.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.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 8d27b2165ccd45343b577631f9e19e2b9619aa24..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.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.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.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.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.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.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.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.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 38821921711bf9d9ecf94e36ebfdf7bca878ba89..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.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 c885230cc46982ff84f4f8b10026c54afff6859e..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.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 88c99208679080682094f369c6db18bd0e5283e9..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.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 14364066d2fa108a24be87f005c2e0a6bce40756..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.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 a606eac714e321bfa78df6709fd39685665b7439..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.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 7c8a63d15d27f4c32b2fa410cddd9d688cab5c23..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.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 de1a942094da8c318b35f1c24c9e6e110106842b..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.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.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 34a7b67ef1f8590dd7a6a5ea37dc447b8ca7104e..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.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.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 1aec39065f79ef1fcdf4165fe164b86098694e2d..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.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 faa20947665a0e49c570974ad724dd48108c30ae..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.CurrentLoc.get () in
+ let loc = Current_loc.get () in
let r =
try
ignore (Visitor.visitFramacCodeAnnotation vis ca);
false
with Exit -> true
in
- Cil.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.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 8741fe7ea42754bfae1230ba6ab801d53dbb2c57..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.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.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 9a063c21cea44ee5b54938be5b28d21a1fcf8f1b..fddf07d1882cdb193ed23f3dabcc0c1fb6686622 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -200,15 +200,11 @@ 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.CurrentLoc.set vi.vdecl;
(* Consider that local are initialized to a constant value *)
- From_memory.bind_var vi Eva.Deps.bottom acc
+ Current_loc.with_loc vi.vdecl
+ (From_memory.bind_var vi Eva.Deps.bottom) acc
in
- let loc = Cil.CurrentLoc.get () in
-
- let r = List.fold_left aux_local m b.blocals in
- Cil.CurrentLoc.set loc;
- r
+ List.fold_left aux_local m b.blocals
let unbind_locals m b =
let aux_local acc vi =
@@ -631,7 +627,8 @@ struct
compute_using_prototype_for_state state kf assigns
let compute_and_return kf =
- let call_site_loc = CurrentLoc.get () in
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Current_loc.get () in
From_parameters.feedback
"Computing for function %a%s"
Kernel_function.pretty kf
@@ -651,7 +648,6 @@ struct
From_parameters.feedback
"Done for function %a" Kernel_function.pretty kf;
Async.yield ();
- CurrentLoc.set call_site_loc;
result
let compute kf =
diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml
index 39811a30718a58cb83dd09d11109b6ddffb958b9..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.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.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 a234c7413cdbcc87b98a99f084aa0c271e2172ee..90481b13789fd6bfbcae4aeca2f6bbb738029a1d 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -361,7 +361,8 @@ module Store(* (B:sig *)
end
let mu (f:(t -> t)) (value,conds,stmt) =
- Cil.CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
+ let open Current_loc.Operators in
+ let<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc stmt in
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 da358e697703fddfc6fd79c918593dfc433726a8..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.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.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 e10d16d41c0a3c74a0b3efe9f2cba0b17a27aa4e..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.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.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 29708325fc01fe1491e081b383a2fbad776e0b9a..6cc50602a3d17d0d1cbcd473be79b56e646ac181 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -126,10 +126,11 @@ let register_modified_zones lmap stmt =
* @raise Kernel_function.No_Definition if [kf] has no definition
*)
let compute kf =
+ let open Current_loc.Operators in
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.CurrentLoc.set (Cil_datatype.Stmt.loc s);
+ let<> UpdatedCurrentLoc = Cil_datatype.Stmt.loc s in
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 7c7af57c0fb70de70acd47227954931fe5004fb7..7125d3e988e48332bbd990bdb07ed58f14bb5223 100644
--- a/src/plugins/wp/Context.ml
+++ b/src/plugins/wp/Context.ml
@@ -20,19 +20,6 @@
(* *)
(**************************************************************************)
-(* -------------------------------------------------------------------------- *)
-(* --- Location --- *)
-(* -------------------------------------------------------------------------- *)
-
-let with_current_loc loc phi x =
- let tmp = Cil_const.CurrentLoc.get () in
- try
- Cil_const.CurrentLoc.set loc ;
- let y = phi x in
- Cil_const.CurrentLoc.set tmp ; y
- with error ->
- Cil_const.CurrentLoc.set tmp ; raise error
-
(* -------------------------------------------------------------------------- *)
(* --- 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 ab494fb2497ada67372a7d7cccfd7ae5bfd734f5..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.CurrentLoc.get()));
+ | None -> raise (NonNaturalLoop (Current_loc.get()));
| Some pi -> pi
| exception Not_found ->
(* cut circularities *)
@@ -216,28 +216,21 @@ struct
(* Compute a stmt node *)
and stmt env a (s: stmt) : W.t_prop =
- let kl = Cil.CurrentLoc.get () in
- try
- Cil.CurrentLoc.set (Stmt.loc s) ;
- 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
- let do_assert env CfgAnnot.{ code_admitted ; code_verified } w =
- opt_fold (prove_property env) code_verified @@
- opt_fold (use_property env) code_admitted w
- in
- let probes = Probe.annotations s in
- let do_probe env (probe,term) =
- W.add_probe env.we ~stmt:s probe term in
- let pi =
- W.label env.we (Some s) (Clabels.stmt s) @@
- List.fold_right (do_probe env) probes @@
- List.fold_right (do_assert env) cas @@
- control env a s
- in
- Cil.CurrentLoc.set kl ; pi
- with err ->
- Cil.CurrentLoc.set kl ; raise err
+ 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
+ let do_assert env CfgAnnot.{ code_admitted ; code_verified } w =
+ opt_fold (prove_property env) code_verified @@
+ opt_fold (use_property env) code_admitted w
+ in
+ let probes = Probe.annotations s in
+ let do_probe env (probe,term) = W.add_probe env.we ~stmt:s probe term in
+ W.label env.we (Some s) (Clabels.stmt s) @@
+ List.fold_right (do_probe env) probes @@
+ List.fold_right (do_assert env) cas @@
+ control env a s
(* Branching wrt control-flow *)
and control env a s : W.t_prop =
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 653c64c01e79984f1d2e50dc82d0450bc349106d..9c922d48a981cdb2933f826d7729d1968a04f039 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -423,6 +423,8 @@ let loop_contract_pids kf stmt =
| _ -> []
let compile Key.{ kf ; smoking ; bhv ; prop } =
+ 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 07ebdf4cd43f28b86f25c4e8349682638d5d0426..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.CurrentLoc.get () in
- Cil.CurrentLoc.set var.vdecl ;
- let obj = W.init wenv var initinfo.init obj in
- Cil.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 ed8d44bafa9b41e21793538de8f5b97740f07e7f..1a9cdb55c93ad75e184f55c754b96cf284e48e2f 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -236,6 +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 Current_loc.Operators in
+ let<> UpdatedCurrentLoc = e.eloc in
match (Cil.constFold true e).enode with
| Const(CInt64(k,_,_)) ->
begin
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
index 5f4ee04ee6ffdd79f6143e2bcd7b2cbcd7c9bd36..868d4d0e33c65f43115fbe4a9f7106cac2f673d2 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing stmtcompiler_test.i (no preprocessing)
-[kernel:CERT:MSC:37] stmtcompiler_test.i:135: Warning:
+[kernel:CERT:MSC:37] stmtcompiler_test.i:142: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
[kernel:annot:missing-spec] stmtcompiler_test.i:103: Warning:
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.res.oracle
index edc3c3e8bd788ed5f4a240d6366891a8482ce2e2..121fcf34159bcace4dadf18afd22dac29854083c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing bigarray.c (with preprocessing)
-[kernel] bigarray.c:19: Warning:
+[kernel] bigarray.c:15: Warning:
Cannot represent length of array as an attribute
[wp] Running WP plugin...
[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
diff --git a/tests/cil/change_to_instr.ml b/tests/cil/change_to_instr.ml
index 85f19109e0f142708efddda38da2ef5813fffb8b..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.CurrentLoc.get()) ; i ]
+ Cil.ChangeTo [ Skip(Current_loc.get()) ; i ]
end
let run () =
diff --git a/tests/cil/oracle/bts297.res.oracle b/tests/cil/oracle/bts297.res.oracle
index 5fc89c0dd2dda67a2ccfcccaf525e50b20d48ed5..dd664411222826146e76a9badfdb3c5a3eeac885 100644
--- a/tests/cil/oracle/bts297.res.oracle
+++ b/tests/cil/oracle/bts297.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing bts297.c (with preprocessing)
-[kernel:CERT:MSC:37] bts297.c:4: Warning:
+[kernel:CERT:MSC:37] bts297.c:10: Warning:
Body of function abrupt falls-through. Adding a return statement
/* Generated by Frama-C */
int abrupt(int x)
diff --git a/tests/cil/queue_ghost_instr.ml b/tests/cil/queue_ghost_instr.ml
index 78dfc0eeb16cf32a9301bbb1cc595975da5b9c08..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.CurrentLoc.get())])
+ this#queueInstr([Skip(Current_loc.get())])
| _ -> ()
end ;
Cil.DoChildren
method! vinst _ =
let open Cil_types in
- this#queueInstr([Skip(Cil.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 c2248a4ebc119d082c215d70662ce313ab5fe2d4..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.CurrentLoc.get () in
+ let loc = Current_loc.get () in
add_assert loc (Option.get self#current_kf) stmt;
DoChildren
diff --git a/tests/misc/oracle/bts0452.res.oracle b/tests/misc/oracle/bts0452.res.oracle
index a954072f5cd6a74b22846cef82539cde84f1b323..9eb04c5c869d7e5639526aebec450390ee9b6da3 100644
--- a/tests/misc/oracle/bts0452.res.oracle
+++ b/tests/misc/oracle/bts0452.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing bts0452.i (no preprocessing)
-[kernel:CERT:MSC:37] bts0452.i:13: Warning:
+[kernel:CERT:MSC:37] bts0452.i:15: Warning:
Body of function f falls-through. Adding a return statement
-[kernel:CERT:MSC:37] bts0452.i:27: Warning:
+[kernel:CERT:MSC:37] bts0452.i:29: Warning:
Body of function h falls-through. Adding a return statement
diff --git a/tests/slicing/oracle/use_spec.0.res.oracle b/tests/slicing/oracle/use_spec.0.res.oracle
index 03163696bd5ddfb298785dce8b9645c62b36fe2b..ac13268d3f3b619039669269dca7e9f107595582 100644
--- a/tests/slicing/oracle/use_spec.0.res.oracle
+++ b/tests/slicing/oracle/use_spec.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing use_spec.i (no preprocessing)
-[kernel:CERT:MSC:37] use_spec.i:18: Warning:
+[kernel:CERT:MSC:37] use_spec.i:19: Warning:
Body of function f falls-through. Adding a return statement
[slicing] slicing requests in progress...
[eva] Analyzing a complete application starting at main
diff --git a/tests/slicing/oracle/use_spec.1.res.oracle b/tests/slicing/oracle/use_spec.1.res.oracle
index 4a1393123e19554421d78748b6751f1109942a4e..a31502ad99e2832eb3faabd36931f827124eb3f2 100644
--- a/tests/slicing/oracle/use_spec.1.res.oracle
+++ b/tests/slicing/oracle/use_spec.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing use_spec.i (no preprocessing)
-[kernel:CERT:MSC:37] use_spec.i:18: Warning:
+[kernel:CERT:MSC:37] use_spec.i:19: Warning:
Body of function f falls-through. Adding a return statement
[slicing] slicing requests in progress...
[eva] Analyzing a complete application starting at main2
diff --git a/tests/spec/oracle/annot_decl_bts1009.res.oracle b/tests/spec/oracle/annot_decl_bts1009.res.oracle
index 24b7d528817faf8c506b1b0619b23082306e79d8..52c967c7f828dcfe27b41a8862c4d9a4045d78fe 100644
--- a/tests/spec/oracle/annot_decl_bts1009.res.oracle
+++ b/tests/spec/oracle/annot_decl_bts1009.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing annot_decl_bts1009.i (no preprocessing)
-[kernel:annot-error] annot_decl_bts1009.i:5: Warning:
+[kernel:annot-error] annot_decl_bts1009.i:4: Warning:
Statement contract and ACSL pragmas over a local definition are not implemented. Ignoring annotation
/* Generated by Frama-C */
void f(void)
diff --git a/tests/syntax/ghost_cv_var_decl.ml b/tests/syntax/ghost_cv_var_decl.ml
index c278d32a902345b7364575590f67e3b9fcdd3c9f..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.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.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.CurrentLoc.get())
+ Cil_datatype.Location.pretty (Current_loc.get())
Cil_datatype.Varinfo.pretty v
ghost_status (Cil.var v) ;
Cil.DoChildren
diff --git a/tests/syntax/oracle/exit.res.oracle b/tests/syntax/oracle/exit.res.oracle
index 497136c44c5477f9adf7df0bf6afe5f6c2300dba..b1c0da8451dba83ec07bafa6d224454de4d17fef 100644
--- a/tests/syntax/oracle/exit.res.oracle
+++ b/tests/syntax/oracle/exit.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing exit.c (with preprocessing)
-[kernel:CERT:MSC:37] exit.c:16: Warning:
+[kernel:CERT:MSC:37] exit.c:21: Warning:
Body of function g falls-through. Adding a return statement
/* Generated by Frama-C */
#include "errno.h"
diff --git a/tests/syntax/oracle/inline_calls.0.res.oracle b/tests/syntax/oracle/inline_calls.0.res.oracle
index bae30a7ef5a11bb4af12f713e1150f946ec853f7..18da0e0c968c55fdbf22e7452c0f5d4c758bee6f 100644
--- a/tests/syntax/oracle/inline_calls.0.res.oracle
+++ b/tests/syntax/oracle/inline_calls.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing inline_calls.i (no preprocessing)
-[kernel:CERT:MSC:37] inline_calls.i:40: Warning:
+[kernel:CERT:MSC:37] inline_calls.i:43: Warning:
Body of function f1 falls-through. Adding a return statement
/* Generated by Frama-C */
int f(void)
diff --git a/tests/syntax/oracle/inline_calls.1.res.oracle b/tests/syntax/oracle/inline_calls.1.res.oracle
index 88333fa15d09fa47b3bdaa0243ba7fe31769aaa3..348ad3debfee0a5e49b9c024e5dd1c54a8304d08 100644
--- a/tests/syntax/oracle/inline_calls.1.res.oracle
+++ b/tests/syntax/oracle/inline_calls.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing inline_calls.i (no preprocessing)
-[kernel:CERT:MSC:37] inline_calls.i:40: Warning:
+[kernel:CERT:MSC:37] inline_calls.i:43: Warning:
Body of function f1 falls-through. Adding a return statement
/* Generated by Frama-C */
int f(void)
diff --git a/tests/syntax/oracle/inline_calls.2.res.oracle b/tests/syntax/oracle/inline_calls.2.res.oracle
index 288f587fc4ced8a89e18b78bfecf6f03a7e9a0cd..b621c0e9c33bfcb4ec5bff0caf5b703c58f082de 100644
--- a/tests/syntax/oracle/inline_calls.2.res.oracle
+++ b/tests/syntax/oracle/inline_calls.2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing inline_calls.i (no preprocessing)
-[kernel:CERT:MSC:37] inline_calls.i:40: Warning:
+[kernel:CERT:MSC:37] inline_calls.i:43: Warning:
Body of function f1 falls-through. Adding a return statement
/* Generated by Frama-C */
int f(void)
diff --git a/tests/syntax/oracle/one_ret_assert.res.oracle b/tests/syntax/oracle/one_ret_assert.res.oracle
index 96cf184dbb2786103bf326fbf029fbafd6add876..4f0a21cbe7d8e33e926d182a6aa88e7b741ea762 100644
--- a/tests/syntax/oracle/one_ret_assert.res.oracle
+++ b/tests/syntax/oracle/one_ret_assert.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing one_ret_assert.i (no preprocessing)
-[kernel:CERT:MSC:37] one_ret_assert.i:8: Warning:
+[kernel:CERT:MSC:37] one_ret_assert.i:9: Warning:
Body of function g falls-through. Adding a return statement
/* Generated by Frama-C */
int X;
diff --git a/tests/syntax/oracle/vla_switch.res.oracle b/tests/syntax/oracle/vla_switch.res.oracle
index 6b88253698403a3e87872419f16fb096da8c6559..5e4482172743410aeb94d7e518cc9675c428198c 100644
--- a/tests/syntax/oracle/vla_switch.res.oracle
+++ b/tests/syntax/oracle/vla_switch.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing vla_switch.i (no preprocessing)
-[kernel:CERT:MSC:37] vla_switch.i:16: Warning:
+[kernel:CERT:MSC:37] vla_switch.i:20: Warning:
Body of function case3 falls-through. Adding a return statement
[kernel] User Error: vla_switch.i:7, cannot jump from switch statement bypassing initialization of variable b, declared at vla_switch.i:9
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/imprecise_invalid_write.res.oracle b/tests/value/oracle/imprecise_invalid_write.res.oracle
index 7dabe5398d5293a332b7025fb2e6e1cc19738130..229134d6c791211c00349241044a3b4fe5bbc83f 100644
--- a/tests/value/oracle/imprecise_invalid_write.res.oracle
+++ b/tests/value/oracle/imprecise_invalid_write.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing imprecise_invalid_write.i (no preprocessing)
-[kernel:CERT:MSC:37] imprecise_invalid_write.i:5: Warning:
+[kernel:CERT:MSC:37] imprecise_invalid_write.i:6: Warning:
Body of function main1 falls-through. Adding a return statement
-[kernel:CERT:MSC:37] imprecise_invalid_write.i:10: Warning:
+[kernel:CERT:MSC:37] imprecise_invalid_write.i:11: Warning:
Body of function main2 falls-through. Adding a return statement
-[kernel:CERT:MSC:37] imprecise_invalid_write.i:17: Warning:
+[kernel:CERT:MSC:37] imprecise_invalid_write.i:18: Warning:
Body of function main3 falls-through. Adding a return statement
[eva] Analyzing a complete application starting at main
[eva] Computing initial state