Skip to content
Snippets Groups Projects
Commit 3a6f6364 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Do not emit redundant invalid_pointer and memory_access alarms.

parent a5a70d3f
No related branches found
No related tags found
No related merge requests found
......@@ -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;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment