2021-02-24 18:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001586Frama-CPlug-in > wppublic2014-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)

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

~0004505

correnson (manager)

Fix committed to master branch.

~0004533

correnson (manager)

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