Frama-C Bug Tracking System - Frama-C
View Issue Details
0000892Frama-CKernelpublic2011-07-26 12:242014-02-12 16:59
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000892: Cil wrongly authorizes references to local variables in static arrays
frama-c -check crashes on the following code. int tab[16]; void* main(void) { int i; static const int* t[] = { &tab[1], &tab[3], &tab[4], &i }; return &t; } Declaring t as static causes Cil to lift the array to the global scope of the module, but this is incorrect because of &i. I think the program is incorrect in the first place, but Cil should reject it, instead of silently producing a wrong AST.
No tags attached.
Issue History
2011-07-26 12:24yakobowskiNew Issue
2011-07-26 12:24yakobowskiStatusnew => assigned
2011-07-26 12:24yakobowskiAssigned To => virgile
2011-08-04 17:07svnCheckin
2011-08-04 17:07svnStatusassigned => resolved
2011-08-04 17:07svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59monateNote Added: 0004751
2014-02-12 16:59monateAssigned Tovirgile => monate
2014-02-12 16:59monateStatusclosed => resolved

2014-02-12 16:59   
Fix committed to stable/neon branch.