Frama-C In a blog post earlier this year, John Regehr wonders when software verification will finally matter. He means “formal verification”, I am pretty sure. “Verification” is what practitioners of, say, the software development V-cycle have been doing for decades, and it has kept us safe for that long—at least, when...
Read MoreI know! Let us make [ and ] function as meta-characters when in code style. Users will surely love the ability to insert hyperlinks inside the code they are writing a blog post about. —The authors of the Content Management System this blog relies on In the previous post, (float){…},...
Read MoreYesterday's quiz was about the expression *(char*)(float[]){x*x} - 63 (for big-endian architectures) or *(3+(char*)(float[]){x*x}) - 63 (for little-endian ones). This post provides an explanation. First, let us try the function on a few values: int main(){ for (unsigned int i=0; i<=20; i++) printf(\l(%2u)=%d" i l(i)); } This may provide the...
Read MoreA remark I have not heard about the last two posts is the following. Pascal, how can you, in your last post claim that formal verification would have found the bug in your decimal-to-floating-point function? This is the kind of outrageous claim you rant against in your penultimate post! Formal...
Read More