float to int conversion

["Warlich, Christof" <christof dot warlich at siemens dot com>]

Hi,
 
imho, float to int conversion is wrong when the float exceeds the integer range:
 
$ cat test1.c
#include <stdio.h>
int main() {
    float a = 1.23e24f;
    printf("%d, %d\n", (int) a, (int) 1.23e24f);
    return 0;
}
 
$ gcc test1.c
$ ./a.out
-2147483648, 2147483647
 
The problem even occurs when being close to, but still within the integer range:
 
$ cat test2.c
#include <stdio.h>
int main() {
    float c = 0x7fffffbf;
    float d = 0x7fffffc0;
    printf("%d, %d\n", (int) c, (int) d);   
    return 0;
}
 
$ gcc test2.c
$ ./a.out
2147483520, -2147483648
 
In both cases, the problem disappears with optimization turned on, so a workaround
is easy, e.g.
  
$ gcc -O1 test2.c
$ ./a.out
2147483520, 2147483647
 
Is this a (known) bug, shall it be reported? I this with several versions of gcc at hand
under both Linux and MinGW, i.e. V4.2.3, 4.5.4 and 4.7.2.
 
Thanks for your suggestions,
 
Chris