Specification of loop assigns
Virgile Prevosto on 6 October 2010

A simple example Broadly speaking, every location which is not mentioned in such a clause should have the same value when exiting the corresponding code as it when entering it. For instance, if we take the following declaration (extracted from ACSL by Example) /*@ assigns \ othing; */ bool equal(const...

Read More

Progress of the value analysis tutorial
Pascal Cuoq on 30 September 2010

Boron's value analysis manual has the beginning of a captivating tutorial and I figure that the suspense must be unbearable. I on the other hand already know how it ends. But I'm not telling yet. Neener-neener! Okay maybe later on this blog. The new manual (with an expanded tutorial) will...

Read More

Welcome to the Frama-C blog
Virgile Prevosto on 30 September 2010

Frama-C is an extensible platform dedicated to the analysis of C programs. It provides various plug-ins for navigating in a C code and better understanding its semantics. It can also be used to guarantee the absence of run-time error in a given program. At last, given a specification expressed in...

Read More