From 7da9dcffc2f983cbb1811e512d9d37e67477b7ec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Sat, 15 Jan 2022 22:49:54 +0100
Subject: [PATCH] [Eva] Do not crash when the inout plugin is missing.
Warns at the start of an analysis when the inout plugin is missing.
---
src/plugins/value/domains/cvalue/cvalue_domain.ml | 4 +++-
src/plugins/value/engine/compute_functions.ml | 7 +++++++
tests/value/oracle/unknown_sizeof.0.res.oracle | 1 +
tests/value/oracle/unknown_sizeof.1.res.oracle | 1 +
4 files changed, 12 insertions(+), 1 deletion(-)
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 57dd8ab350c..cd9f4376d4e 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 e294447de66..89f505305e4 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 b106b41c0ed..4244ff0a82b 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 52d022abfce..fd9e82d2f78 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:
--
GitLab