0001586: Bug in let-elimination (due to <==> and assert false).

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001586

Frama-C

Plug-in > wp

public

2013-12-16 11:10

2014-03-13 15:57

Reporter

correnson

Assigned To

correnson

Priority

normal

Severity

major

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Neon-20140301

Summary

0001586: Bug in let-elimination (due to <==> and assert false).

Description

Bug in let-elimination (due to <==> and assert false).
Using -wp-no-let makes the assert false not-proved as expected.

Additional Information

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.

Tags

No tags attached.

Attached Files

q19_switch_fun_call.c [^] (1,335 bytes) 2013-12-16 11:10 [Show Content] [Hide Content]

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

q20_switch_fun_call.c [^] (1,276 bytes) 2013-12-16 11:45 [Show Content] [Hide Content]

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

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.

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	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: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