Tag Archives: floating-point

Solution to yesterday's quiz
Pascal Cuoq on 29 November 2012

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 More

C99 quiz
Pascal Cuoq on 28 November 2012

Here is a convenient one-liner: int l(unsigned int x) { return *(char*)(float[]){x*x} - 63; } What does it do on my faithful PowerMac? The Intel version is not as nice. That's progress for you: *(3+(char*)(float){x*x}) - 63

Read More

Funny floating-point bugs in Frama-C Oxygen's front-end
Pascal Cuoq on 19 November 2012

In 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 More

About the rounding error in these Patriot missiles
Pascal Cuoq on 18 November 2012

An 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 More

Short, difficult programs
Pascal Cuoq on 2 November 2012

When 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