diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml index 57dd8ab350c1bc6586f6a7e13e6e336afdadb003..cd9f4376d4ef60a4c288d294eb3bca0ec1345b88 100644 --- a/src/plugins/value/domains/cvalue/cvalue_domain.ml +++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml @@ -563,7 +563,9 @@ module State = struct Value_parameters.result "%t" Value_perf.display let post_analysis _state = - if Value_parameters.ForceValues.get () && Value_parameters.verbose_atleast 1 + if Value_parameters.ForceValues.get () + && Value_parameters.verbose_atleast 1 + && Plugin.is_present "inout" then Value_parameters.ForceValues.output display_results end diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml index e294447de6682233ba5f0af253b3df0c0c345341..89f505305e48128fbed9ca567db7db6b36124c7b 100644 --- a/src/plugins/value/engine/compute_functions.ml +++ b/src/plugins/value/engine/compute_functions.ml @@ -54,6 +54,12 @@ let options_ok () = Value_parameters.BuiltinsOverrides.iter (fun (kf, _) -> check_assigns kf); Value_parameters.UsePrototype.iter (fun kf -> check_assigns kf) +let plugins_ok () = + if not (Plugin.is_present "inout") then + Value_parameters.warning + "The inout plugin is missing: some features are disabled, \ + and the analysis may have degraded precision and performance." + (* Do something tasteless in case the user did not put a spec on functions for which he set [-eva-use-spec]: generate an incorrect one ourselves *) let generate_specs () = @@ -73,6 +79,7 @@ let generate_specs () = let pre_analysis () = floats_ok (); options_ok (); + plugins_ok (); Split_return.pretty_strategies (); generate_specs (); Widen.precompute_widen_hints (); diff --git a/tests/value/oracle/unknown_sizeof.0.res.oracle b/tests/value/oracle/unknown_sizeof.0.res.oracle index b106b41c0ed6f8b83419377598478fedd74bcbfe..4244ff0a82bf4d678680de7005b49eb33ba7e264 100644 --- a/tests/value/oracle/unknown_sizeof.0.res.oracle +++ b/tests/value/oracle/unknown_sizeof.0.res.oracle @@ -1,4 +1,5 @@ [kernel] Parsing unknown_sizeof.i (no preprocessing) +[eva] Warning: The inout plugin is missing: some features are disabled, and the analysis may have degraded precision and performance. [eva] Analyzing a complete application starting at main1 [eva] Computing initial state [eva:unknown-size] unknown_sizeof.i:8: Warning: diff --git a/tests/value/oracle/unknown_sizeof.1.res.oracle b/tests/value/oracle/unknown_sizeof.1.res.oracle index 52d022abfce0070deb7ef6ef3f21e519c7411d0a..fd9e82d2f78f1e71419051cac7ceafad4710390f 100644 --- a/tests/value/oracle/unknown_sizeof.1.res.oracle +++ b/tests/value/oracle/unknown_sizeof.1.res.oracle @@ -1,4 +1,5 @@ [kernel] Parsing unknown_sizeof.i (no preprocessing) +[eva] Warning: The inout plugin is missing: some features are disabled, and the analysis may have degraded precision and performance. [eva] Analyzing a complete application starting at main2 [eva] Computing initial state [eva:unknown-size] unknown_sizeof.i:8: Warning: