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