Frama-C One unexpected consequence of writing semi-regularly in a blog, in addition to the other bits of writing that I have to do, is that I am starting to hate my own style. It feels like English sentences always come out my fingers with the same rhythm to them. Precisely dull....
Read MoreI 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 More