From 9622d3d74603277b4bcf9939fcf48830e5fa2248 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Tue, 27 Sep 2022 11:02:02 +0200
Subject: [PATCH] [ivette] Some minor modifications
It's just code styling details.
---
ivette/src/frama-c/kernel/Properties.tsx | 19 +++++++------------
src/plugins/eva/domains/taint_domain.ml | 14 +++++---------
2 files changed, 12 insertions(+), 21 deletions(-)
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index 724e84c6564..5b66ec5c0d0 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 dc1f05c9ba4..95ea09a4a54 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
--
GitLab