2021-02-24 18:31 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001586Frama-CPlug-in > wppublic2013-12-16 11:102014-03-13 15:57
Reportercorrenson 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001586: Bug in let-elimination (due to <==> and assert false).
DescriptionBug in let-elimination (due to <==> and assert false).
Using -wp-no-let makes the assert false not-proved as expected.
Additional InformationIn 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.
TagsNo tags attached.
Attached Files
  • c file icon q19_switch_fun_call.c (1,335 bytes) 2013-12-16 11:10 - 
    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 \false;
    return -1;
    break;

  case A:
    return 1;
    break;

  case B:
    return 2;
    break;

  default:
    return -1;
    break;
  }
}
    c file icon q19_switch_fun_call.c (1,335 bytes) 2013-12-16 11:10 +
  • c file icon q20_switch_fun_call.c (1,276 bytes) 2013-12-16 11:45 - 
    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;
  }
}
    c file icon q20_switch_fun_call.c (1,276 bytes) 2013-12-16 11:45 +

-Relationships
+Relationships

-Notes

~0004377

dmentre (reporter)

2013-12-16 11:46

 Another example added. VC for "assert x > 0;" has False in hypothesis.

~0004505

correnson (manager)

2014-02-05 16:29

 Fix committed to master branch.

~0004533

correnson (manager)

2014-02-12 16:57

 Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2013-12-16 11:10 correnson New Issue
2013-12-16 11:10 correnson Status new => assigned
2013-12-16 11:10 correnson Assigned To => correnson
2013-12-16 11:10 correnson File Added: q19_switch_fun_call.c
2013-12-16 11:45 dmentre File Added: q20_switch_fun_call.c
2013-12-16 11:46 dmentre Note Added: 0004377
2014-02-05 16:29 correnson Source_changeset_attached => framac master 65bc56b6
2014-02-05 16:29 correnson Note Added: 0004505
2014-02-05 16:29 correnson Status assigned => resolved
2014-02-05 16:29 correnson Resolution open => fixed
2014-02-12 16:53 correnson Source_changeset_attached => framac stable/neon 65bc56b6
2014-02-12 16:57 correnson Note Added: 0004533
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
+Issue History