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.