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] RE : Behaviour allowing to prove 1==2

Hello Lo?c,

Le 16/12/2013 11:11, CORRENSON Loic 218851 a ?crit :
> Due to WP simplifications, (assert 1==2) is always translated locally in (assert \false).
> In the behaviors, repeating the assumes clause in the requires, be it with (==>) or (<==>) is useless.

Yes. We are going to simplify those annotations following you remarks.

> In the generated proof obligations, removing the (assert \false) clause, you can see that all then generated proof obligations are correct, using the two variants (with ==> or with <==>). Moreover, you can notice that in the (==>) case, the assumes clause is not repeated.

Well, we don't think the generated PO are correct, for at least some of 
them. If you look at the attached file, we are able to prove x > 0 and x 
< 0 in a row within the switch case. In fact, both VC have "Have: false" 
in hypothesis.

This is how we discovered the issue, in our real code we have more 
complex code in the switch cases and they were proved a bit too easily. :-)

> I suspect the bug to come from late simplification stage of WP.
> Using -wp-no-let turns off the bug.

Thanks, that gives us a workaround.

> I opened an issue in the BTS :http://bts.frama-c.com/view.php?id=1586

Thanks, I have added this example.

Best regards,
david

-------------- next part --------------

typedef enum {N, A, B} trans_t;

/*@ behavior more_than_five:
      assumes x > 5;
      ensures x > 5 <==> \result == A;

    behavior less_than_five:
      assumes x >= 0 && x <= 5;
      ensures (x >= 0 && x <= 5) <==> \result == B;

    behavior none:
      assumes x < 0;
      ensures x < 0 <==> \result == N;

   complete behaviors;
   disjoint behaviors;
 */
trans_t compute_trans(int x)
{
  if (x > 5)
    return A;
  else if (x >= 0)
    return B;
  else
    return N;
}

/*@ behavior more_than_five:
      assumes x > 5;
      ensures x > 5 ==> \result == A;

    behavior less_than_five:
      assumes x >= 0 && x <= 5;
      ensures (x >= 0 && x <= 5) ==> \result == B;

    behavior none:
      assumes x < 0;
      ensures x < 0 ==> \result == N;

   complete behaviors;
   disjoint behaviors;
 */
trans_t compute_trans2(int x)
{
  if (x > 5)
    return A;
  else if (x >= 0)
    return B;
  else
    return N;
}

/*@ ensures \result == -1 || \result == 1 || \result == 2;
 */
int main(int x)
{
  trans_t trans = N;

  trans = compute_trans(x);

  switch(trans) {
  case N:
    //@ assert x < 0;
    //@ assert x > 0;
    return -1;
    break;

  case A:
    return 1;
    break;

  case B:
    return 2;
    break;

  default:
    return -1;
    break;
  }
}