Frama-C This post follows that post. It is a brief survey of the alarms obtained when analyzing donut.c such as a programmer might do when ey is only trying to find bugs or in the context of verification as a first step to get an estimate on the difficulty of the...
Read MoreA facetious colleague reports the following program as a bug: int main () { signed char c=0; while(1) c++; return 0; } The commandline frama-c -val -val-signed-overflow-alarms charpp.c, he says, does not emit any alarm for the c++; instruction. Indeed, the c++; above is equivalent to c = (signed char)...
Read MoreHere's a cool obfuscated C program by Andy Sloane that draws a revolving donut. You know where this is heading... I am going to suggest that someone should verify it. I will get us started. 1. Download the code 2. Determine what library functions it needs: $ frama-c -metrics donut.c...
Read MoreThis post is a backward changelog that introduces actual new features. Beat that, Emacs 19 Antinews! Shortly after the release of Carbon, I offered to my Frama-C co-developers the idea of a great clean-up of the value analysis for the next release. This would not immediately add new features (indeed,...
Read MoreJohn Gruber writes about new release 10 of text editor BBEdit: I’ve been beta-testing 10 for months and at this point I couldn’t bear to go back to version 9. Wow! I would hate an editor that come a new release puts you in a position to say things like...
Read More