Frama-C I do not expect that many people are diligently working at this time of year, and this is my excuse for posting this series of productivity-wasting links. Some of them are even on-topic. For those who missed it, GNU/Linux Magazine/France has a summer special [removed dead link] on the C...
Read MoreHey, I left out one alarm last time: donut.c:15 ... out of bounds read. assert \valid(". -~:;=!*#$@"+tmp_7); This corresponds to ". -~:;=!*#$@"[N>0?N:0] in the obfuscated code. I wanted to have a blog post about this construct in particular because I was curious whether it would break the content management system's...
Read MoreCsmith that I mentioned earlier in this blog is a random generator of C programs. That much sounds easy but it generates only well-defined programs which two or more compilers have no excuse for compiling into executables that produce different results. And it generates varied and interesting enough C programs...
Read MoreThis 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 More