From 796318fc46a78bde3822697a66e532aaf041f15a Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 2 Feb 2024 11:44:26 +0100
Subject: [PATCH] Use let<> instead of let*, add documentation
---
src/kernel_internals/typing/cabs2cil.ml | 24 ++++++++--------
src/kernel_internals/typing/cfg.ml | 2 +-
src/kernel_internals/typing/mergecil.ml | 10 +++----
src/kernel_internals/typing/oneret.ml | 2 +-
src/kernel_internals/typing/unroll_loops.ml | 4 +--
src/kernel_services/analysis/dataflow2.ml | 8 +++---
src/kernel_services/analysis/dataflows.ml | 4 +--
src/kernel_services/analysis/stmts_graph.ml | 2 +-
src/kernel_services/ast_data/globals.ml | 2 +-
src/kernel_services/ast_printing/cprint.ml | 6 ++--
src/kernel_services/ast_queries/cil.ml | 20 ++++++-------
src/kernel_services/ast_queries/cil_const.ml | 2 +-
src/kernel_services/ast_queries/cil_const.mli | 28 +++++++++++++++++--
.../ast_queries/logic_typing.ml | 2 +-
.../ast_queries/logic_utils.ml | 2 +-
.../ast_transformations/filter.ml | 2 +-
src/kernel_services/visitors/cabsvisit.ml | 4 +--
src/plugins/aorai/aorai_dataflow.ml | 2 +-
src/plugins/wp/cfgInfos.ml | 2 +-
src/plugins/wp/ctypes.ml | 2 +-
20 files changed, 78 insertions(+), 52 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index cd635b8e030..0484105bdd6 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -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 Cil_const.CurrentLoc.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 ->
@@ -2430,7 +2431,7 @@ class gatherLabelsClass : Cabsvisit.cabsVisitor = object (self)
method! vstmt s =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = get_statementloc s in
+ let<> CurrentLocUpdated = get_statementloc s in
(match s.stmt_node with
| LABEL (lbl,_,_) ->
(try
@@ -2955,7 +2956,8 @@ let rec setOneInit this o preinit =
match o with
| NoOffset -> assert false
| Index({enode = Const(CInt64(i,_,_));eloc}, off) ->
- CurrentLoc.set eloc;
+ let open Cil_const.CurrentLoc.Operators in
+ let<> UpdatedCurrentLoc = eloc in
to_integer i, off
| Field (f, off) ->
(* Find the index of the field *)
@@ -5410,7 +5412,7 @@ and doExp local_env
let ghost = local_env.is_ghost in
let loc = e.expr_loc in
(* will be reset at the end of the compilation of current expression. *)
- let* CurrentLocUpdated = loc in
+ let<> 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
@@ -8605,7 +8607,7 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
| None -> empty_funspec (), Cil_const.CurrentLoc.get ()
| Some (spec,loc) ->
begin
- let* CurrentLocUpdated = loc in
+ let<> CurrentLocUpdated = loc in
let loc = Cil_const.CurrentLoc.get () in
let res =
try
@@ -8632,7 +8634,7 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
(match logic_spec with
| None -> ()
| Some (spec,loc) ->
- let* CurrentLocUpdated = loc in
+ let<> CurrentLocUpdated = loc in
let merge_spec = function
| GFunDecl(old_spec, _, oldloc) ->
let behaviors =
@@ -9045,7 +9047,7 @@ and doAliasFun ghost vtype (thisname:string) (othername:string)
(* Do one declaration *)
and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = get_definitionloc def in
+ let<> CurrentLocUpdated = get_definitionloc def in
match def with
| Cabs.DECDEF (logic_spec, (s, nl), loc) ->
(* Do the specifiers exactly once *)
@@ -9367,7 +9369,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
begin
match spec with
| Some (spec,loc) ->
- let* CurrentLocUpdated = loc in
+ let<> CurrentLocUpdated = loc in
(try
!currentFunctionFDEC.sspec <-
Ltyping.funspec behaviors
@@ -9485,7 +9487,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
(* Now see whether we can fall through to the end of the function *)
if blockFallsThrough !currentFunctionFDEC.sbody then begin
let loc = endloc in
- let* CurrentLocUpdated = endloc in
+ let<> CurrentLocUpdated = endloc in
let protect_return,retval =
(* Guard the [return] instructions we add with an
[\assert \false]*)
@@ -9563,7 +9565,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
List.iter
(fun decl ->
let loc = convLoc decl.Logic_ptree.decl_loc in
- let* CurrentLocUpdated = loc in
+ let<> CurrentLocUpdated = loc in
try
let tdecl = Ltyping.annot decl in
let attr = fc_stdlib_attribute [] in
@@ -9851,7 +9853,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
in
let ghost = s.stmt_ghost in
let local_env = { local_env with is_ghost = ghost } in
- let* CurrentLocUpdated = convLoc (get_statementloc s) in
+ let<> CurrentLocUpdated = convLoc (get_statementloc s) in
match s.stmt_node with
| Cabs.NOP loc ->
{ empty
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index a083b65de20..59666e7574f 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -440,7 +440,7 @@ let xform_switch_block ?(keepSwitch=false) b =
[] -> []
| s :: rest ->
begin
- let* CurrentLocUpdated = Stmt.loc s in
+ 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 bd220141677..0f950a6eb62 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -867,7 +867,7 @@ let rec global_annot_without_irrelevant_attributes ga =
let rec global_annot_pass1 g =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Cil_datatype.Global_annotation.loc g in
+ let<> CurrentLocUpdated = Cil_datatype.Global_annotation.loc g in
match g with
| Dvolatile(hs,rvi,wvi,_,loc) ->
let process_term_kind (t,k as id) =
@@ -1709,7 +1709,7 @@ let oneFilePass1 (f:file) : unit =
newrep.ndata.vdecl <- newdecl
in
let iter g =
- let* CurrentLocUpdated = Cil_datatype.Global.loc g in
+ let<> CurrentLocUpdated = Cil_datatype.Global.loc g in
match g with
| GVarDecl (vi, l) | GVar (vi, _, l) | GFunDecl (_, vi, l)->
incr currentDeclIdx;
@@ -2195,7 +2195,7 @@ let renameInlinesVisitor = new renameInlineVisitorClass
let rec logic_annot_pass2 ~in_axiomatic g a =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Cil_datatype.Global_annotation.loc a in
+ let<> CurrentLocUpdated = Cil_datatype.Global_annotation.loc a in
match a with
| Dfun_or_pred (li, _) ->
begin
@@ -2605,7 +2605,7 @@ let oneFilePass2 (f: file) =
end
end
in
- let* CurrentLocUpdated = Cil_datatype.Global.loc g in
+ let<> CurrentLocUpdated = Cil_datatype.Global.loc g in
match g with
| GVarDecl (vi, l) as g ->
incr currentDeclIdx;
@@ -3090,7 +3090,7 @@ let global_merge_spec g =
ignore (visitCilFunspec alpha spec)
with Not_found -> ()
in
- let* CurrentLocUpdated = Cil_datatype.Global.loc g in
+ let<> CurrentLocUpdated = Cil_datatype.Global.loc g in
match g with
| GFun(fdec, _) ->
Kernel.debug ~dkey:Kernel.dkey_linker
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index a70e226a5a1..2a6089b41dc 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -342,7 +342,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
List.rev (s::acc)
| ({skind=Return (retval, loc)} as s) :: rests ->
- let* CurrentLocUpdated = loc in
+ let<> 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 52ba428e53f..7b091cdb3ce 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -386,7 +386,7 @@ let copy_block kf switch_label_action break_continue_must_change bl =
?(break_continue_must_change = break_continue_must_change) =
copy_block ~switch_label_action ~break_continue_must_change
in
- let* CurrentLocUpdated = Cil_datatype.Stmt.loc_skind stkind in
+ let<> CurrentLocUpdated = Cil_datatype.Stmt.loc_skind stkind in
match stkind with
| (Instr _ | Return _ | Throw _) as keep ->
keep,labelled_stmt_tbl,calls_tbl
@@ -624,7 +624,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
goes into the remaining loop. *)
(* TODO: transforms loop annotations into statement contracts
inside the unrolled parts. *)
- let* CurrentLocUpdated = loc in
+ let<> CurrentLocUpdated = loc in
let break_lbl_stmt =
let break_label = fresh_label () in
let break_lbl_stmt = mkEmptyStmt () in
diff --git a/src/kernel_services/analysis/dataflow2.ml b/src/kernel_services/analysis/dataflow2.ml
index 78cbdedb0df..30f3adc5485 100644
--- a/src/kernel_services/analysis/dataflow2.ml
+++ b/src/kernel_services/analysis/dataflow2.ml
@@ -333,7 +333,7 @@ module Forwards(T : ForwardsTransfer) = struct
(** Process a statement *)
let processStmt worklist (s: stmt) : unit =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Cil_datatype.Stmt.loc s in
+ let<> 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;
@@ -359,7 +359,7 @@ module Forwards(T : ForwardsTransfer) = struct
match s.skind with
| Instr i ->
- let* CurrentLocUpdated = Cil_datatype.Instr.loc i in
+ let<> CurrentLocUpdated = Cil_datatype.Instr.loc i in
let after = T.doInstr s i curr in
do_succs after
@@ -582,7 +582,7 @@ struct
(* Find the state before the branch *)
- let* CurrentLocUpdated = Cil_datatype.Stmt.loc s in
+ let<> CurrentLocUpdated = Cil_datatype.Stmt.loc s in
let d: T.t =
match T.doStmt s with
Done d -> d
@@ -606,7 +606,7 @@ struct
match s.skind with
| Instr i ->
begin
- let* CurrentLocUpdated = Cil_datatype.Instr.loc i in
+ 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 147962023fc..44484e0142e 100644
--- a/src/kernel_services/analysis/dataflows.ml
+++ b/src/kernel_services/analysis/dataflows.ml
@@ -488,7 +488,7 @@ struct
let update_before (stmt, new_state) =
let open Cil_const.CurrentLoc.Operators in
let ord = Fenv.to_ordered stmt in
- let* CurrentLocUpdated = Cil_datatype.Stmt.loc stmt in
+ let<> 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
@@ -511,7 +511,7 @@ struct
let cur_state = P.get_before ord in
let stmt = Fenv.to_stmt ord in
Kernel.debug ~dkey:Kernel.dkey_dataflow "forward: doing stmt %d" stmt.sid;
- let* CurrentLocUpdated = Cil_datatype.Stmt.loc stmt in
+ let<> 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 7da1516e121..14a22f00e8e 100644
--- a/src/kernel_services/analysis/stmts_graph.ml
+++ b/src/kernel_services/analysis/stmts_graph.ml
@@ -268,7 +268,7 @@ let rec get_block_stmts blk =
and get_stmt_stmts s =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Cil_datatype.Stmt.loc s 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 0ec59170bb7..6e2dc297939 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -255,7 +255,7 @@ module Functions = struct
let loc =
match fundec with Definition (_,loc) | Declaration (_,_,_,loc) -> loc
in
- let* CurrentLocUpdated = 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 6c7d0ff3f4e..adadf1c5e63 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -355,7 +355,7 @@ and print_expression_level (lvl: int) fmt (exp : expression) =
let (txt, lvl') = get_operator exp in
let print_expression fmt exp = print_expression_level lvl' fmt exp in
let print_exp fmt e =
- let* CurrentLocUpdated = e.expr_loc in
+ let<> CurrentLocUpdated = e.expr_loc in
match e.expr_node with
NOTHING -> ()
| PAREN exp -> print_expression fmt exp
@@ -427,7 +427,7 @@ and print_for_init fmt fc =
and print_statement fmt stat =
let open Cil_const.CurrentLoc.Operators in
let loc = Cabshelper.get_statementloc stat in
- let* CurrentLocUpdated = loc in
+ 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
@@ -583,7 +583,7 @@ and print_defs fmt defs =
and print_def fmt def =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Cabshelper.get_definitionloc def 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 0f19d21e7a6..6f7f08daa4d 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1422,7 +1422,7 @@ let copy_logic_label is_copy l =
let rec visitCilTerm vis t =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = t.term_loc in
+ let<> CurrentLocUpdated = t.term_loc in
doVisitCil vis (fun x-> x) vis#vterm childrenTerm t
and childrenTerm vis t =
@@ -2076,7 +2076,7 @@ and childrenModelInfo vis m =
and visitCilModelInfo vis m =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = m.mi_decl in
+ let<> CurrentLocUpdated = m.mi_decl in
let m' =
doVisitCil
vis (Visitor_behavior.Memo.model_info vis#behavior) vis#vmodel_info childrenModelInfo m
@@ -2090,7 +2090,7 @@ and visitCilModelInfo vis m =
and visitCilAnnotation vis a =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Global_annotation.loc a in
+ let<> CurrentLocUpdated = Global_annotation.loc a in
doVisitCil vis id vis#vannotation childrenAnnotation a
and childrenAnnotation vis a =
@@ -2203,7 +2203,7 @@ and childrenCodeAnnot vis ca =
and visitCilExpr (vis: cilVisitor) (e: exp) : exp =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = e.eloc in
+ let<> CurrentLocUpdated = e.eloc in
doVisitCil vis (Visitor_behavior.cexpr vis#behavior) vis#vexpr childrenExp e
and childrenExp (vis: cilVisitor) (e: exp) : exp =
@@ -2336,7 +2336,7 @@ and childrenLocal_init vi (vis: cilVisitor) li =
and visitCilInstr (vis: cilVisitor) (i: instr) : instr list =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Cil_datatype.Instr.loc i in
+ let<> CurrentLocUpdated = Cil_datatype.Instr.loc i in
doVisitListCil vis id vis#vinst childrenInstr i
and childrenInstr (vis: cilVisitor) (i: instr) : instr =
@@ -2401,7 +2401,7 @@ and childrenInstr (vis: cilVisitor) (i: instr) : instr =
(* visit all nodes in a Cil statement tree in preorder *)
and visitCilStmt (vis:cilVisitor) (s: stmt) : stmt =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Cil_datatype.Stmt.loc s in
+ let<> 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 *)
@@ -2654,7 +2654,7 @@ and childrenType (vis : cilVisitor) (t : typ) : typ =
(* we just visit the varinfo node *)
and visitCilVarDecl (vis : cilVisitor) (v : varinfo) : varinfo =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = v.vdecl in
+ let<> CurrentLocUpdated = v.vdecl in
doVisitCil vis (Visitor_behavior.Memo.varinfo vis#behavior)
vis#vvdec childrenVarDecl v
@@ -2860,7 +2860,7 @@ let visitCilEnumInfo vis e =
let rec visitCilGlobal (vis: cilVisitor) (g: global) : global list =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Global.loc g in
+ let<> CurrentLocUpdated = Global.loc g in
doVisitListCil vis id vis#vglob childrenGlobal g
and childrenGlobal (vis: cilVisitor) (g: global) : global =
match g with
@@ -4964,7 +4964,7 @@ let compareConstant c1 c2 =
let iterGlobals (fl: file) (doone: global -> unit) : unit =
let open Cil_const.CurrentLoc.Operators in
let doone' g =
- let* CurrentLocUpdated = Global.loc g in
+ let<> CurrentLocUpdated = Global.loc g in
doone g
in
List.iter doone' fl.globals;
@@ -4976,7 +4976,7 @@ let iterGlobals (fl: file) (doone: global -> unit) : unit =
let foldGlobals (fl: file) (doone: 'a -> global -> 'a) (acc: 'a) : 'a =
let open Cil_const.CurrentLoc.Operators in
let doone' acc g =
- let* CurrentLocUpdated = Global.loc g in
+ let<> CurrentLocUpdated = Global.loc g in
doone acc g
in
let acc' = List.fold_left doone' acc fl.globals in
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index 3e0dc923d43..5620c04bbff 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -58,7 +58,7 @@ module CurrentLoc = struct
let from_option opt =
Option.value ~default:(get ()) opt
- let ( let* ) loc f =
+ let ( let<> ) loc f =
let oldLoc = get () in
let finally () = set oldLoc in
let work () = set loc; f CurrentLocUpdated in
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index 29048062c9e..b13af1036f0 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -48,13 +48,37 @@ val voidType: typ
(** A reference to the current location. If you are careful to set this to
the current location then you can use some built-in logging functions that
- will print the location. *)
+ will print the location.
+*)
module CurrentLoc: sig
include State_builder.Ref with type data = location
module Operators : sig
+
+ (** [CurrentLocUpdated] is a simple constructor which can be used as
+ documentation : [let<> CurrentLocUpdated = loc in ...] or replaced with
+ [_]
+ *)
type operation = CurrentLocUpdated
+
+ (** Utils function, [from_option opt] will return [l] if [opt] is [Some l]
+ and [CurrentLoc.get ()] if it is [None].
+ *)
val from_option : data option -> data
- val ( let* ) : data -> (operation -> 'a) -> 'a
+
+ (**
+ [let<> _ = loc in ...] can be used to mimic the behavior obtained with
+ [
+ let oldloc = CurrentLoc.get () in
+ try
+ CurrentLoc.set loc;
+ let res = ... in
+ CurrentLoc.set oldloc;
+ res
+ with exn -> CurrentLoc.set oldloc; raise exn
+ ].
+ [let<>] syntax requires to open [CurrentLoc.Operators].
+ *)
+ val ( let<> ) : data -> (operation -> 'a) -> 'a
end
end
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 955e92833e0..9ef42c4aab5 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -4101,7 +4101,7 @@ struct
let rec annot in_axiomatic a =
let open Cil_const.CurrentLoc.Operators in
let loc = a.decl_loc in
- let* CurrentLocUpdated = loc in
+ 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_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index a16e6432ea8..5a36ce4b6a8 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -103,7 +103,7 @@ let plain_array_to_ptr ty =
match lo with
| None -> []
| Some e ->
- let* CurrentLocUpdated = e.eloc in
+ let<> CurrentLocUpdated = 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 7e5582543c7..df3d6806689 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -434,7 +434,7 @@ end = struct
method! vcode_annot v =
let open Cil_const.CurrentLoc.Operators in
let loc_opt = Cil_datatype.Code_annotation.loc v in
- let* CurrentLocUpdated = from_option loc_opt in
+ let<> 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/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index 78ea03e24a6..de08ffaffe9 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -84,13 +84,13 @@ class nopCabsVisitor : cabsVisitor = object
method vinitexpr (_e:init_expression) = DoChildren
method vstmt (s: statement) =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = get_statementloc s in
+ let<> CurrentLocUpdated = get_statementloc s in
DoChildren
method vblock (_b: block) = DoChildren
method vvar (s: string) = s
method vdef (d: definition) =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = get_definitionloc d in
+ let<> CurrentLocUpdated = get_definitionloc d in
DoChildren
method vtypespec (_ts: typeSpecifier) = DoChildren
method vdecltype (_dt: decl_type) = DoChildren
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index b569d4c464a..2e6c599f820 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -963,7 +963,7 @@ let filter_init_state restrict initial map acc =
let backward_analysis_aux stack kf ret_state =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Kernel_function.get_location kf in
+ let<> CurrentLocUpdated = 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/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 031337e2cc9..c8f382f35fc 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -424,7 +424,7 @@ let loop_contract_pids kf stmt =
let compile Key.{ kf ; smoking ; bhv ; prop } =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = Kernel_function.get_location kf in
+ let<> CurrentLocUpdated = 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/ctypes.ml b/src/plugins/wp/ctypes.ml
index 00b1c4c922c..f69fa373646 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -237,7 +237,7 @@ let char c = Integer.to_int64_exn (Cil.charConstToInt c)
let constant e =
let open Cil_const.CurrentLoc.Operators in
- let* CurrentLocUpdated = e.eloc in
+ let<> CurrentLocUpdated = e.eloc in
match (Cil.constFold true e).enode with
| Const(CInt64(k,_,_)) ->
begin
--
GitLab