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

  • Subject: [Frama-c-discuss] Behaviour allowing to prove 1==2
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Fri, 13 Dec 2013 16:13:02 +0100
Hello,

In the attached program, we have no assumption and everything is proved 
with WP (Frama-C Fluorine June), including the assert 1==2 in case N!

   frama-c-gui -pp-annot -wp -wp-rte q19_switch_fun_call.c

It appears that the issue is coming from the equivalences used in the 
behaviours of compute_trans(). If we replace "<==>" by "==>", then the 
1==2 assert is not proved (substitute call to compute_trans() by 
compute_trans2() in main()).

In both cases (compute_trans() and compute_trans2()), the contract is 
always proved.

When 1==2 is proved, it appears that we have "Have: false" in 
corresponding VC, as if all the cases in the switch were considered not 
taken.

We have two questions:

  1. Could somebody explain us what is really occurring in this case? We 
do not understand from where the contradiction is coming from.

  2. Is there a methodology to avoid this situation? I though than when 
everything is green without any assumption, then we are sure that 
everything is correct.

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 1==2;
    return -1;
    break;

  case A:
    return 1;
    break;

  case B:
    return 2;
    break;

  default:
    return -1;
    break;
  }
}