Possible undefined behaviour while bitcasting floats and integers
tomsik68 opened this issue · 2 comments
When casting floats to integers(or vice versa), semantics of LLVM bitcast instruction differ from semantics of C cast.
Consider this program:
float a = 123.25;
unsigned int i = (unsigned int) a;
printf("%d", i);It outputs 123, because C cast truncates the decimal part of the float and then converts IEEE754 representation to integer representation. However, this doesn't preserve bits of the value (which LLVM bitcast does).
It was addressed in commit: f3d232d .
The solution is this:
float a = 123.25;
unsigned int i = *((unsigned int*) &a);There is a potential problem with this solution: Casting float pointers to integer pointers has undefined behaviour in the C standard.
One correct solution would be to use an intermediate union for the conversion, like this:
typedef union {
float f;
unsigned int word;
} aux;
float a = 123.25;
aux uni;
uni.f = a;
unsigned int i = uni.word;
printf("%d", i);The resulting program works as intended, but CPAchecker doesn't accept this way of converting it via pointers. CPAchecker doesn't accept conversion via memcpy either. Conversion via unions is necessary to solve this issue.
The resulting program verifies correctly in CBMC.