Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001751Frama-CPlug-in > wppublic2014-04-11 22:212015-03-17 22:18
Reporterjens 
Assigned Topatrick 
PriorityhighSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001751: Frama-C/WP "forgets" a proven assertion
DescriptionIn 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.

TagsNo tags attached.
Attached Filesc file icon strange_after_shift.c [^] (137 bytes) 2014-04-11 22:21 [Show Content]

- Relationships
related to 0001750closedpatrick Frama-C/WP fails to discharge simple bit operation for small integer types 

-  Notes
(0005181)
correnson (manager)
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 (developer)
2014-06-11 11:29

 Changes done for 0001750 allows alt-ergo to solve these POs.
(0005223)
patrick (developer)
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 (manager)
2014-09-23 10:17

 Fixed in related issue

- Issue History
Date Modified Username Field Change
2014-04-11 22:21 jens New Issue
2014-04-11 22:21 jens Status new => assigned
2014-04-11 22:21 jens Assigned To => correnson
2014-04-11 22:21 jens File Added: strange_after_shift.c
2014-06-02 16:00 correnson Note Added: 0005181
2014-06-02 16:01 correnson Assigned To correnson => patrick
2014-06-02 16:01 correnson Status assigned => acknowledged
2014-06-02 16:15 correnson Relationship added related to 0001750
2014-06-11 11:29 patrick Note Added: 0005222
2014-06-11 11:45 patrick Note Added: 0005223
2014-09-23 10:17 correnson Note Added: 0005482
2014-09-23 10:17 correnson Status acknowledged => resolved
2014-09-23 10:17 correnson Resolution open => fixed
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker