Blog

Value analysis tutorial, part 3: answering one quiz
Pascal Cuoq on 15 October 2010

This is another episode in the advanced value analysis tutorial. The first episode was here and the second one here. There were a couple of questions left unanswered at the break. This post answers the first one. Quiz 1: continuing the study of the first five calls to Skein_256_Update what...

Read More

Value analysis tutorial, part 2
Pascal Cuoq on 7 October 2010

In order to create a tradition of providing solutions to previous quizzes, this post is a partial answer to the question in this one about Frama-C's value analysis. To recap: at the end of the Boron tutorial we arrive at the main function below. This function is useful as an...

Read More

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