Frama-C Bug Tracking System - Frama-C
View Issue Details
0001750Frama-CPlug-in > wppublic2014-04-11 18:502015-03-17 22:17
jens 
patrick 
normalminoralways
closedfixed 
Frama-C Neon-20140301 
Frama-C Sodium 
0001750: Frama-C/WP fails to discharge simple bit operation for small integer types
In 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.
No tags attached.
related to 0001751closed patrick Frama-C/WP "forgets" a proven assertion 
c bit_and.c (402) 2014-04-11 18:50
https://bts.frama-c.com/file_download.php?file_id=732&type=bug
Issue History
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.