From 7afe0cc2285e0d626c6caabd2b0065e1bcbd454f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 25 Oct 2023 15:08:16 +0200
Subject: [PATCH] [Eva] Removes unused module [Bool] from Abstract_interp.
---
.../abstract_interp/abstract_interp.ml | 95 -------------------
.../abstract_interp/abstract_interp.mli | 5 -
2 files changed, 100 deletions(-)
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index b7e45ea6820..db5edf1847c 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -306,101 +306,6 @@ module Rel = struct
let sub_abs = sub
end
-
-module Bool = struct
- type t = Top | True | False | Bottom
- let hash (b : t) = Hashtbl.hash b
- let equal (b1 : t) (b2 : t) = b1 = b2
- let compare (b1 : t) (b2 : t) = Stdlib.compare b1 b2
- let pretty fmt = function
- | Top -> Format.fprintf fmt "Top"
- | True -> Format.fprintf fmt "True"
- | False -> Format.fprintf fmt "False"
- | Bottom -> Format.fprintf fmt "Bottom"
- let is_included t1 t2 = match t1, t2 with
- | Bottom, _
- | _, Top
- | True, True
- | False, False -> true
- | _ -> false
- let bottom = Bottom
- let top = Top
- let join b1 b2 = match b1, b2 with
- | Top, _
- | _, Top
- | True, False -> Top
- | True, _
- | _, True -> True
- | False, _
- | _, False -> False
- | Bottom, Bottom -> Bottom
- let narrow b1 b2 = match b1, b2 with
- | Bottom, _
- | _, Bottom
- | True, False -> Bottom
- | True, _
- | _, True -> True
- | False, _
- | _, False -> False
- | Top, Top -> Top
- let link = join
- let meet = narrow
- type widen_hint = unit
- let widen () = join
- let cardinal_zero_or_one b = not (equal b top)
- let intersects b1 b2 = match b1, b2 with
- | Bottom, _ | _, Bottom -> false
- | _, Top | Top, _ -> true
- | False, False | True, True -> true
- | False, True | True, False -> false
- let diff b1 b2 = match b1, b2 with
- | b1, Bottom -> b1
- | _, Top -> Bottom
- | Bottom, _ -> Bottom
- | Top, True -> False
- | Top, False -> True
- | True, True -> Bottom
- | True, False -> True
- | False, True -> False
- | False, False -> Bottom
- let diff_if_one b1 b2 = match b1, b2 with
- | b1, Top -> b1
- | _, _ -> diff b1 b2
- let fold_enum f b init =
- let elements = match b with
- | Top -> [True; False]
- | True -> [True]
- | False -> [False]
- | Bottom -> []
- in
- List.fold_right (fun b acc -> f b acc) elements init
- let cardinal = function
- | Top -> 2
- | True | False -> 1
- | Bottom -> 0
- let cardinal_less_than b i =
- let c = cardinal b in
- if c > i then raise Not_less_than
- else c
-
- type blt = t
- include (Datatype.Make_with_collections
- (struct
- type t = blt
- let name = "Bool_lattice"
- let structural_descr = Structural_descr.t_abstract
- let reprs = [Top; True; False; Bottom]
- let equal = equal
- let compare = compare
- let hash = hash
- let rehash = Datatype.identity
- let copy = Datatype.identity
- let pretty = pretty
- let mem_project = Datatype.never_any_project
- end) :
- Datatype.S with type t := t)
-end
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/abstract_interp/abstract_interp.mli b/src/kernel_services/abstract_interp/abstract_interp.mli
index bf60c997734..4f130d983ec 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.mli
+++ b/src/kernel_services/abstract_interp/abstract_interp.mli
@@ -92,11 +92,6 @@ module Rel : sig
val check: rem:t -> modu:Int.t -> bool
end
-module Bool : sig
- type t = Top | True | False | Bottom
- include Full_AI_Lattice_with_cardinality with type t := t
-end
-
module Make_Lattice_Set
(V : Datatype.S)
(Set: Lattice_type.Hptset with type elt = V.t)
--
GitLab