Frama-C:
Plug-ins:
Libraries:

Frama-C API - Lattice_bounds

Types, monads and utilitary functions for lattices in which the bottom and/or the top are managed separately from other values.

type 'a or_bottom = [
  1. | `Value of 'a
  2. | `Bottom
]
type 'a or_top = [
  1. | `Value of 'a
  2. | `Top
]
type 'a or_top_bottom = [
  1. | `Value of 'a
  2. | `Bottom
  3. | `Top
]
module Bottom : sig ... end
module Top : sig ... end
module TopBottom : sig ... end