LatticeSignature for lattices. Functors for common lattices.
module Pretty = GoblintCil.Prettymodule type PO = sig ... endmodule type S = sig ... endException raised by a topless lattice in place of a top value. Surrounding lattice functors may handle this on their own.
Exception raised by a bottomless lattice in place of a bottom value. Surrounding lattice functors may handle this on their own.
exception Invalid_widen of Pretty.docval assert_valid_widen :
leq:('a -> 'b -> bool) ->
pretty_diff:(unit -> ('a * 'b) -> Pretty.doc) ->
'a ->
'b ->
unitmodule UnitConf (N : Printable.Name) : sig ... endmodule Unit : sig ... endmodule NoBotTop : sig ... endmodule Fake (Base : Printable.S) : sig ... endmodule type PD = sig ... endmodule FakeSingleton (Base : PD) : sig ... endmodule HashCached (M : S) : sig ... endmodule Flat (Base : Printable.S) (N : Printable.LiftingNames) : sig ... endmodule Lift (Base : S) (N : Printable.LiftingNames) : sig ... endmodule LiftPO (Base : PO) (N : Printable.LiftingNames) : sig ... endmodule ProdSimple (Base1 : S) (Base2 : S) : sig ... endmodule type Num = sig ... endmodule Chain (P : Printable.ChainParams) : S with type t = int