diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml index 4c2bd6202f7d9bf8b4e91887c318447f15b091c5..39b5d236544be119a96fefd6848729ddafab8c9e 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 d39e990b9dc6613be513aa5d2a42f825a005386f..8126dda260958b2954f0aaf4e52df515036e9c3a 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 8fe9a26d5b60bd0222ce0d623b4ac0c87bd01c35..da5c14f22b2a58f2bb6a5d3a09e37611a204211b 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 dd67f76849324e533f84ca8f79ec551b87078fb0..e2280ec81b2c4ad240ddcd1902c29356572e55d9 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 34883ace8adb8f69fb01045657630c21715090d6..6e92b4373d7234f4919ff260b91e34f67b68df90 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 a14dd721dea46ae8235d8920d4808ea5ddd6e1fa..a35f29f8d30cc08b81ea9531ead9184e34b242df 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 *)