--- layout: fc_discuss_archives title: Message 80 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



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                    |