Module `Lattice`Source

Signature for lattices. Functors for common lattices.

module Pretty = GoblintCil.Pretty

Sourceexception Uncomparable

Sourcemodule type PO = sig ... end

Sourcemodule type S = sig ... end

Sourceexception TopValue

Exception raised by a topless lattice in place of a top value. Surrounding lattice functors may handle this on their own.

Sourceexception BotValue

Exception raised by a bottomless lattice in place of a bottom value. Surrounding lattice functors may handle this on their own.

Sourceexception Unsupported of string

Sourceval unsupported : string -> 'a

Sourceexception Invalid_widen of Pretty.doc

Source

val assert_valid_widen : 
  leq:('a -> 'b -> bool) ->
  pretty_diff:(unit -> ('a * 'b) -> Pretty.doc) ->
  'a ->
  'b ->
  unit

Sourcemodule UnitConf (N : Printable.Name) : sig ... end

Sourcemodule Unit : sig ... end

Sourcemodule NoBotTop : sig ... end

Sourcemodule Fake (Base : Printable.S) : sig ... end

Sourcemodule type PD = sig ... end

Sourcemodule FakeSingleton (Base : PD) : sig ... end

Sourcemodule Reverse (Base : S) : sig ... end

Sourcemodule HConsed (Base : S) (Arg : sig ... end) : sig ... end

Sourcemodule HashCached (M : S) : sig ... end

Sourcemodule FlatConf (Conf : Printable.LiftConf) (Base : Printable.S) : sig ... end

Sourcemodule Flat (Base : Printable.S) : sig ... end

Sourcemodule LiftConf (Conf : Printable.LiftConf) (Base : S) : sig ... end

Sourcemodule Lift (Base : S) : sig ... end

Sourcemodule LiftPO (Conf : Printable.LiftConf) (Base : PO) : sig ... end

Source

module Lift2Conf
  (Conf : Printable.Lift2Conf)
  (Base1 : S)
  (Base2 : S) : 
  sig ... end

Sourcemodule Lift2 (Base1 : S) (Base2 : S) : sig ... end

Source

module ProdConf
  (C : Printable.ProdConfiguration)
  (Base1 : S)
  (Base2 : S) : 
  sig ... end

Sourcemodule Prod (Base1 : S) (Base2 : S) : sig ... end

Sourcemodule ProdSimple (Base1 : S) (Base2 : S) : sig ... end

Sourcemodule Prod3 (Base1 : S) (Base2 : S) (Base3 : S) : sig ... end

Sourcemodule LiftBot (Base : S) : sig ... end

Sourcemodule LiftTop (Base : S) : sig ... end

Sourcemodule Liszt (Base : S) : sig ... end

Sourcemodule type Num = sig ... end

Sourcemodule ProdList (Base : S) (N : Num) : sig ... end

Sourcemodule Chain (P : Printable.ChainParams) : S with type t = int

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.domain/Lattice/index.html

Module `Lattice`Source

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.domain/Lattice/index.html

Module LatticeSource

Module `Lattice`Source