--- layout: fc_discuss_archives title: Message 81 from Frama-C-discuss on May 2010 ---
Claude Marche schrieb: > You are assuming that every true property is provable. > > SMT provers have almost no knowledge of shift operations, so you need > to give hints to them under the form of a lemma. > Here is your example below, slightly modified/simplified. > > The lemma itself is not proved of course, you have to convince > yourself of its truth by other means: from human review to use of a > proof assistant. > > - Claude > > #pragma JessieIntegerModel(math) > > typedef struct s1 { unsigned int mantissa; int exponent; }; > > /*@ lemma shift_prop: \forall integer x,y; > y >= 8 ==> > (x << 8) * (1 << (y-8)) == x * (1 << y); > */ > > /*@ requires \valid(e); > @ requires 0 < e->mantissa < 10; > @ requires 10 < e->exponent < 20; > @ ensures > @ e->mantissa * (1 << e->exponent) == \old(e->mantissa * (1 << > 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; > } > Using the lemma as a "precondition" worked for the example, although I'm not yet alltogether content with it,since it is not a totally formal prove of course. But thank you for the hint. I then tried it with the next part myself, with another lemma. It didn't work, though i think I used the technique the same way you did: #pragma JessieIntegerModel(math) typedef struct s1 { unsigned int mantissa; int exponent; }; /*@ lemma shift_prop: \forall integer x,y; y >= 8 ==> (x << 8) * (1 << (y-8)) == x * (1 << y); */ /*@ lemma shift_prop2: \forall integer x,y; ((x >> 3) + 1) * (1 << (y + 3)) >= x * (1 << y); */ /*@ requires \valid(e); @ ensures e->mantissa * (1 << e->exponent) >= \old(e->mantissa * (1 << e->exponent)); */ int sizetype_normalize(struct s1* e) { unsigned int min_mantissa = 1 << 21; unsigned int max_mantissa = 1 << 29; if (e->mantissa < min_mantissa) { e->mantissa <<= 8; e->exponent -= 8; } if (e->mantissa >= max_mantissa) { e->mantissa = (e->mantissa >> 3) + 1; e->exponent += 3; } return 0; } Could you explain to me what is wrong here? Lemma2 states (in my opinion) exactly what is done in the second if-condition.