Problem with _Bool(when casting to int or with ?:)
ID0001847: This issue was created automatically from Mantis Issue 1847. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001847 | Frama-C | Plug-in > wp | public | 2014-07-21 | 2014-07-21 |
| Reporter | davyg | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
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);