Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001589Frama-CKernelpublic2013-12-26 23:302014-03-13 15:57
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001589: access to volatile variable is eliminated from AST
Description~ $ 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004383)
virgile (developer)
2014-01-06 13:17

Fix committed to master branch.
(0004384)
virgile (developer)
2014-01-06 13:20

Fixed in git
(0004544)
virgile (developer)
2014-02-12 16:57

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2013-12-26 23:30 pascal New Issue
2013-12-26 23:30 pascal Status new => assigned
2013-12-26 23:30 pascal Assigned To => virgile
2014-01-06 13:17 virgile Note Added: 0004383
2014-01-06 13:17 virgile Resolution open => fixed
2014-01-06 13:20 virgile Note Added: 0004384
2014-01-06 13:20 virgile Status assigned => resolved
2014-02-12 16:57 virgile Note Added: 0004544
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker