From aec4b8cbabd7f9c40a09e12352dfa8b9bb17207f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 26 Sep 2024 14:15:02 +0200
Subject: [PATCH] [Eva] Removes some debug messages.
---
src/plugins/eva/engine/compute_functions.ml | 7 +------
src/plugins/eva/engine/transfer_stmt.ml | 12 +++---------
src/plugins/eva/self.ml | 2 --
src/plugins/eva/self.mli | 2 --
src/plugins/eva/utils/cvalue_callbacks.ml | 4 ----
5 files changed, 4 insertions(+), 23 deletions(-)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index a3bd81ebe62..fd44697b05b 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -23,8 +23,6 @@
open Cil_types
open Eval
-let dkey = Self.register_category "callbacks"
-
(* Clear Eva's various caches. Some operations of Eva depend on parameters,
such as -ilevel or -plevel, so clearing those caches ensures that those
options have the expected effect.
@@ -216,12 +214,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let ab = Logic.create init_state call.kf in
ignore (Logic.check_fct_preconditions kinstr call.kf ab init_state);
end;
- if Parameters.ValShowProgress.get () then begin
+ if Parameters.ValShowProgress.get () then
Self.feedback ~current:true
"Reusing old results for call to %a" Kernel_function.pretty call.kf;
- Self.debug ~dkey
- "calling Record_Value_New callbacks on saved previous result";
- end;
apply_call_results_hooks call init_state (`Reuse i);
(* call can be cached since it was cached once *)
Transfer.{ states; cacheable = Cacheable; }
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index f9e0d865b61..373b1bc3c8a 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -146,16 +146,10 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
a bug."
fmt
- let report_unreachability state (result, alarms) fmt =
+ let report_unreachability _state (result, alarms) fmt =
if result = `Bottom && Alarmset.is_empty alarms
- then begin
- Self.debug ~current:true ~once:true ~level:1
- ~dkey:Self.dkey_incompatible_states
- "State without concretization: %a" Domain.pretty state;
- notify_unreachability fmt
- end
- else
- Format.ifprintf Format.std_formatter fmt
+ then notify_unreachability fmt
+ else Format.ifprintf Format.std_formatter fmt
(* The three functions below call evaluation functions and notify the user
if they lead to bottom without alarms. *)
diff --git a/src/plugins/eva/self.ml b/src/plugins/eva/self.ml
index 590a2a4da92..9e1978abbf2 100644
--- a/src/plugins/eva/self.ml
+++ b/src/plugins/eva/self.ml
@@ -80,9 +80,7 @@ let dkey_final_states = register_category "final-states"
let dkey_summary = register_category "summary"
let dkey_pointer_comparison = register_category "pointer-comparison"
let dkey_cvalue_domain = register_category "d-cvalue"
-let dkey_incompatible_states = register_category "incompatible-states"
let dkey_iterator = register_category "iterator"
-let dkey_callbacks = register_category "callbacks"
let dkey_widening = register_category "widening"
let dkey_recursion = register_category "recursion"
diff --git a/src/plugins/eva/self.mli b/src/plugins/eva/self.mli
index 4872dcfaa89..1c3f9472c47 100644
--- a/src/plugins/eva/self.mli
+++ b/src/plugins/eva/self.mli
@@ -49,9 +49,7 @@ val dkey_summary : category
val dkey_pointer_comparison: category
val dkey_cvalue_domain: category
-val dkey_incompatible_states: category
val dkey_iterator : category
-val dkey_callbacks : category
val dkey_widening : category
val dkey_recursion : category
diff --git a/src/plugins/eva/utils/cvalue_callbacks.ml b/src/plugins/eva/utils/cvalue_callbacks.ml
index e8f7e5f9c7b..7a67b3e69b4 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.ml
+++ b/src/plugins/eva/utils/cvalue_callbacks.ml
@@ -22,8 +22,6 @@
open Cil_types
-let dkey = Self.dkey_callbacks
-
type state = Cvalue.Model.t
type analysis_kind = [ `Builtin | `Spec | `Body | `Reuse ]
@@ -65,8 +63,6 @@ let register_call_results_hook f =
(fun (callstack, kf, state, results) -> f callstack kf state results)
let apply_call_results_hooks callstack kf state call_results =
- if Parameters.ValShowProgress.get () && not (Call_Results.is_empty ())
- then Self.debug ~dkey "now calling Call_Results callbacks";
Call_Results.apply (callstack, kf, state, call_results)
--
GitLab