Frama-C Bug Tracking System - Frama-C
View Issue Details
0001113Frama-CKernelpublic2012-03-08 17:262014-02-12 16:59
Frama-C Nitrogen-20111001 
Frama-C Oxygen-20120901 
0001113: Preprocessing code may yield expanded code with undeclared variables
Some variables introduced by Frama-C during the preprocessing phase (i.e. the result of "frama-c -print") may not be declared (thus yielding incorrect code). A simple example where this occurs is when declaring arrays with variable size, e.g.: int k[2*rounds]; is transformed as int *k; __lengthofk = (unsigned int)(2 * rounds); k = (int *)__builtin_alloca(sizeof(*k) * __lengthofk); with __lengthofk being left undeclared. See attached file for a (complete) simple example. HOW TO REPRODUCE: Preprocess code with e.g. a variable-sized array declaration. This is however not the only case where this seem to happen. EXPECTED BEHAVIOUR: In this example, declaration of __lengthofk as unsigned int.
Might be a regression from Carbon. I have scripts (that I didn't write myself, though, so I may not use them properly) that first preprocess C programs with Frama-C before using again Frama-C on the `expanded' code. I don't think the previous user of those scripts had any problems with missing declarations when using them on Frama-C B & C, and yet they pretty much always fail for me when using Frama-C N (but succeed when I manually add the missing declarations).
No tags attached.
c nodec.c (149) 2012-03-08 17:26
Issue History
2012-03-08 17:26pkarpmanNew Issue
2012-03-08 17:26pkarpmanFile Added: nodec.c
2012-03-08 18:42signolesStatusnew => assigned
2012-03-08 18:42signolesAssigned To => virgile
2012-03-30 09:20pkarpmanNote Added: 0002812
2012-03-30 15:29svnCheckin
2012-03-30 15:29svnStatusassigned => resolved
2012-03-30 15:29svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004709
2014-02-12 16:59Statusclosed => resolved

2012-03-30 09:20   
For information, contrary to what I said in the additional info, Carbon seems to exhibit the bug as well.
2014-02-12 16:59   
Fix committed to stable/neon branch.