Frama-C 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 MoreEvery 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 More