diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx index 724e84c65649e646b8dd3d81249d91e8b3eea978..5b66ec5c0d049cfa2498c4b161151e48999e54e0 100644 --- a/ivette/src/frama-c/kernel/Properties.tsx +++ b/ivette/src/frama-c/kernel/Properties.tsx @@ -202,27 +202,22 @@ function filterAlarm(alarm: string | undefined): boolean { } function filterEva(p: Property): boolean { - let b = true; if ('priority' in p && p.priority === false && filter('eva.priority_only')) - b = false; + return false; if ('taint' in p) { switch (p.taint) { case 'not_tainted': case 'not_applicable': - if (filter('eva.data_tainted_only') || filter('eva.ctrl_tainted_only')) - b = false; - break; + const data_tainted_only = filter('eva.data_tainted_only'); + const ctrl_tainted_only = filter('eva.ctrl_tainted_only'); + return !(data_tainted_only || ctrl_tainted_only); case 'direct_taint': - if (filter('eva.ctrl_tainted_only')) - b = false; - break; + return !(filter('eva.ctrl_tainted_only')); case 'indirect_taint': - if (filter('eva.data_tainted_only')) - b = false; - break; + return !(filter('eva.data_tainted_only')); } } - return b; + return true; } function filterProperty(p: Property): boolean { diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml index dc1f05c9ba4a2b930ed96fae8816505b414a0bfc..95ea09a4a544a6ab00a9f0624547c84d57f67bf0 100644 --- a/src/plugins/eva/domains/taint_domain.ml +++ b/src/plugins/eva/domains/taint_domain.ml @@ -597,13 +597,9 @@ let () = Abstractions.register_hook interpret_taint_logic type taint = Direct | Indirect | Untainted -let is_tainted state ?indirect zone = - let intersects_any_taint z = - Zone.intersects (Zone.join state.locs_data state.locs_control) z - in - if Zone.intersects zone state.locs_data - then Direct - else if Zone.intersects zone state.locs_control - || Option.fold indirect ~none:false ~some:intersects_any_taint - then Indirect +let is_tainted { locs_data ; locs_control } ?indirect zone = + let intersects_any z = Zone.(intersects (join locs_data locs_control) z) in + let is_indirect () = Option.fold indirect ~none:false ~some:intersects_any in + if Zone.intersects zone locs_data then Direct + else if Zone.intersects zone locs_control || is_indirect () then Indirect else Untainted