Frama-C:
Plug-ins:
Libraries:

Frama-C API - Numerors_arithmetics

type t = {
  1. exact : I.t;
  2. approx : I.t;
  3. abs_err : I.t;
  4. rel_err : I.t;
}

Type manipulated by the arithmetics

val pretty : Stdlib.Format.formatter -> t -> unit

Pretty printer

val zero : t -> t

Return a value with all fields to zero. The <approx> field will use the precision of the approx field of the parameter

Return the precision of the <approx> field

val create : I.t -> I.t -> I.t -> I.t -> t

Create a record from intervals

val apply : (I.t -> I.t -> I.t) -> t -> t -> t

Apply an operation on each fields of the operands

val change_prec : Numerors_utils.Precisions.t -> t -> t

Return a new value with the same fields as the input but with an <approx> field with the given precision

val forward_interaction : t -> t

Handling of forward interactions

val join : t -> t -> t

Lattice methods

val narrow : t -> t -> t Eva.Eval.or_bottom
val compare : t -> t -> int
val is_included : t -> t -> bool
module type Arithmetic = sig ... end

Signature of an arithmetic

module Exact : Arithmetic with type forward = I.t

Modules which implement the previous signature for each field of <t>

module Approx : Arithmetic with type forward = I.t
module Abs_Err : Arithmetic with type forward = exact:I.t -> approx:I.t -> I.t
module Rel_Err : Arithmetic with type forward = exact:I.t -> abs_err:I.t -> I.t
module Backward_Comparisons : sig ... end

Backward comparisons