Frama-C In this sequel to a previous post about numerical precision and the value analysis we tackle another extremely common implementation technique the linear interpolation table. In an attempt to make things less boring the approximated function this time is a sine and takes as its argument a double representing an...
Read MoreFrama-C's value analysis wasn't aimed at verifying numerical precision of C functions when it was conceived. There already was a specialized project for this purpose. However the value analysis needed to handle floating-point computations correctly (that is without omitting any of the possible behaviors the function can have at run-time)...
Read MoreEvery once in a while, someone asks about single-precision floating-point support in Frama-C. Until recently it was often in the context of the value analysis, but actually, thanks to a lot of interesting new results obtained in the context of this project people working on deductive verification within Frama-C can...
Read More