Logo Hisseo

Effect of rounding on decimal literals

The very first caveat one encounters with floating-point calculations is that decimal contants might not be represented exactly.

The following short code illustrates this issue.

#pragma JessieFloatModel(strict)

//@ ensures \result == 7.0;
double test1() {
  return 2.0 * 3.5;

//@ ensures \result == 0.100000001490116119384765625;
float test2() { 
  return 0.1f;

This is proved entirely by the Jessie plugin of the Frama-C environement, thanks to the use of the Gappa prover as back-end. Other SMT solvers are proving part of the verification conditions, but not the ones involving floating-point rounding.