diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index 0b59d55c65bedf4517163f9383ac8e38df405684..8ec8dba455741efcceec85330e0f622410bcf327 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/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
diff --git a/src/plugins/eva/domains/cvalue/builtins_misc.ml b/src/plugins/eva/domains/cvalue/builtins_misc.ml
index 9d6c78ca537d7078b0e151f817614a2fa2ccd3e5..7238d3e459cc9966cc61209b4d6bcfa52de73650 100644
--- a/src/plugins/eva/domains/cvalue/builtins_misc.ml
+++ b/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
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index ab67e6f585735b0035a0844fbcfa16d6ac420263..0c7bd34fdb07177cf8626a36f13c9c675448c15a 100644
--- a/src/plugins/eva/engine/iterator.ml
+++ b/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
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index a8ea53b9baf6785cfc5a4af4eceb8ac8ccbc3878..27c8c62b98e4c22dc3cafcfffba856dd7a573147 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/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
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 72a2129efb597b05b4372119dc97c323f2c53dd9..b40e802a7f76c006b911ee53fd796a4a28c22902 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/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
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index a147daaa16051d4a2e98ece7079b2d456d4a1bdb..9d319318e27a4d59cc370331764fb1edf5eaadb9 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/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} *)
diff --git a/src/plugins/eva/values/cvalue_forward.ml b/src/plugins/eva/values/cvalue_forward.ml
index bdeb63e5308b760d781a2213253300c02bb4de02..44e344b820908f215e146305f9b7419fe02d0104 100644
--- a/src/plugins/eva/values/cvalue_forward.ml
+++ b/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