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 MoreI like to think the sentence this post borrows as title is one of the most condensed jokes in The Hitch-Hiker's Guide to the Galaxy series, if one takes the sentence to mean "Pick any number using an uniform probability". It may seem that I am over-interpreting, and perhaps I...
Read MoreA little while ago, I was commenting somewhere that Forth had the ultimate control structure, the BEGIN (1) WHILE (2) REPEAT construction. (1) and (2) are holes to be filled with programs. WHILE takes an evaluated condition from the stack, so that (1) can usually be divided into (1a): do...
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 MoreCsmith testing A typical Frama-C Csmith testing script repeats four actions in an infinite loop: getting a random program from Csmith; compiling and executing it; analyzing it with Frama-C; using the results from step 3, possibly together with those of step 2, to determine whether the program reveals something that...
Read More