[Eva] Removes some debug messages.

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; }

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. *)

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"
 

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
 

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)