Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001076Frama-CPlug-in > Evapublic2012-01-30 12:152012-09-19 17:16
ReporterJochen 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 file icon exm22.c [^] (85 bytes) 2012-01-30 12:15 [Show Content]

- Relationships

-  Notes
(0002646)
pascal (reporter)
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.

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)
2012-01-31 10:22

That's ok for me. You should sometimes update the according section (p.43) in the value-analysis manual.
(0003095)
yakobowski (manager)
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
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker