Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

Hello Virgile,

2013/8/29 Virgile Prevosto <virgile.prevosto at m4x.org>:
> I'm afraid that WP tries to play it a bit too smart here: if you look
> at the generated goal, you'll see that the values of the m[i] have
> been const-folded, so that you have m[0] == 128, m[1] == 64, etc. It
> makes the assert on m[0] trivial, but
> the assert on m[bit] much more complicated, as the prover somehow has
> to revert back the transformation. Since we're dealing with a bitwise
> rather than an arithmetic operation, I'm not sure that there's an easy
> way to have alt-ergo prove that.

Argh!! Thank you for the explanation!

I found an overkill way to prove the property by building it manually
and putting it as requirement of the function of interest (see below).
I also need to call WP with -wp-model "Typed,int".

Even if now everything is proved, this is ugly and much less readable
than the original program. :-(

I also thought of combining Value analysis and WP to do the same kind
of thing as below program, but using Value to prove the property on
the static version of m[]. Unfortunately, Value seems unable to reason
on \forall quantifier and I see no other way to express the property.

A third approach would be to attach a global invariant to the static m
(and still require the property at f() entrance):
 global invariant my_m:
       \forall integer i; 0 <= i  < 8 ==> m[i] == (1 << (7-i));
Unfortunately, WP does not seem to support it (and probably would have
the same issue to prove it).

====

unsigned char m[8];

/*@ requires n >= 0;
    requires \forall integer i; 0 <= i  < 8 ==> m[i] == (1 << (7-i));
 */
int f(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;
}

int main(int n)
{
  int i;

  if (n < 0) return -1;

  /*@ loop invariant 0 <= i <= 8;
      loop invariant \forall integer j; 0 <= j < i ==> m[j] == (1 << (7-j));
      loop invariant n >= 0;
   */
  for (i=0; i<8; i++) {
    m[i] = (1 << (7-i));
  }
  //@ assert \forall integer i; 0 <= i  < 8 ==> m[i] == (1 << (7-i));

  f(n);
  return 0;
}
====

Best regards,
david