Tag Archives: floating-point

Verifying numerical precision with Frama-C's value analysis — part 2
Pascal Cuoq on 10 February 2011

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 More

Verifying numerical precision with Frama-C's value analysis
Pascal Cuoq on 22 January 2011

Frama-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 More

IEEE 754 single-precision numbers in Frama-C
Pascal Cuoq on 20 November 2010

Every 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