Frama-C:
Plug-ins:
Libraries:

Frama-C API - Field

This module provides a generic signature describing mathematical fields, i.e algebraic structure that behave like rationals, reals or complex numbers. The signature also provides several functions that are not directly part of fields definition, but are useful nonetheless, in particular when using fields to model floating point computations.

  • since Frama-C+dev
type 't bounds = {
  1. lower : 't;
  2. upper : 't;
}

This type is used to return bounds for mathematical functions that cannot be exactly computed using rationals, like the square root for instance.

module type S = sig ... end