diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index ae2a20ae8290e181f17ee018e2e4de1c84967ba0..9807305d313ebbcdaa354103847e76ce590d8792 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -632,9 +632,6 @@ module Assigns: sig
module DepsOrUnassigned : sig
type t =
- | DepsBottom (** Bottom of the lattice, never bound inside a memory state
- at a valid location. (May appear for bases for which the
- validity does not start at 0, currently only NULL.) *)
| Unassigned (** Location has never been assigned *)
| AssignedFrom of Deps.t (** Location guaranteed to have been overwritten,
its contents depend on the [Deps.t] value *)
diff --git a/src/plugins/eva/types/assigns.ml b/src/plugins/eva/types/assigns.ml
index 012d7bee76053319fa155e0fe3da511f75c5730e..ba5ac5946caa0df13d83e7e69abcdf8e72ed9164 100644
--- a/src/plugins/eva/types/assigns.ml
+++ b/src/plugins/eva/types/assigns.ml
@@ -25,7 +25,6 @@ module DepsOrUnassigned = struct
include Datatype.Serializable_undefined
type t =
- | DepsBottom
| Unassigned
| AssignedFrom of Deps.t
| MaybeAssignedFrom of Deps.t
@@ -34,17 +33,15 @@ module DepsOrUnassigned = struct
let name = "Eva.Froms.DepsOrUnassigned"
let pretty fmt = function
- | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
| Unassigned -> Format.pp_print_string fmt "UNASSIGNED"
| AssignedFrom fd -> Deps.pretty_precise fmt fd
| MaybeAssignedFrom fd ->
Format.fprintf fmt "%a (or UNASSIGNED)" Deps.pretty_precise fd
let hash = function
- | DepsBottom -> 1
- | Unassigned -> 2
- | AssignedFrom fd -> Hashtbl.hash (3, Deps.hash fd)
- | MaybeAssignedFrom fd -> Hashtbl.hash (4, Deps.hash fd)
+ | Unassigned -> 1
+ | AssignedFrom fd -> Hashtbl.hash (2, Deps.hash fd)
+ | MaybeAssignedFrom fd -> Hashtbl.hash (3, Deps.hash fd)
let reprs = Unassigned :: List.map (fun r -> AssignedFrom r) Deps.reprs
end
@@ -53,7 +50,6 @@ module DepsOrUnassigned = struct
include Datatype_Input
let join d1 d2 = match d1, d2 with
- | DepsBottom, d | d, DepsBottom -> d
| Unassigned, Unassigned -> Unassigned
| Unassigned, AssignedFrom fd | AssignedFrom fd, Unassigned ->
MaybeAssignedFrom fd
@@ -68,14 +64,11 @@ module DepsOrUnassigned = struct
MaybeAssignedFrom (Deps.join fd1 fd2)
let is_included d1 d2 = match d1, d2 with
- | DepsBottom, (DepsBottom | Unassigned | AssignedFrom _ |
- MaybeAssignedFrom _)
| Unassigned, (Unassigned | AssignedFrom _ | MaybeAssignedFrom _) ->
true
| MaybeAssignedFrom fd1, (AssignedFrom fd2 | MaybeAssignedFrom fd2)
| AssignedFrom fd1, AssignedFrom fd2 ->
Deps.is_included fd1 fd2
- | (Unassigned | AssignedFrom _ | MaybeAssignedFrom _), DepsBottom
| (AssignedFrom _ | MaybeAssignedFrom _), Unassigned
| AssignedFrom _, MaybeAssignedFrom _ ->
false
@@ -85,11 +78,11 @@ module DepsOrUnassigned = struct
let default_is_bottom = false
let to_zone = function
- | DepsBottom | Unassigned -> Locations.Zone.bottom
+ | Unassigned -> Locations.Zone.bottom
| AssignedFrom fd | MaybeAssignedFrom fd -> Deps.to_zone fd
let may_be_unassigned = function
- | DepsBottom | AssignedFrom _ -> false
+ | AssignedFrom _ -> false
| Unassigned | MaybeAssignedFrom _ -> true
end
@@ -97,7 +90,7 @@ module Memory = struct
(* A From table is internally represented as a Lmap of [DepsOrUnassigned].
However, the API mostly hides this fact, and exports access functions
that take or return [Deps.t] values. This way, the user needs not
- understand the subtleties of DepsBottom/Unassigned/MaybeAssigned. *)
+ understand the subtleties of Unassigned/MaybeAssigned. *)
include Lmap_bitwise.Make_bitwise(DepsOrUnassigned)
@@ -150,7 +143,6 @@ module Memory = struct
(* If the interval can be unassigned, we collect its bound. We also
return the dependencies stored at this interval. *)
let default, v = match v with
- | DepsOrUnassigned.DepsBottom -> false, Deps.bottom
| DepsOrUnassigned.Unassigned -> true, Deps.bottom
| DepsOrUnassigned.MaybeAssignedFrom v -> true, v
| DepsOrUnassigned.AssignedFrom v -> false, v
@@ -234,6 +226,6 @@ let outputs assigns =
(fun z v acc ->
let open DepsOrUnassigned in
match v with
- | DepsBottom | Unassigned -> acc
+ | Unassigned -> acc
| AssignedFrom _ | MaybeAssignedFrom _ -> Locations.Zone.join z acc)
m Locations.Zone.bottom
diff --git a/src/plugins/eva/types/assigns.mli b/src/plugins/eva/types/assigns.mli
index a4b3fb16b0b08959ada08b3ab2e7428bb46e8778..cd354ebbb5d1600b0b7ca12489c08b9cd5403901 100644
--- a/src/plugins/eva/types/assigns.mli
+++ b/src/plugins/eva/types/assigns.mli
@@ -27,9 +27,6 @@
module DepsOrUnassigned : sig
type t =
- | DepsBottom (** Bottom of the lattice, never bound inside a memory state
- at a valid location. (May appear for bases for which the
- validity does not start at 0, currently only NULL.) *)
| Unassigned (** Location has never been assigned *)
| AssignedFrom of Deps.t (** Location guaranteed to have been overwritten,
its contents depend on the [Deps.t] value *)
diff --git a/src/plugins/from/from_memory.ml b/src/plugins/from/from_memory.ml
index 9446b88258bf9610b94b42ce0140b2c7ded02bf4..bf8e718ac28c518efdfbfa16aa74e04beb72f1b8 100644
--- a/src/plugins/from/from_memory.ml
+++ b/src/plugins/from/from_memory.ml
@@ -28,7 +28,6 @@ module DepsOrUnassigned = struct
let subst f d =
match d with
- | DepsBottom -> DepsBottom
| Unassigned -> Unassigned
| AssignedFrom fd ->
let fd' = f fd in
@@ -39,8 +38,6 @@ module DepsOrUnassigned = struct
let compose d1 d2 =
match d1, d2 with
- | DepsBottom, _ | _, DepsBottom ->
- DepsBottom (* could indicate dead code. Not used in practice anyway *)
| Unassigned, _ -> d2
| AssignedFrom _, _ -> d1
| MaybeAssignedFrom _, Unassigned -> d1
@@ -52,14 +49,12 @@ module DepsOrUnassigned = struct
(* for backwards compatibility *)
let pretty fmt fd =
match fd with
- | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
| Unassigned -> Format.pp_print_string fmt "(SELF)"
| AssignedFrom d -> Zone.pretty fmt (Deps.to_zone d)
| MaybeAssignedFrom d ->
Format.fprintf fmt "%a (and SELF)" Zone.pretty (Deps.to_zone d)
let pretty_precise fmt = function
- | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
| Unassigned -> Format.pp_print_string fmt "UNASSIGNED"
| AssignedFrom fd -> Deps.pretty_precise fmt fd
| MaybeAssignedFrom fd ->
@@ -197,7 +192,6 @@ let collapse_return x = x
(* ----- Pretty-printing ---------------------------------------------------- *)
let pretty_skip = function
- | DepsOrUnassigned.DepsBottom -> true
| DepsOrUnassigned.Unassigned -> true
| DepsOrUnassigned.AssignedFrom _ -> false
| DepsOrUnassigned.MaybeAssignedFrom _ -> false
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 3c4ca70562ce8dd7da47f16b043c443c61c937be..98e6aee809bcc8eaa0abe9bcd2004e290aa4edb6 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -526,7 +526,7 @@ let extract_inout_from_froms assigns =
(* Skip zones fully unassigned, they are not really port of the
dependencies, but just present in the offsetmap to avoid "holes" *)
match (in_ : Eva.Assigns.DepsOrUnassigned.t) with
- | DepsBottom | Unassigned -> acc
+ | Unassigned -> acc
| AssignedFrom in_ | MaybeAssignedFrom in_ ->
Zone.join acc_in (Eva.Deps.to_zone in_),
Zone.join acc_out out