Module Framac_ivalSource

Sourcemodule Abstract_interp : sig ... end

Functors for generic lattices implementations. @plugin developer guide

Sourcemodule Bottom : sig ... end

Types, monads and utilitary functions for lattices in which the bottom is managed separately from other values.

Sourcemodule Fc_float : sig ... end

Implementation of floating-point values of different precision, using the standard ocaml floating-point numbers in double precision. Long_Double and Real are inexact.

Sourcemodule Float_interval : sig ... end
module Float_interval_sig : sig ... end

Signature for the floating-point interval semantics.

module Float_sig : sig ... end

Interface of floating-point numbers of different precisions.

Sourcemodule Floating_point : sig ... end

Floating-point operations.

Sourcemodule Fval : sig ... end

Floating-point intervals, used to construct arithmetic lattices. The interfaces of this module may change between Frama-C versions. Contact us if you need stable APIs.

Sourcemodule Integer : sig ... end

Extension of Big_int compatible with Zarith.

Sourcemodule Ival : sig ... end

Arithmetic lattices. The interfaces of this module may change between Frama-C versions. Contact us if you need stable APIs.

Sourcemodule Ival_noinf : sig ... end

Arithmetic lattices. The interfaces of this module may change between Frama-C versions. Contact us if you need stable APIs.

Sourcemodule Pretty_utils : sig ... end