From 29c865bce43ab2844159308e9b6e8aba899e7953 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 4 Apr 2022 09:24:29 +0200
Subject: [PATCH] [Eva] Exports [condition_truth_value] in the new Eva API.
Uses it in other plugins, instead of Db.Value.
---
src/plugins/pdg/build.ml | 2 +-
src/plugins/postdominators/compute.ml | 3 +--
src/plugins/slicing/slicingTransform.ml | 2 +-
src/plugins/sparecode/transform.ml | 2 +-
src/plugins/value/utils/results.ml | 1 +
src/plugins/value/utils/results.mli | 4 ++++
6 files changed, 9 insertions(+), 5 deletions(-)
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 4c2bd6202f7..39b5d236544 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -765,7 +765,7 @@ let process_condition ctrl_dpds_infos pdg state stmt condition =
let decls_cond = Cil.extract_varinfos_from_exp condition in
let controlled_stmts = CtrlDpds.get_if_controlled_stmts ctrl_dpds_infos stmt in
- let go_then, go_else = Db.Value.condition_truth_value stmt in
+ let go_then, go_else = Eva.Results.condition_truth_value stmt in
let real = go_then && go_else (* real dpd if we can go in both branches *) in
if not real then
debug
diff --git a/src/plugins/postdominators/compute.ml b/src/plugins/postdominators/compute.ml
index d39e990b9dc..8126dda2609 100644
--- a/src/plugins/postdominators/compute.ml
+++ b/src/plugins/postdominators/compute.ml
@@ -258,8 +258,7 @@ include
let is_accessible = Eva.Results.is_reachable
let dependencies = [ Eva.Analysis.self ]
let name = "value"
- let eval_cond stmt _e =
- Db.Value.condition_truth_value stmt
+ let eval_cond stmt _e = Eva.Results.condition_truth_value stmt
end)
(Db.PostdominatorsValue)
diff --git a/src/plugins/slicing/slicingTransform.ml b/src/plugins/slicing/slicingTransform.ml
index 8fe9a26d5b6..da5c14f22b2 100644
--- a/src/plugins/slicing/slicingTransform.ml
+++ b/src/plugins/slicing/slicingTransform.ml
@@ -449,7 +449,7 @@ module Visibility (SliceName : sig
info
let cond_edge_visible _ff_opt s =
- Db.Value.condition_truth_value s
+ Eva.Results.condition_truth_value s
end
diff --git a/src/plugins/sparecode/transform.ml b/src/plugins/sparecode/transform.ml
index dd67f768493..e2280ec81b2 100644
--- a/src/plugins/sparecode/transform.ml
+++ b/src/plugins/sparecode/transform.ml
@@ -155,7 +155,7 @@ module BoolInfo = struct
with Kernel_function.No_Statement -> true
let cond_edge_visible _ s =
- Db.Value.condition_truth_value s
+ Eva.Results.condition_truth_value s
end
module Info = Filter.F (BoolInfo)
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 34883ace8ad..6e92b4373d7 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -682,6 +682,7 @@ let is_reachable_kinstr kinstr =
let module M = Make () in
M.is_reachable (before_kinstr kinstr)
+let condition_truth_value = Db.Value.condition_truth_value
(* Callers / callsites *)
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index a14dd721dea..a35f29f8d30 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -275,6 +275,10 @@ val is_reachable : Cil_types.stmt -> bool
the main function has been analyzed for [Kglobal]. *)
val is_reachable_kinstr : Cil_types.kinstr -> bool
+val condition_truth_value: Cil_types.stmt -> bool * bool
+(** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
+ (resp. snd) is true if and only if the condition of the 'if' has been
+ evaluated to true (resp. false) at least once during the analysis. *)
(*** Callers / Callees / Callsites *)
--
GitLab