Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001801Frama-CPlug-in > wppublic2014-06-06 12:422014-06-06 12:42
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001801: WP doesn't warn about volatile variables
DescriptionI noticed that WP doesn't handle volatile variables, which is not a problem, but the problem is that it proves properties about them without any warning at all, which a quiet embarrassing I suppose.
Steps To Reproduce$ frama-c -wp-fct main test_volatile.c volatile int v = 10; //@ ensures \result == 10; int main (void) { int x = v; //@ assert v == 10; v = 3; //@ assert v == 3; return x; }
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-06-06 12:42 Anne New Issue
2014-06-06 12:42 Anne Status new => assigned
2014-06-06 12:42 Anne Assigned To => correnson


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker