[Eva] Remove obsolete warning_once_current

src/plugins/eva/domains/cvalue/builtins_malloc.ml

@@ -535,7 +535,7 @@ let calloc_builtin state args =
   let size = Cvalue.V.mul nmemb sizev in
   let size_ok = alloc_size_ok size in
   if size_ok <> Alarmset.True then
-    Eva_utils.warning_once_current
+    Self.warning ~current:true ~once:true
       "calloc out of bounds: assert(nmemb * size <= SIZE_MAX)";
   let c_values =
     if size_ok = Alarmset.False (* size always overflows *)
@@ -861,7 +861,7 @@ let reallocarray_builtin state args =
   let size = Cvalue.V.mul nmemb sizev in
   let size_ok = alloc_size_ok size in
   if size_ok <> Alarmset.True then
-    Eva_utils.warning_once_current
+    Self.warning ~current:true ~once:true
       "reallocarray out of bounds: assert(nmemb * size <= SIZE_MAX)";
   if size_ok = Alarmset.False (* size always overflows *)
   then Builtins.Result [Cvalue.V.singleton_zero]
@@ -920,7 +920,8 @@ let check_leaked_malloced_bases state _ =
   let alloced_bases = Dynamic_Alloc_Bases.get () in
   Base_hptmap.iter
     (fun base _ -> if check_if_base_is_leaked base state then
-        Eva_utils.warning_once_current "memory leak detected for %a"
+        Self.warning ~current:true ~once:true
+          "memory leak detected for %a"
           Base.pretty base)
     alloced_bases;
   let c_clobbered = Base.SetLattice.bottom in

src/plugins/eva/domains/cvalue/builtins_misc.ml

@@ -20,13 +20,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Eva_utils
-
 open Lattice_bounds.Bottom.Operators
 
 let frama_C_assert state actuals =
   let do_bottom () =
-    warning_once_current "Frama_C_assert: false";
+    Self.warning ~current:true ~once:true "Frama_C_assert: false";
     Cvalue.Model.bottom
   in
   match actuals with
@@ -42,11 +40,13 @@ let frama_C_assert state actuals =
           Cvalue_transfer.update valuation state
         in
         match state with
-        | `Value state -> warning_once_current "Frama_C_assert: unknown"; state
+        | `Value state ->
+          Self.warning ~current:true ~once:true "Frama_C_assert: unknown";
+          state
         | `Bottom -> do_bottom ()
       end
       else begin
-        warning_once_current "Frama_C_assert: true";
+        Self.warning ~current:true ~once:true "Frama_C_assert: true";
         state
       end
     in

src/plugins/eva/engine/iterator.ml

@@ -259,7 +259,7 @@ module Make_Dataflow
     let asm_contracts = Annotations.code_annot stmt in
     match Logic_utils.extract_contract asm_contracts with
     | [] ->
-      Eva_utils.warning_once_current
+      Self.warning ~current:true ~once:true
         "assuming assembly code has no effects in function %t"
         Eva_utils.pretty_current_cfunction_name;
       id
@@ -717,7 +717,7 @@ module Computer
       Dataflow.merge_results ~save_results;
       let f = Kernel_function.get_definition kf in
       if Cil.typeHasAttribute "noreturn" f.svar.vtype && results <> [] then
-        Eva_utils.warning_once_current
+        Self.warning ~current:true ~once:true
           "function %a may terminate but has the noreturn attribute"
           Kernel_function.pretty kf;
       results, !Dataflow.cacheable

src/plugins/eva/engine/transfer_specification.ml

@@ -40,7 +40,7 @@ let find_default_behavior spec =
   List.find (fun b' -> b'.b_name = Cil.default_behavior_name) spec.spec_behavior
 
 let warn_empty_assigns () =
-  Eva_utils.warning_once_current
+  Self.warning ~current:true ~once:true
     "Cannot handle empty assigns clause. Assuming assigns \\nothing: \
      be aware this is probably incorrect."
 
@@ -164,7 +164,7 @@ let precise_loc_of_assign env kind term =
     in
     if kind <> From then reduce_to_valid_location kind term loc else Some loc
   with Eval_terms.LogicEvalError e ->
-    Eva_utils.warning_once_current
+    Self.warning ~current:true ~once:true
       "@[<hov 0>@[<hov 2>cannot interpret %a@]%a;@ effects will be ignored@]"
       pp_assign_clause (kind, term) pp_eval_error e;
     None

src/plugins/eva/utils/eva_utils.ml

@@ -106,9 +106,6 @@ let pretty_actuals fmt actuals =
 let pretty_current_cfunction_name fmt =
   Kernel_function.pretty fmt (current_kf())
 
-let warning_once_current fmt =
-  Self.warning ~current:true ~once:true fmt
-
 (* Emit alarms in "non-warning" mode *)
 let alarm_report ?current ?source ?emitwith ?echo ?once ?append =
   Self.warning ~wkey:Self.wkey_alarm

src/plugins/eva/utils/eva_utils.mli

@@ -63,7 +63,6 @@ val get_subdivision: stmt -> int
 val pretty_actuals :
   Format.formatter -> (Eva_ast.exp * Cvalue.V.t) list -> unit
 val pretty_current_cfunction_name : Format.formatter -> unit
-val warning_once_current : ('a, Format.formatter, unit) format -> 'a
 
 (** Emit an alarm, either as warning or as a result, according to
     status associated to {!Self.wkey_alarm} *)

src/plugins/eva/values/cvalue_forward.ml

@@ -540,8 +540,9 @@ let eval_float_constant f fkind fstring =
         if Fc_float.is_infinite f_lower && Fc_float.is_infinite f_upper
         then
           begin
-            Eva_utils.warning_once_current
-              "cannot parse floating-point constant, returning imprecise result";
+            Self.warning ~current:true ~once:true
+              "cannot parse floating-point constant, \
+               returning imprecise result";
             neg_infinity, infinity
           end
         else f_lower, f_upper