Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001847Frama-CPlug-in > wppublic2014-07-21 10:062014-07-21 10:06
Reporterdavyg 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0001847: Problem with _Bool(when casting to int or with ?:)
DescriptionIn 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 InformationThis 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);
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-07-21 10:06 davyg New Issue
2014-07-21 10:06 davyg Status new => assigned
2014-07-21 10:06 davyg Assigned To => correnson


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker