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 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

val narrow : state ->
state -> state Eval.or_bottom

Over-approximation of the intersection of two abstract states (called meet in the literature). Used only to gain some precision when interpreting the complete behaviors of a function specification. Can be very imprecise without impeding the analysis: meet x y = `Value x is always sound.