diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml index f10a55ce9e..6c47f1e87a 100644 --- a/src/cdomains/arrayDomain.ml +++ b/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 diff --git a/src/cdomains/arrayDomain.mli b/src/cdomains/arrayDomain.mli index e7db47a708..9b5a713859 100644 --- a/src/cdomains/arrayDomain.mli +++ b/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 diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 9dfc65a1f1..4a83447e97 100644 --- a/src/cdomains/valueDomain.ml +++ b/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