[Eva] Removes unused value DepsBottom.

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 *)

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

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 *)

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

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