Frama-C API - `Abstract_interp`

Functors for generic lattices implementations.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val feedback_approximation : ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a

exception Error_Top

Raised by some functions when encountering a top value.

exception Error_Bottom

Raised by Lattice_Base.project.

exception Not_less_than

Raised by Lattice.cardinal_less_than.

exception Can_not_subdiv

Used by other modules e.g. Fval.subdiv_float_interval.

type truth =

| True
| False
| Unknown
(*
Truth values with a possibility for 'Unknown'
*)

val inv_truth : truth -> truth

module Comp : sig ... end

Signatures for comparison operators ==, !=, <, >, <=, >=.

module Int : sig ... end

module Rel : sig ... end

"Relative" integers. They are subtraction between two absolute integers

module Make_Lattice_Set (V : Datatype.S) (Set : Lattice_type.Hptset with type elt = V.t) : Lattice_type.Lattice_Set with module O = Set

module Make_Hashconsed_Lattice_Set (V : Hptmap.Id_Datatype) (Set : Hptset.S with type elt = V.t) : Lattice_type.Lattice_Set with module O = Set

See e.g. base.ml and locations.ml to see how this functor should be applied. The O module passed as argument is the same as O in the result. It is passed here to avoid having multiple modules calling Hptset.Make on the same argument (which is forbidden by the datatype library, and would cause hashconsing problems)

Frama-C API - Abstract_interp

Frama-C API - `Abstract_interp`