| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0001847 | Frama-C | Plug-in > wp | public | 2014-07-21 10:06 | 2014-07-21 10:06 |
|
| Reporter | davyg | |
| Assigned To | correnson | |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Status | assigned | Resolution | open | |
| Platform | | OS | | OS Version | |
| Product Version | | |
| Target Version | | Fixed in Version | | |
|
| Summary | 0001847: Problem with _Bool(when casting to int or with ?:) |
| Description | In this example the ensures seems to be impossible to prove whereas it should
be easy :
//@ensures (!\result) == (!x);
_Bool f(_Bool x) {
_Bool y;
return (y?x:x);
}
I put the bug in Wp category but it can be see as a framaC bug depending from where it comes from. |
| Additional Information | This must be due to the transformation of ?: into an if statement
with an int local variable which lead more or less to a function like
this that can't be proven :
//@ensures (!\result) == (!x);
_Bool g(_Bool x) {
int t = x;
return t;
}
This must be due to the lack of information about the cast.
I think that the transformation of ?: should use a _Bool temp
variable instead of an int. Or int cast should have a lemma like \forall _Bool x; (x != 0) <==> (((int) x) != 0); |
| Tags | No tags attached. |
|
| Attached Files | |
|
Relationships 
Relationships