Frama-C Bug Tracking System - Frama-C
View Issue Details
0001751Frama-CPlug-in > wppublic2014-04-11 22:212015-03-17 22:18
jens 
patrick 
highmajoralways
closedfixed 
Frama-C Neon-20140301 
Frama-C Sodium 
0001751: Frama-C/WP "forgets" a proven assertion
In the following function void strange_after_shift(unsigned int x) { unsigned int y = x & 1; //@ assert y == 0 || y == 1; //@ assert 0 <= y <= 1; } the first assertion is discharged by Qed but the second assertion (which should also hold) is not discharged with Alt-Ergo. Moreover, when I try to prove it with Coq, then I cannot see any hypothesis that represents the first assertion.
No tags attached.
related to 0001750closed patrick Frama-C/WP fails to discharge simple bit operation for small integer types 
c strange_after_shift.c (137) 2014-04-11 22:21
https://bts.frama-c.com/file_download.php?file_id=733&type=bug
Issue History
2014-04-11 22:21jensNew Issue
2014-04-11 22:21jensStatusnew => assigned
2014-04-11 22:21jensAssigned To => correnson
2014-04-11 22:21jensFile Added: strange_after_shift.c
2014-06-02 16:00corrensonNote Added: 0005181
2014-06-02 16:01corrensonAssigned Tocorrenson => patrick
2014-06-02 16:01corrensonStatusassigned => acknowledged
2014-06-02 16:15corrensonRelationship addedrelated to 0001750
2014-06-11 11:29patrickNote Added: 0005222
2014-06-11 11:45patrickNote Added: 0005223
2014-09-23 10:17corrensonNote Added: 0005482
2014-09-23 10:17corrensonStatusacknowledged => resolved
2014-09-23 10:17corrensonResolutionopen => fixed
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:18signolesStatusresolved => closed

Notes
(0005181)
correnson   
2014-06-02 16:00   
This is due to an over-confident simplification on bitwise operation, that turns (y == 0 || y == 1) into true, thus making it disappear from the goal / the hypothesis. We have to investigate the issue. As a workaround, simply disable the bitwise simplifications with -wp-no-bits option.
(0005222)
patrick   
2014-06-11 11:29   
Changes done for #1750 allows alt-ergo to solve these POs.
(0005223)
patrick   
2014-06-11 11:45   
The first note given by Loïc is the real explanation of this issue. That should be discussed...
(0005482)
correnson   
2014-09-23 10:17   
Fixed in related issue