diff --git a/src/analyses/base.ml b/src/analyses/base.ml index ab0d61a874..c842d6dce1 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -274,7 +274,7 @@ struct let rec addToOffset n (t:typ option) = function | `Index (i, `NoOffset) -> (* Binary operations on pointer types should not generate warnings in SV-COMP *) - GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> + let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in (* If we have arrived at the last Offset and it is an Index, we add our integer to it *) `Index(IdxDom.add i (iDtoIdx n), `NoOffset) | `Field (f, `NoOffset) -> diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 08ad447b5a..366277cb9b 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -894,6 +894,6 @@ struct let invariant man st exp tv = (* The computations that happen here are not computations that happen in the programs *) (* Any overflow during the forward evaluation will already have been flagged here *) - GobRef.wrap AnalysisState.executing_speculative_computations true - @@ fun () -> invariant man st exp tv + let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in + invariant man st exp tv end diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 7831f3d064..e40db604cf 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -2031,7 +2031,7 @@ struct v let dump () = - Out_channel.with_open_bin (get_string "exp.priv-prec-dump") @@ fun f -> + let@ f = Out_channel.with_open_bin (get_string "exp.priv-prec-dump") in (* LVH.iter (fun (l, x) v -> Logs.debug "%a %a = %a" CilType.Location.pretty l CilType.Varinfo.pretty x VD.pretty v ) lvh; *) diff --git a/src/autoTune.ml b/src/autoTune.ml index 044b60bb46..63eb2b683c 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -62,7 +62,7 @@ class findAllocsInLoops = object method! vinst = function | Call (_, Lval (Var f, NoOffset), args,_,_) when LibraryFunctions.is_special f -> - Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo f) ~finally:Fun.id @@ fun () -> + let@ () = Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo f) ~finally:Fun.id in let desc = LibraryFunctions.find f in begin match desc.special args with | Malloc _ @@ -96,7 +96,7 @@ let functionArgs fd = (ResettableLazy.force functionCallMaps).argLists |> Functi let findMallocWrappers () = let isMalloc f = - Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () -> + let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) in if LibraryFunctions.is_special f then let desc = LibraryFunctions.find f in let args = functionArgs f in @@ -177,7 +177,7 @@ let disableIntervalContextsInRecursiveFunctions () = let hasFunction pred = let relevant_static var = - Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () -> + let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) in if LibraryFunctions.is_special var then let desc = LibraryFunctions.find var in GobOption.exists (fun args -> pred desc args) (functionArgs var) @@ -185,7 +185,7 @@ let hasFunction pred = false in let relevant_dynamic var = - Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () -> + let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) in if LibraryFunctions.is_special var then let desc = LibraryFunctions.find var in (* We don't really have arguments at hand, so we cheat and just feed it a list of MyCFG.unknown_exp of appropriate length *) diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml index 2d51f60996..7a1a83038b 100644 --- a/src/cdomain/value/cdomains/offset.ml +++ b/src/cdomain/value/cdomains/offset.ml @@ -217,7 +217,8 @@ struct (* Interval of floor and ceil division in case bitfield offset. *) let bytes_offset = Idx.of_interval (Cilfacade.ptrdiff_ikind ()) Z.(fdiv bits_offset eight, cdiv bits_offset eight) in let remaining_offset = offset_to_index_offset ~typ:field.ftype o in - GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bytes_offset remaining_offset + let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in + Idx.add bytes_offset remaining_offset | `Index (x, o) -> let (item_typ, item_size_in_bytes) = match Option.map unrollType typ with @@ -228,9 +229,13 @@ struct (None, Idx.top ()) in (* Binary operations on offsets should not generate overflow warnings in SV-COMP *) - let bytes_offset = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.mul item_size_in_bytes x in + let bytes_offset = + let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in + Idx.mul item_size_in_bytes x + in let remaining_offset = offset_to_index_offset ?typ:item_typ o in - GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bytes_offset remaining_offset + let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in + Idx.add bytes_offset remaining_offset in offset_to_index_offset ?typ offs diff --git a/src/cdomain/value/util/wideningThresholds.ml b/src/cdomain/value/util/wideningThresholds.ml index 8031236234..7133d88c2a 100644 --- a/src/cdomain/value/util/wideningThresholds.ml +++ b/src/cdomain/value/util/wideningThresholds.ml @@ -115,7 +115,7 @@ class extractInvariantsVisitor (exps) = object method! vinst (i: instr) = match i with | Call (_, Lval (Var f, NoOffset), args, _, _) when LibraryFunctions.is_special f -> - Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () -> + let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) in let desc = LibraryFunctions.find f in begin match desc.special args with | Assert { exp; _ } -> diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 425560e2f1..25c394cf6e 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -153,7 +153,7 @@ struct outside of the apron-related expression conversion. *) let simplify e = - GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> + let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a)) in let simp = query e ikind in let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ikind simp in @@ -177,11 +177,13 @@ struct | false -> (* Cast is not injective - we now try to establish suitable ranges manually *) let t_ik = Cilfacade.get_ikind t in (* retrieving a valuerange for a non-injective cast works by a query to the value-domain with subsequent value extraction from domtuple - which should be speculative, since it is not program code *) - let const,res = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> + let const,res = + let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in (* try to evaluate e by EvalInt Query *) let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a)) in (* convert response to a constant *) - IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res, res in + IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res, res + in match const with | Some c -> Cst (Coeff.s_of_z c) (* Got a constant value -> use it straight away *) (* I gotten top, we can not guarantee injectivity *) diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index 41b83a7297..d2d1a92f8c 100644 --- a/src/common/framework/cfgTools.ml +++ b/src/common/framework/cfgTools.ml @@ -600,7 +600,7 @@ let fprint_hash_dot cfg = let extraNodeStyles node = [] end in - Out_channel.with_open_text "cfg.dot" @@ fun out -> + let@ out = Out_channel.with_open_text "cfg.dot" in let iter_edges f = H.iter (fun n es -> List.iter (f n) es) cfg in let ppf = Format.formatter_of_out_channel out in fprint_dot (module CfgPrinters (NoExtraNodeStyles)) iter_edges ppf; @@ -663,7 +663,7 @@ let dead_code_cfg ~path (module FileCfg: MyCFG.FileCfg) live = let dot_file_name = fd.svar.vname^".dot" in let file_dir = GobSys.mkdir_or_exists_absolute Fpath.(base_dir / c_file_name) in let fname = Fpath.(file_dir / dot_file_name) in - Out_channel.with_open_text (Fpath.to_string fname) @@ fun out -> + let@ out = Out_channel.with_open_text (Fpath.to_string fname) in let ppf = Format.formatter_of_out_channel out in fprint_fundec_html_dot (module FileCfg.Cfg) live fd ppf; Format.pp_print_flush ppf (); diff --git a/src/incremental/serialize.ml b/src/incremental/serialize.ml index 7e01fafa9b..cb8ae58ec0 100644 --- a/src/incremental/serialize.ml +++ b/src/incremental/serialize.ml @@ -20,7 +20,7 @@ let gob_results_dir op = let server () = GobConfig.get_bool "server.enabled" let marshal obj fileName = - Out_channel.with_open_bin (Fpath.to_string fileName) @@ fun chan -> + let@ chan = Out_channel.with_open_bin (Fpath.to_string fileName) in Marshal.to_channel chan obj [] let unmarshal fileName = diff --git a/src/solver/sLR.ml b/src/solver/sLR.ml index 0f239ae813..968ca6879f 100644 --- a/src/solver/sLR.ml +++ b/src/solver/sLR.ml @@ -481,7 +481,7 @@ module PrintInfluence = struct module S1 = Sol (S) (HM) let solve x y = - Out_channel.with_open_text "test.dot" @@ fun ch -> + let@ ch = Out_channel.with_open_text "test.dot" in let r = S1.solve x y in let f k _ = let q = if HM.mem S1.wpoint k then " shape=box style=rounded" else "" in diff --git a/src/transform/deadCode.ml b/src/transform/deadCode.ml index 1b9db8d06a..1f6b74695a 100644 --- a/src/transform/deadCode.ml +++ b/src/transform/deadCode.ml @@ -174,7 +174,7 @@ module RemoveDeadCode : Transform.S = struct the main function(s). Dead functions and globals are removed, since there is no chain of syntactic references to them from the main function(s). *) let open GoblintCil.RmUnused in - GobRef.wrap keepUnused false @@ fun () -> + let@ () = GobRef.wrap keepUnused false in removeUnused ~isRoot:(function | GFun (fd, _) -> List.mem fd.svar.vname (get_string_list "mainfun") diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml index c6c3979788..b625595478 100644 --- a/src/transform/evalAssert.ml +++ b/src/transform/evalAssert.ml @@ -44,7 +44,7 @@ struct let is_lock exp args = match exp with | Lval(Var v,_) when LibraryFunctions.is_special v -> - Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo v) @@ fun () -> + let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo v) in let desc = LibraryFunctions.find v in (match desc.special args with | Lock _ -> true diff --git a/src/transform/transform.ml b/src/transform/transform.ml index acba3e76e4..675bec4932 100644 --- a/src/transform/transform.ml +++ b/src/transform/transform.ml @@ -37,8 +37,8 @@ let run_transformations ?(file_output = true) file names ask = if file_output && List.exists (fun (_, (module T : S)) -> T.requires_file_output) active_transformations then let filename = GobConfig.get_string "trans.output" in - Out_channel.with_open_text filename @@ fun oc -> - GobRef.wrap GoblintCil.lineDirectiveStyle None @@ fun () -> + let@ oc = Out_channel.with_open_text filename in + let@ () = GobRef.wrap GoblintCil.lineDirectiveStyle None in dumpFile defaultCilPrinter oc filename file let run file name = run_transformations ~file_output:false file [name] diff --git a/src/util/std/gobFun.ml b/src/util/std/gobFun.ml new file mode 100644 index 0000000000..42f939e00b --- /dev/null +++ b/src/util/std/gobFun.ml @@ -0,0 +1,5 @@ +module Syntax = +struct + let (let@) f x = f x + (** [let@ x = f in e] is [f @@ fun x -> e]. *) +end diff --git a/src/util/std/goblint_std.ml b/src/util/std/goblint_std.ml index 98c8742c0c..66fc0c1b40 100644 --- a/src/util/std/goblint_std.ml +++ b/src/util/std/goblint_std.ml @@ -5,6 +5,7 @@ OCaml standard library extensions which are not provided by {!Batteries}. *) module GobArray = GobArray +module GobFun = GobFun module GobGc = GobGc module GobHashtbl = GobHashtbl module GobList = GobList @@ -15,6 +16,8 @@ module GobSys = GobSys module GobUnix = GobUnix module GobTuple = GobTuple +include GobFun.Syntax + (** {1 Other libraries} External library extensions. *) diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml index 607f518fd3..d6504d1588 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -63,7 +63,7 @@ struct List.exists (fun (_, edge) -> match edge with | Proc (_, Lval (Var fv, NoOffset), args) when LibraryFunctions.is_special fv -> - Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo fv) @@ fun () -> + let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo fv) in let desc = LibraryFunctions.find fv in begin match desc.special args with | Lock _ -> true diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index d46c4ca818..fdeb15bace 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -87,7 +87,7 @@ let main () = GoblintCil.iterGlobals ast (function | GFun (fd, _) -> - Out_channel.with_open_text (fd.svar.vname ^ ".dot") @@ fun out -> + let@ out = Out_channel.with_open_text (fd.svar.vname ^ ".dot") in let iter_edges = CfgTools.iter_fd_edges (module Cfg) fd in let ppf = Format.formatter_of_out_channel out in CfgTools.fprint_dot (module CfgTools.CfgPrinters (LocationExtraNodeStyles)) iter_edges ppf; diff --git a/tests/regression/cfg/util/dune b/tests/regression/cfg/util/dune index 8ab300b531..0c56de0434 100644 --- a/tests/regression/cfg/util/dune +++ b/tests/regression/cfg/util/dune @@ -2,8 +2,10 @@ (name cfgDot) (libraries goblint-cil + goblint_std goblint_logs goblint_common goblint_lib ; TODO: avoid: extract LoopUnrolling and WitnessUtil node predicates from goblint_lib fpath) + (flags :standard -open Goblint_std) (preprocess (pps ppx_deriving.std)))