Floating Point Support

Overview

Ultimate is able to verify C and Boogie 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 handled via the "to_fp" function from the STM 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 and return value.

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