2021-01-24 23:54 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001076Frama-CPlug-in > Evapublic2012-09-19 17:16
ReporterJochen 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001076: "volatile" ignored
DescriptionRunning "frama-c -val exm22.c" on the attached program produces the output "a in {0}". Running the same command after deleting the initialization of "a" in line 2 reports a run-time error (uninitialized variable access) in line 3. Both would be ok if "a" wasn't declared "volatile".

In contrast to the 1st analysis result, the value-analysis manual says on p.43: "the analyzer does not assume that the value read from a volatile variable is identical to the last value written there."
TagsNo tags attached.
Attached Files
  • c file icon exm22.c (85 bytes) 2012-01-30 12:15 -
    int main(void) {
        volatile int a = 0;
        Frama_C_show_each_a(a);
        return a;
    }
    
    c file icon exm22.c (85 bytes) 2012-01-30 12:15 +

-Relationships
+Relationships

-Notes

~0002646

pascal (reporter)

Volatile variables are officially broken since around last July when a reorganization of the representation of programs was made and there was no industrial user to pay for the treatment of volatiles in the value analysis to be re-established.

http://blog.frama-c.com/index.php?post/2011/07/21/Back-to-the-drawing-board

Until someone steps up and funds the week or so of development and validation to fix this, you can assume that volatile variables in the value analysis do not work.

~0002647

Jochen (reporter)

That's ok for me. You should sometimes update the according section (p.43) in the value-analysis manual.

~0003095

yakobowski (manager)

This bug has been fixed at some point after Nitrogen. Notice that 'a' was actually considered volatile when computing expressions; only the printing of its final value was incorrect.

  volatile int a=0;
  return a+1;

   a ? {0}
   __retres ? [--..--]


Notice that the code below is still considered incorrect. This is a conscious design choice.

  volatile int a;
  return a+1;
+Notes

-Issue History
Date Modified Username Field Change
2012-01-30 12:15 Jochen New Issue
2012-01-30 12:15 Jochen Status new => assigned
2012-01-30 12:15 Jochen Assigned To => pascal
2012-01-30 12:15 Jochen File Added: exm22.c
2012-01-30 23:38 pascal Note Added: 0002646
2012-01-31 10:22 Jochen Note Added: 0002647
2012-06-10 18:26 yakobowski Note Added: 0003095
2012-06-10 18:26 yakobowski Status assigned => resolved
2012-06-10 18:26 yakobowski Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History