From 3a6f6364171270d58bd926c451604bbceccae857 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 27 Feb 2020 14:03:08 +0100
Subject: [PATCH] [Eva] Do not emit redundant invalid_pointer and memory_access
 alarms.

---
 src/plugins/value/alarmset.ml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 222eed3099d..21475b79a7a 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -399,7 +399,25 @@ let height_alarm = let open Value_util in function
 let cmp a1 a2 =
   Datatype.Int.compare (height_alarm (fst a1)) (height_alarm (fst a2))
 
+let remove_redundant_alarms map =
+  let filter alarm status =
+    match alarm with
+    | Alarms.Invalid_pointer expr ->
+      let lval = Mem expr, NoOffset in
+      let implies alarm s =
+        status = s &&
+        match alarm with
+        | Alarms.Memory_access (lv, _access_kind) ->
+          Cil_datatype.LvalStructEq.equal lv lval
+        | _ -> false
+      in
+      not (M.exists implies map)
+    | _ -> true
+  in
+  M.filter filter map
+
 let emit_alarms kinstr map =
+  let map = remove_redundant_alarms map in
   let list = M.bindings map in
   let sorted_list = List.sort cmp list in
   List.iter (fun (alarm, status) -> emit_alarm kinstr alarm status) sorted_list;
-- 
GitLab