Floating Point Support

Overview

Ultimate is able to verify C programs, which are using floating point data types. This is realized with the Floating Point SMT Theory.

The functions, types and constants are mapped to the appropriate SMT functions using the "builtin" keyword in the Boogie translation. It works only if the Bitvectortranslation is used.

Floating Point Literals are not translated by Ultimate itself, but are handled via the to_fp function from the SMT Theory, which takes a Real Literal and a Rounding Mode (in this case RNE/RoundNearestTiesToEven) as arguments and translates it to the according float.

Every Boogie function name is suffixed with one of the floating types (FLOAT, DOUBLE, LONGDOUBLE), depending on which type is used as argument. This solves the problem of Boogies missing capability to overload functions by creating functions for each used argument type separately. Semantically equivalent functions (e.g. fp.addFLOAT, fp.addDOUBLE, fp.addLONGDOUBLE) are all translated to the same SMT-Function, which supports overloading.

At the moment, every function uses the RNE Rounding Mode, which is the default behavior in C, except for the conversion functions from floating to int types, which use RTZ (RoundTowardsZero) to simulate the integer truncation.

Usage

Some ultimate settings are needed to work with floating types:

• Automizer (Trace Abstraction)
  • use separate solver for trace checks
  • Logic for external solver: QF_BVFP
• C+ACSL to Boogie Translator
  • use bitvectors instead of ints
• RCFGBuilder
  • Logic for external solver: QF_BVFP