Frama-C Bug Tracking System - Frama-C
View Issue Details
0001589Frama-CKernelpublic2013-12-26 23:302014-03-13 15:57
pascal 
virgile 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Neon-20140301 
0001589: access to volatile variable is eliminated from AST
~ $ cat n.c volatile int x; int main(){ x; x; x; } ~ $ ~/ppc/bin/toplevel.opt -print n.c [kernel] preprocessing with "gcc -C -E -I. n.c" /* Generated by Frama-C */ int volatile x; int main(void) { int __retres; __retres = 0; return __retres; } This transformation does not respect the semantics of the program because x is volatile.
No tags attached.
Issue History
2013-12-26 23:30pascalNew Issue
2013-12-26 23:30pascalStatusnew => assigned
2013-12-26 23:30pascalAssigned To => virgile
2014-01-06 13:17virgileNote Added: 0004383
2014-01-06 13:17virgileResolutionopen => fixed
2014-01-06 13:20virgileNote Added: 0004384
2014-01-06 13:20virgileStatusassigned => resolved
2014-02-12 16:57virgileNote Added: 0004544
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004383)
virgile   
2014-01-06 13:17   
Fix committed to master branch.
(0004384)
virgile   
2014-01-06 13:20   
Fixed in git
(0004544)
virgile   
2014-02-12 16:57   
Fix committed to stable/neon branch.