Frama-C:
Plug-ins:
Libraries:

Frama-C API - Lattice

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.

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.