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