Tag Archives: conversions-and-promotions

The overflow when converting from float to integer is undefined behavior
Pascal Cuoq on 9 October 2013

Integer overflows in C A previous post on this blog was a reminder that in C signed integer arithmetic overflow is undefined behavior. In contrast the behavior of overflows in conversions from integer type to signed integer type is implementation-defined. The C99 standard allows for an implementation-defined signal to be...

Read More

Function pointers in C
Pascal Cuoq on 24 August 2013

This post contains a complete list of everything a C program can do with a function pointer, for a rather reasonable definition of “do”. Examples of things not to do with a function pointer are also provided. That list, in contrast, is in no way exhaustive. What a C program...

Read More

Arithmetic overflows in Fluorine
Pascal Cuoq on 9 July 2013

There is a C quiz in the middle of this post, lost in the middle of all the reminiscing. A history of arithmetic overflows in Frama-C From the very beginnings in 2005, until after the first Open Source release in 2008, Frama-C's value analysis was assuming that all arithmetic overflows...

Read More

Sign extension
Pascal Cuoq on 25 April 2013

There is no “sign extension” in C. Please stop referring to “sign extension” in C programs. In assembly, there is such a thing as “sign extension” Sign-extend is an assembly instruction say movsx %al %ebx to transfer the contents of a narrow register say %al to a wide register say...

Read More

Portable modulo signed arithmetic operations
Pascal Cuoq on 26 February 2013

In a recent post, John Regehr reports on undefined behaviors in Coq! In Coq! Coq! Exclamation point! Coq is a proof assistant. It looks over your shoulder and tells you what remains to be done while you are elaborating a mathematical proof. Coq has been used to check that the...

Read More