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

[Frama-c-discuss] Behaviour allowing to prove 1==2



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;
  }
}