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

[Eva] Removes the inclusion of garbled mix origins.

Origins should never impact the convergence of the analysis.
parent 9e488f23
No related branches found
No related tags found
No related merge requests found
...@@ -392,8 +392,7 @@ module Make_MapSet_Lattice ...@@ -392,8 +392,7 @@ module Make_MapSet_Lattice
let is_included t1 t2 = let is_included t1 t2 =
match t1, t2 with match t1, t2 with
| Top (s1, o1), Top (s2, o2) -> | Top (s1, _), Top (s2, _) -> KSet.is_included s1 s2
KSet.is_included s1 s2 && Origin.is_included o1 o2
| Map _, Top (KSet.Top, _) -> true | Map _, Top (KSet.Top, _) -> true
| Map m, Top (KSet.Set s, _) -> KVMap.for_all (fun k _ -> KSet.O.mem k s) m | Map m, Top (KSet.Set s, _) -> KVMap.for_all (fun k _ -> KSet.O.mem k s) m
| Top _, Map _ -> false | Top _, Map _ -> false
......
...@@ -119,8 +119,6 @@ let join t1 t2 = ...@@ -119,8 +119,6 @@ let join t1 t2 =
| Well, _ | _, Well -> Well | Well, _ | _, Well -> Well
| Origin o1, Origin o2 -> if o1.id <= o2.id then t1 else t2 | Origin o1, Origin o2 -> if o1.id <= o2.id then t1 else t2
let is_included = equal
(* For each garbled mix origin, keep track of: (* For each garbled mix origin, keep track of:
- the number of writes (according to [register_write] below), i.e. the number - the number of writes (according to [register_write] below), i.e. the number
......
...@@ -53,7 +53,6 @@ val pretty_as_reason: Format.formatter -> t -> unit ...@@ -53,7 +53,6 @@ val pretty_as_reason: Format.formatter -> t -> unit
val descr: t -> string val descr: t -> string
val join: t -> t -> t val join: t -> t -> t
val is_included: t -> t -> bool
(** Records the write of an imprecise value of the given bases, (** Records the write of an imprecise value of the given bases,
with the given origin. with the given origin.
......
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