2021-01-21 05:57 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001801Frama-CPlug-in > wppublic2014-06-06 12:42
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
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


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
+Issue History