From 44bb6ab0dbb118d6cc531e382373690cdf7b7ef8 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 19 May 2021 22:04:25 +0200
Subject: [PATCH] [Eva] Do not add lv_zone once again if tainted because of
annotation.
---
src/plugins/value/domains/taint_domain.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 404fab1b7f2..49391ece4c4 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -234,7 +234,7 @@ module TransferTaint = struct
let is_taint_annotated = Zone.is_included lv_zone annot_zone in
if is_taint_annotated
then
- { state with locs_data = Zone.join state.locs_data lv_zone }
+ state
else
(* Compute data-dependency with [state]: whenever [exp] (or its
sub-expressions) is tainted, or [lv] is indexed by a tainted memory
--
GitLab