Blog

Loop assigns, part 3: On the importance of loop invariants
Virgile Prevosto on 27 October 2010

Context Last week's post mentioned that it is not possible to prove the following loop assigns with Jessie: void fill(char* a, char x) { //@ loop assigns a, \at(a,Pre)[0..(a-\at(a,Pre)-1)]; for(;*a;a++) *a = x; return; } and in fact this annotation is not provable. An hint to where the issue lies...

Read More

Unspecified behaviors and derived analyses
Pascal Cuoq on 17 October 2010

Prologue The C standard(s) specifies a minimum of things that all C compilers must agree on. For the sake of efficiency, many syntactically correct constructs are left without an unambiguous meaning. The worst way for a construct not to have an unambiguous meaning is to be undefined behavior. An example...

Read More

loop assigns, part 2
Virgile Prevosto on 15 October 2010

Context Last week's post asked how to express a loop assigns for the following code: void fill(char* a char x) { for(;*a;a++) *a = x; return; } The difficulty here is that the pointer a is modified at each step of the loop and that we must take this fact...

Read More

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