Frama-C API - `Model`

The field over which the abstraction is defined.

module Scalar : Frama_c_kernel.Field.S

type scalar = Scalar.t

The monad used to encode context dependent computations.

It must rely on a context that respects Abstract_context.Leaf.

module Context : sig ... end

module Computation : sig ... end

type 'a computation = 'a Computation.t

Abstraction used for the exact and absolute errors semantics.

module Additive : sig ... end

module Exact = Additive

type exact = Exact.t

module Absolute = Additive

type absolute = Absolute.t

Abstraction used for the relative errors semantics.

module Multiplicative : sig ... end

module Relative = Multiplicative

type relative = Relative.t

Reduced product and other miscellaneous values.

val name : string

Name of the resulting abstract domain.

val new_absolute_elementary_error : exact Eva__.IEEE754.correctly_rounded_expression -> scalar -> absolute computation

The call new_absolute_elementary_error expr bound returns a computation of the absolute abstraction of the elementary rounding error that would be produced by the computation of expr and is bounded by bound.

val new_relative_elementary_error : exact Eva__.IEEE754.correctly_rounded_expression -> scalar -> relative computation

The call new_relative_elementary_error expr bound returns a computation of the relative abstraction of the elementary rounding error that would be produced by the computation of expr and is bounded by bound.

val do_reduce_absolute_with_relative : unit -> bool

The call do_reduce_absolute_with_relative () returns true if and only if the analysis is configured to reduce the absolute errors using the relative error bounds.

val do_reduce_relative_with_absolute : unit -> bool

The call do_reduce_relative_with_absolute () returns true if and only if the analysis is configured to reduce the relative errors using the absolute error bounds.

val recompute_absolute : exact:exact -> relative:relative -> absolute computation

The call recompute_absolute ~exact ~relative returns a computation of absolute error bounds as deduced from exact and relative, respectively representing the exact semantics and the relative error semantics. It will be used if the reduced product is configured to reduce the absolute errors using the relative error bounds.

val recompute_relative : exact:exact -> absolute:absolute -> relative computation

The call recompute_relative ~exact ~absolute returns a computation of relative error bounds as deduced from exact and absolute, respectively representing the exact semantics and the absolute error semantics. It will be used if the reduced product is configured to reduce the relative errors using the absolute error bounds.

val a_x_plus_b_y_over_x_plus_y : a:relative -> x:exact -> b:relative -> y:exact -> relative computation