| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] |
| ID | 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 | | 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 
Relationships