Frama-C Many OCaml programmers use it because it offers a reasonable (to them) compromise between expressivity and control over resources use. Serious OCaml users are often heard complaining about relatively simple optimizations that the compiler does not have. But this reveals as much of the kind of programmers that end up...
Read MoreIf some of the posts in this blog ever get re-organized into a course-style document, this one will be near the beginning, because it's simple and self-contained. The program This example was offered on our bug-tracking system: int putchar(int); void print(const char *ptr) { while (*ptr) putchar(*ptr++); } void putnum(unsigned...
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 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