Frama-C 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 MoreContext 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 MorePrologue 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 MoreContext 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 MoreThis 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