Frama-C Yesterday's quiz was about the expression *(char*)(float[]){x*x} - 63 (for big-endian architectures) or *(3+(char*)(float[]){x*x}) - 63 (for little-endian ones). This post provides an explanation. First, let us try the function on a few values: int main(){ for (unsigned int i=0; i<=20; i++) printf(\l(%2u)=%d" i l(i)); } This may provide the...
Read MoreIn a previous post almost exactly one year ago before Frama-C Oxygen was released I mentioned that the then future release would incorporate a custom decimal-to-binary floating-point conversion function. The reason was that the system's strtof() and strtod() functions could not be trusted. This custom conversion function is written in...
Read MoreAn old rant: misusing Ariane 5 in motivation slides I was lucky to be an intern and then a PhD student at INRIA, while it was still called “INRIA” (it is now called “Inria”). This was about when researchers at INRIA and elsewhere were taken to task to understand the...
Read MoreWhen researchers start claiming that they have a sound and complete analyzer for predicting whether a program statement is reachable, it is time to build a database of interesting programs. Goldbach's conjecture My long-time favorite is a C program that verifies Goldbach's conjecture (actual program left as an exercise to...
Read More