Deduplicate Null declarations

src/cdomains/arrayDomain.ml

@@ -107,9 +107,9 @@ sig
   val smart_leq: (Cil.exp -> BI.t option) -> (Cil.exp -> BI.t option) -> t -> t -> bool
 end
 
-module type LatticeWithNull =
+module type Null =
 sig
-  include LatticeWithSmartOps
+  type t
   type retnull = Null | NotNull | Maybe
 
   val null: unit -> t
@@ -120,6 +120,12 @@ sig
   val not_zero_of_ikind: Cil.ikind -> t
 end
 
+module type LatticeWithNull =
+sig
+  include LatticeWithSmartOps
+  include Null with type t := t
+end
+
 module Trivial (Val: LatticeWithInvalidate) (Idx: Lattice.S): S with type value = Val.t and type idx = Idx.t =
 struct
   include Val

src/cdomains/arrayDomain.mli

@@ -123,9 +123,9 @@ sig
   val smart_leq: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t -> bool
 end
 
-module type LatticeWithNull =
+module type Null =
 sig
-  include LatticeWithSmartOps
+  type t
   type retnull = Null | NotNull | Maybe
 
   val null: unit -> t
@@ -136,6 +136,12 @@ sig
   val not_zero_of_ikind: Cil.ikind -> t
 end
 
+module type LatticeWithNull =
+sig
+  include LatticeWithSmartOps
+  include Null with type t := t
+end
+
 module Trivial (Val: LatticeWithInvalidate) (Idx: Lattice.S): S with type value = Val.t and type idx = Idx.t
 (** This functor creates a trivial single cell representation of an array. The
   * indexing type is taken as a parameter to satisfy the type system, it is not

src/cdomains/valueDomain.ml

@@ -39,13 +39,7 @@ sig
   val is_top_value: t -> typ -> bool
   val zero_init_value: ?varAttr:attributes -> typ -> t
 
-  type retnull = Null | NotNull | Maybe
-  val null: unit -> t
-  val is_null: t -> retnull
-
-  val get_ikind: t -> Cil.ikind option
-  val zero_of_ikind: Cil.ikind -> t
-  val not_zero_of_ikind: Cil.ikind -> t
+  include ArrayDomain.Null with type t := t
 
   val project: VDQ.t -> int_precision option-> ( attributes * attributes ) option -> t -> t
   val mark_jmpbufs_as_copied: t -> t