diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml index a3bd81ebe62d3c50591a9acfb9368ae0cc733e7c..fd44697b05b549db2a2b78bb62a481e54fc85819 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 f9e0d865b6134bdc577b419c581cd1b986b022d3..373b1bc3c8a4a9fd64153bf3418f7b27fdbe400a 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 590a2a4da92a50c211b21900b97a11579ea6568c..9e1978abbf2011b2948475cd5ef3b5c6b565d8de 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 4872dcfaa89771be3000d36644addbf7b5a76f93..1c3f9472c47cf5b161fd22c454abf0178e36e878 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 e8f7e5f9c7b949e388b33ba1a1c76fb8f6eddb1c..7a67b3e69b43169972c1e83d03304187d7947a47 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)