--- layout: fc_discuss_archives title: Message 73 from Frama-C-discuss on August 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proving a simple property on bitshift with WP



Hi,

Coupling Value and WP to the extensive annotations below (discharged by Value) also allows to discharge the last assert by WP.
(This is a very verbose solution, indeed, but might be still readable)
HTH,
D.

frama-c-gui -val -wp -wp-rte bits.c

//-----------------------------------------------

static unsigned char m[] = { (1 << 7), (1 << 6), (1 << 5), (1 << 4), (1 << 3), (1 << 2), (1 << 1), (1 << 0) };

/*@ requires n >= 0;  */
int main(int n)
{
  int size, bit;

  size = 8;
  bit = n%size;
  //@ assert 0 <= bit <= 7;

  //@ assert m[0] == ((unsigned char)(1 << 7));
  //@ assert m[1] == ((unsigned char)(1 << 7-(1%8)));
  //@ assert m[2] == ((unsigned char)(1 << 7-(2%8)));
  //@ assert m[3] == ((unsigned char)(1 << 7-(3%8)));
  //@ assert m[4] == ((unsigned char)(1 << 7-(4%8)));
  //@ assert m[5] == ((unsigned char)(1 << 7-(5%8)));
  //@ assert m[6] == ((unsigned char)(1 << 7-(6%8)));
  //@ assert m[7] == ((unsigned char)(1 << 7-(7%8)));
  //@ assert m[bit] == ((unsigned char)1 << (7-(n%8)));

  return 0;
}

> -----Message d'origine-----
> De?: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-
> discuss-bounces at lists.gforge.inria.fr] De la part de David MENTRE
> Envoy??: jeudi 29 ao?t 2013 15:48
> ??: Frama-C public discussion
> Objet?: Re: [Frama-c-discuss] Proving a simple property on bitshift
> with WP