Frama-C This new series is dedicated to the verification of the C version of Open Source compression library QuickLZ version 1.5.0 using Frama-C's Value Analysis. The source code can be downloaded from the web site. QuickLZ offers compression and decompression routines using the Lempel-Ziv (LZ) algorithm. Various options are provided at...
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 sort of question (here about the trade-offs involved in the choice of the level of intermediate language to statically analyze) is the reason I still visit StackOverflow despite everything that is wrong with it.
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 More