Frama-C Bug Tracking System - Frama-C
View Issue Details
0001076Frama-CPlug-in > Evapublic2012-01-30 12:152012-09-19 17:16
Assigned Topascal 
PlatformOSOS Version
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 Filesc exm22.c (85) 2012-01-30 12:15

2012-01-30 23:38   
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.

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.
2012-01-31 10:22   
That's ok for me. You should sometimes update the according section (p.43) in the value-analysis manual.
2012-06-10 18:26   
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;

Issue History
2012-01-30 12:15JochenNew Issue
2012-01-30 12:15JochenStatusnew => assigned
2012-01-30 12:15JochenAssigned To => pascal
2012-01-30 12:15JochenFile Added: exm22.c
2012-01-30 23:38pascalNote Added: 0002646
2012-01-31 10:22JochenNote Added: 0002647
2012-06-10 18:26yakobowskiNote Added: 0003095
2012-06-10 18:26yakobowskiStatusassigned => resolved
2012-06-10 18:26yakobowskiResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva