--- layout: fc_discuss_archives title: Message 80 from Frama-C-discuss on May 2010 ---
Michael Schausten wrote: > 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? > 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; } -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |