diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 613d5ee148de1b13ebb7fb05591c2b75dff9b1a7..db87d8e403909537189631ed70c4d267f5975de2 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2429,7 +2429,8 @@ class gatherLabelsClass : Cabsvisit.cabsVisitor = object (self)
ChangeDoChildrenPost (blk, fun _ -> (self#removeLocalLabels blk; blk))
method! vstmt s =
- CurrentLoc.set (get_statementloc s);
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = get_statementloc s in
(match s.stmt_node with
| LABEL (lbl,_,_) ->
(try
@@ -5405,11 +5406,11 @@ and doExp local_env
(e: Cabs.expression)
(what: expAction)
=
+ let open Cil_const.CurrentLoc.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* CurrentLocUpdated = 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
@@ -7446,7 +7447,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 =
@@ -8458,6 +8458,7 @@ and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
* varinfo *)
and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * Cabs.attribute list))
(((n,ndt,a,cloc), inite) : Cabs.init_name) : varinfo =
+ let open Cil_const.CurrentLoc.Operators in
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
@@ -8599,24 +8600,28 @@ 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 (), Cil_const.CurrentLoc.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* CurrentLocUpdated = loc in
+ let loc = Cil_const.CurrentLoc.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 ()));
@@ -8627,7 +8632,7 @@ 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* CurrentLocUpdated = loc in
let merge_spec = function
| GFunDecl(old_spec, _, oldloc) ->
let behaviors =
@@ -9038,10 +9043,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 Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = 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
@@ -9101,18 +9107,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, Cil_const.CurrentLoc.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'' =
@@ -9134,8 +9138,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
| _ -> 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 +9165,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 +9188,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 *)
@@ -9347,10 +9348,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* CurrentLocUpdated = loc in
(try
!currentFunctionFDEC.sspec <-
Ltyping.funspec behaviors
@@ -9360,22 +9377,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 _ =
@@ -9537,8 +9541,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 +9562,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* CurrentLocUpdated = loc in
try
let tdecl = Ltyping.annot decl in
let attr = fc_stdlib_attribute [] in
@@ -9832,6 +9835,7 @@ and doBodyScope local_env blk =
enterScope (); let res = doBody local_env blk in exitScope (); res
and doStatement local_env (s : Cabs.statement) : chunk =
+ let open Cil_const.CurrentLoc.Operators in
let mk_loop_annot a loc =
try
List.map
@@ -9845,12 +9849,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* CurrentLocUpdated = 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 +9877,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 +9889,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 +9906,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 +9915,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 +9945,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 +9958,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 +9980,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 +9996,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 +10014,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 +10026,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 +10041,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 +10064,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 +10077,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 +10135,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 +10186,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 +10194,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..a083b65de20bfc977f541e5844bfcdfc5a33d346 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 Cil_const.CurrentLoc.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* CurrentLocUpdated = 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/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index ebfddbe38cf7c713ae56f44d57c075a73e07c962..62d502e6773630768e9037aefcc8f5ac54846b36 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 Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = 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 Cil_const.CurrentLoc.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 ;
@@ -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* CurrentLocUpdated = 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) =
@@ -2619,9 +2611,9 @@ let oneFilePass2 (f: file) =
end
end
in
+ let* CurrentLocUpdated = 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 +2623,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 +2644,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 +2683,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 +2897,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
()
@@ -2953,8 +2941,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
()
@@ -2988,10 +2975,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 +2990,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
()
@@ -3033,8 +3018,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 +3087,7 @@ let merge_specs orig to_merge =
List.iter merge_one_spec to_merge
let global_merge_spec g =
+ let open Cil_const.CurrentLoc.Operators in
Kernel.debug ~dkey:Kernel.dkey_linker
"Merging global %a" Cil_printer.pp_global g;
let rename v spec =
@@ -3111,8 +3096,9 @@ let global_merge_spec g =
ignore (visitCilFunspec alpha spec)
with Not_found -> ()
in
+ let* CurrentLocUpdated = 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 +3116,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 +3142,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..a70e226a5a11ca16b95d25f524e3cfc401d359c9 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 Cil_const.CurrentLoc.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* CurrentLocUpdated = loc in
(*
ignore (E.log "Fixing return(%a) at %a\n"
insert
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 99d340404d6171cd4b9e704637e1134382b75433..5920ecb4cb17bd2e94a4f21224db35bbe732cae2 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -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 Cil_const.CurrentLoc.Operators in
let copy_block
?(switch_label_action = switch_label_action)
?(break_continue_must_change = break_continue_must_change) =
copy_block ~switch_label_action ~break_continue_must_change
in
+ let* CurrentLocUpdated = Cil_datatype.Stmt.loc_skind stkind in
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 Cil_const.CurrentLoc.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* CurrentLocUpdated = 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/analysis/dataflow2.ml b/src/kernel_services/analysis/dataflow2.ml
index b19f0472066216ea847fcf3fcb34a9bcacd47038..78cbdedb0df40ea7d7f60900cba3f0e34e0b9d9b 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 Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = 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,10 +357,9 @@ 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* CurrentLocUpdated = Cil_datatype.Instr.loc i in
let after = T.doInstr s i curr in
do_succs after
@@ -576,12 +576,13 @@ struct
(** Process a statement and return true if the set of live return
* addresses on its entry has changed. *)
let processStmt (s: stmt) : bool =
+ let open Cil_const.CurrentLoc.Operators in
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* CurrentLocUpdated = Cil_datatype.Stmt.loc s in
let d: T.t =
match T.doStmt s with
Done d -> d
@@ -605,7 +606,7 @@ struct
match s.skind with
| Instr i ->
begin
- CurrentLoc.set (Cil_datatype.Instr.loc i);
+ let* CurrentLocUpdated = 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/dataflows.ml b/src/kernel_services/analysis/dataflows.ml
index 72b33b6425c7a4a8eff13b0b37d721f60f1bd043..147962023fcdf1673b64c454cc6542724045a6fa 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;;
-
(****************************************************************)
@@ -488,8 +486,9 @@ struct
W.insert ord) P.init;;
let update_before (stmt, new_state) =
+ let open Cil_const.CurrentLoc.Operators in
let ord = Fenv.to_ordered stmt in
- CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
+ let* CurrentLocUpdated = Cil_datatype.Stmt.loc stmt in
let join =
(* If we know that we already have to recompute before.(ord), we
can omit the inclusion testing, and only perform the join. The
@@ -508,10 +507,11 @@ struct
;;
let do_stmt ord =
+ let open Cil_const.CurrentLoc.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* CurrentLocUpdated = 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..7da1516e1217d251c397864fd4baa9d489c91944 100644
--- a/src/kernel_services/analysis/stmts_graph.ml
+++ b/src/kernel_services/analysis/stmts_graph.ml
@@ -267,7 +267,8 @@ 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 open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = Cil_datatype.Stmt.loc s in
let compute_stmt_stmts s = match s.skind with
| Instr _ | Return _ | Throw _ -> Stmt.Set.singleton s
| Continue _ | Break _ | Goto _ -> Stmt.Set.singleton s
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index ef6d471b155acd4567379df9895081df24e9f4c4..0ec59170bb7ae6008c35b6bb242aee9a4f7ebd91 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -241,6 +241,7 @@ module Functions = struct
update_orig_name kf; kf)
let update_kf kf fundec spec =
+ let open Cil_const.CurrentLoc.Operators in
let oldloc = get_location kf in
(match kf.fundec, fundec with
(* we never update a definition with a declaration (see bug 1914).
@@ -251,8 +252,10 @@ 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);
+ let loc =
+ match fundec with Definition (_,loc) | Declaration (_,_,_,loc) -> loc
+ in
+ let* CurrentLocUpdated = loc in
Logic_utils.merge_funspec ~oldloc kf.spec spec
let replace_by_declaration s v l=
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index e611e6cd33fc0aedf51735c54b961355f6fbdf11..6c7d0ff3f4e319561deb81c455946c64e46ffb7a 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 Cil_const.CurrentLoc.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* CurrentLocUpdated = 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 Cil_const.CurrentLoc.Operators in
let loc = Cabshelper.get_statementloc stat in
- Cil_const.CurrentLoc.set loc;
+ let* CurrentLocUpdated = 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 Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = 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..229b1eeb4422bf7dad6b1d1a4724732d101d4cc9 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1423,10 +1423,9 @@ 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
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = t.term_loc in
+ doVisitCil vis (fun x-> x) vis#vterm childrenTerm t
and childrenTerm vis t =
let tn' = visitCilTermNode vis t.term_node in
@@ -2078,13 +2077,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 Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = 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 +2091,9 @@ 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
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = Global_annotation.loc a in
+ doVisitCil vis id vis#vannotation childrenAnnotation a
and childrenAnnotation vis a =
match a with
@@ -2208,10 +2204,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
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = e.eloc in
+ 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 +2337,9 @@ 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
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = Cil_datatype.Instr.loc i in
+ doVisitListCil vis id vis#vinst childrenInstr i
and childrenInstr (vis: cilVisitor) (i: instr) : instr =
let fExp = visitCilExpr vis in
@@ -2410,31 +2402,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 Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = 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 +2655,10 @@ 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
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = v.vdecl in
+ 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 +2861,9 @@ 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
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = Global.loc g in
+ doVisitListCil vis id vis#vglob childrenGlobal g
and childrenGlobal (vis: cilVisitor) (g: global) : global =
match g with
| GFun (f, l) ->
@@ -4982,8 +4964,9 @@ let compareConstant c1 c2 =
(* Iterate over all globals, including the global initializer *)
let iterGlobals (fl: file) (doone: global -> unit) : unit =
+ let open Cil_const.CurrentLoc.Operators in
let doone' g =
- CurrentLoc.set (Global.loc g);
+ let* CurrentLocUpdated = Global.loc g in
doone g
in
List.iter doone' fl.globals;
@@ -4993,8 +4976,9 @@ let iterGlobals (fl: file) (doone: global -> unit) : unit =
(* Fold over all globals, including the global initializer *)
let foldGlobals (fl: file) (doone: 'a -> global -> 'a) (acc: 'a) : 'a =
+ let open Cil_const.CurrentLoc.Operators in
let doone' acc g =
- CurrentLoc.set (Global.loc g);
+ let* CurrentLocUpdated = Global.loc g in
doone acc g
in
let acc' = List.fold_left doone' acc fl.globals in
@@ -7067,8 +7051,7 @@ let uniqueVarNames (f: file) : unit =
(* 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
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index 41ad002c8f3c36694caca652b57ee54f08b310b7..3e0dc923d435b3903acea56a0639660ff2540de6 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -43,14 +43,29 @@
open Cil_types
-module CurrentLoc =
- State_builder.Ref
- (Cil_datatype.Location)
- (struct
- let dependencies = []
- let name = "CurrentLoc"
- let default () = Cil_datatype.Location.unknown
- end)
+module CurrentLoc = struct
+ include
+ State_builder.Ref
+ (Cil_datatype.Location)
+ (struct
+ let dependencies = []
+ let name = "CurrentLoc"
+ let default () = Cil_datatype.Location.unknown
+ end)
+ module Operators = struct
+ type operation = CurrentLocUpdated
+
+ let from_option opt =
+ Option.value ~default:(get ()) opt
+
+ let ( let* ) loc f =
+ let oldLoc = get () in
+ let finally () = set oldLoc in
+ let work () = set loc; f CurrentLocUpdated in
+ Fun.protect ~finally work
+ end
+
+end
let voidType = TVoid([])
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index ff5c455d9a7dd4af62a63aa59d3ad991ac3aef30..f19a87d7be8693be87fd5a6ee778a5f0d7c7c26e 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -47,7 +47,14 @@ open Cil_types
val voidType: typ
(** forward reference to current location (see {!Cil.CurrentLoc})*)
-module CurrentLoc: State_builder.Ref with type data = location
+module CurrentLoc: sig
+ include State_builder.Ref with type data = location
+ module Operators : sig
+ type operation = CurrentLocUpdated
+ val from_option : data option -> data
+ val ( let* ) : data -> (operation -> 'a) -> 'a
+ end
+end
module Vid: sig val next: unit -> int end
module Sid: 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/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 1eac2474cd76980f80c8a23c14fb9abb5533fc10..4b134221b8853bf5a0e3f5fbb48c259c710374ce 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -4099,8 +4099,9 @@ struct
| TDsyn typ -> LTsyn (plain_logic_type loc env typ)
let rec annot in_axiomatic a =
+ let open Cil_const.CurrentLoc.Operators in
let loc = a.decl_loc in
- Cil.CurrentLoc.set loc;
+ let* CurrentLocUpdated = 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_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index 2542d8938c1255addaca43f7014357a57a8ebe8a..7e5582543c74ed401aba71189d82d3a6e7d94678 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -432,7 +432,9 @@ end = struct
new_locals
method! vcode_annot v =
- Option.iter Cil.CurrentLoc.set (Cil_datatype.Code_annotation.loc v);
+ let open Cil_const.CurrentLoc.Operators in
+ let loc_opt = Cil_datatype.Code_annotation.loc v in
+ let* CurrentLocUpdated = from_option loc_opt in
let 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/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index cd08b5e4e508a32ccc9167ab19888309bdd9d8f9..78ea03e24a62f61b1c3d2065b8fdf388f1a68038 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -83,12 +83,14 @@ class nopCabsVisitor : cabsVisitor = object
method vexpr (_e:expression) = DoChildren
method vinitexpr (_e:init_expression) = DoChildren
method vstmt (s: statement) =
- CurrentLoc.set (get_statementloc s);
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = get_statementloc s in
DoChildren
method vblock (_b: block) = DoChildren
method vvar (s: string) = s
method vdef (d: definition) =
- CurrentLoc.set (get_definitionloc d);
+ let open Cil_const.CurrentLoc.Operators in
+ let* CurrentLocUpdated = get_definitionloc d in
DoChildren
method vtypespec (_ts: typeSpecifier) = DoChildren
method vdecltype (_dt: decl_type) = DoChildren