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.