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



Hello,

I would like to prove the property "m[bit] == ((unsigned char)1 <<
(7-(n%8)))" in the following program using WP but I am currently
failing doing so. Any suggestion to help me prove it?

I run WP with:
  frama-c-gui -wp -wp-rte q1_bitshift.c

I have tried to use a more detailed memory model with "-wp-model
"Typed,int" " without success.

I am using Frama-C Fluorine 20130501, Why3 0.81 and Alt-Ergo 0.95.1.

===
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[bit] == ((unsigned char)1 << (7-(n%8)));

  return 0;
}

=====

Best regards,
david