--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on May 2010 ---
Hello, I'm not successfull verifying the following piece of code: #include <math.h> #pragma JessieIntegerModel(math) typedef struct s1 { unsigned int mantissa; int exponent; }; /*@ requires (0 < (*e).mantissa < 10) && (10 < (*e).exponent < 20); ensures ((*e).mantissa * (1 << (*e).exponent)) == (\old((*e).mantissa) * (1 << \old((*e).exponent))); */ int sizetype_normalize(struct s1* e) { unsigned int min_mantissa = 1 << 21; if ((*e).mantissa < min_mantissa) { (*e).mantissa <<= 8; (*e).exponent -= 8; } return 0; } The computation actually is mantissa * 2^exponent. When i shift the mantissa 8 bits to the left, but therefore decrease the exponent by 8, the result should be the same as before. However, Alt-Ergo can't prove this. What am I doing wrong?