Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001750Frama-CPlug-in > wppublic2014-04-11 18:502015-03-17 22:17
Reporterjens 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001750: Frama-C/WP fails to discharge simple bit operation for small integer types
DescriptionIn the attached file there are for simple functions that computes b = a & 1; //@ assert b == 0 || b == 1; where a and b are of type unsigned char, unsigned short, unsigned int and unsigned long. Only for the types unsigned int and unsigned long cab WP (in fact QED) discharge the assertion. Both alt-ergo and CVC4 fail on unsigned char and unsigned short. I would be very nice if Frama-C/WP could handle the other cases automatically as well.
Steps To Reproduce
Additional Information
TagsNo tags attached.
Relationships
related to 0001751closed patrick Frama-C/WP "forgets" a proven assertion 
Attached Filesc bit_and.c (402) 2014-04-11 18:50
https://bts.frama-c.com/file_download.php?file_id=732&type=bug
Issue History
Date ModifiedUsernameFieldChange
2014-04-11 18:50jensNew Issue
2014-04-11 18:50jensStatusnew => assigned
2014-04-11 18:50jensAssigned To => correnson
2014-04-11 18:50jensFile Added: bit_and.c
2014-06-02 16:15corrensonRelationship addedrelated to 0001751
2014-06-02 16:15corrensonAssigned Tocorrenson => patrick
2014-06-10 12:48patrickNote Added: 0005218
2014-06-11 11:19patrickNote Added: 0005221
2014-06-11 11:19patrickStatusassigned => resolved
2014-06-11 11:19patrickResolutionopen => fixed
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:17signolesStatusresolved => closed

Notes
(0005218)
patrick   
2014-06-10 12:48   
Some axioms have to be added for alt-ergo: axiom bit_test_introduction_land : (forall x:int [land(x, 1)| land(1, x)]. ((not (land(x, 1) = 0)) -> bit_test(x, 0))) axiom bit_test_introduction_land_bis : (forall x:int [land(x, 1)| land(1, x)]. (bit_test(x, 0) -> (land(x, 1) = 1)))
(0005221)
patrick   
2014-06-11 11:19   
Fix committed to master branch.