Blog

Tag Archives: value

Helping the value analysis — part 1
Pascal Cuoq on 23 March 2011

Introduction This post introduces a new series about the art of helping the value analysis to be more precise. Until now, in the numerical precision series of this blog, this was easy enough. There was a single input variable and the obvious way to get more precise output values was...

Read More

This time for real: verifying function cosine
Pascal Cuoq on 3 March 2011

This post follows that post where a typical double-precision implementation for a cosine function is shown. That implementation is not a correctly rounded implementation but its double result is precise to a level close to what the double-precision floating-point representation allows. It uses low-level tricks that make it faster on...

Read More

Analyzing unit tests and interpretation speed
Pascal Cuoq on 1 March 2011

I once claimed in a comment that with the value analysis, when the source code is fully available, you can analyze many executable C programs with maximum precision. For this to work, all inputs must have been decided in advance and be provided. It can therefore be likened to running...

Read More

On switch statements
Pascal Cuoq on 28 February 2011

In Carbon 20110201 and earlier versions of Frama-C, if you do not use precautions when analyzing a program with switch statements, you get imprecise results. Consider the example program below. main(int argc, char **argv){ switch(argc){ case 1: Frama_C_show_each_no_args(argc); break; case 2: Frama_C_show_each_exactly_2(argc); /* fall through */ case 3: Frama_C_show_each_2_or_3(argc); break;...

Read More

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