Frama-C:
Plug-ins:
Libraries:

Frama-C API - IEEE754_sig

This module provides the type definitions and module signatures used by the IEEE754 module to build an abstract semantics of floating-point computations as defined by the IEEE-754 standard. See this module for more information.

Miscellaneous definitions.

type 'a correctly_rounded_expression =
  1. | Cast of 'a
  2. | Sqrt of 'a
  3. | Add of 'a * 'a
  4. | Sub of 'a * 'a
  5. | Mul of 'a * 'a
  6. | Div of 'a * 'a

Type encoding correctly rounded operations. Values of this type are provided to the model when asked to represent elementary rounding errors. Relational abstractions may use them to keep track of the relations between rounding errors during the analysis.

type resulting_format =
  1. | Format : 'f Frama_c_kernel.Typed_float.format -> resulting_format

Existential type on format.

module type Computation = sig ... end

Abstract values may be context dependent, which can be easily represented using a monad. This signature extends monads signature with a resolve function, that must be able to concretize a monadic computation on a given context.

Abstract representation of subsets over a field.

module type Abstraction = sig ... end

Modeling used to abstract the IEEE-754 semantics.

module type Modeling = sig ... end