module type Lattice =sig
..end
type
state
val top : state
val is_included : state -> state -> bool
val join : state ->
state -> state
val join_and_is_included : state ->
state -> state * bool
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