Module type Abstract_domain.Lattice

module type Lattice = sig .. end

Lattice structure of a domain.

type state

val top : state

Greatest element.

val is_included : state -> state -> bool

Inclusion test.

val join : state ->
       state -> state

Semi-lattice structure.

val join_and_is_included : state ->
       state -> state * bool

Do both operations simultaneously

val widen : Cil_types.kernel_function ->
       Cil_types.stmt ->
       state ->
       state -> state

widen h t1 t2 is an over-approximation of join t1 t2. Assumes is_included t1 t2