Blog

Documentation
Pascal Cuoq on 10 December 2010

So it may seem that I have a pretty good job for having nothing more important to worry about —that may or may not be accurate— but I worry about the state of the Frama-C documentation in general and of the value analysis in particular. I hate noticing that it's...

Read More

Unspecified behaviors and derived analyses, part 2
Pascal Cuoq on 4 December 2010

Context This post is a sequel and conclusion to this remark. Example of derived analysis: slicing When writing a Frama-C plug-in to assist in reverse-engineering source code it does not really make sense to expect the user to check the alarms that are emitted by the value analysis. Consider for...

Read More

Value analysis tutorial, part 5: jumping to conclusions
Pascal Cuoq on 22 November 2010

This post is in two parts, both of them independently good fits for the title, and still not completely without relation to each other, but that's probably a coincidence. Methodology In this thread, we aim at the verification of low-level properties for the functions in Skein. In the last post,...

Read More

Value analysis tutorial, part 4: one solution to second quiz
Pascal Cuoq on 21 November 2010

This post offers one answer to the second quiz from part 2. For context here are links to part 1 and part 3. The question was: how should we get rid of the last alarm below and conclude that Skein-256 is indeed safe from run-time errors when used in the...

Read More

IEEE 754 single-precision numbers in Frama-C
Pascal Cuoq on 20 November 2010

Every once in a while, someone asks about single-precision floating-point support in Frama-C. Until recently it was often in the context of the value analysis, but actually, thanks to a lot of interesting new results obtained in the context of this project people working on deductive verification within Frama-C can...

Read More