Frama-C This post follows that post. For cases 2 and 3 in order to get more complete execution traces we again take advantage of Frama_C_dump_each(). Before launching the analysis we insert a call to this primitive right at the end of RoCo_process() so that local variables of that function will be...
Read MoreHow it started In the last post we started a new series about helping the value analysis be more precise. We introduced an interpolation function with the goal of verifying that it is free of run-time errors. Having launched a first value analysis we got one alarm we need to...
Read MoreIntroduction 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 MoreThis 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 MoreIn a previous post there was a cosine function that I made up for the purpose of blogging about it. Let us now look at a real cosine function (OpenBSD's libm derived from widespread code written at Sun in the 1990s) to get a feeling how far off we were:...
Read More