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