--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Small function with Shifting



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?