Preprocessing code may yield expanded code with undeclared variables
ID0001113: This issue was created automatically from Mantis Issue 1113. Further discussion may take place here.
|Product Version||Frama-C Nitrogen-20111001||Target Version||-||Fixed in Version||Frama-C Oxygen-20120901|
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.:
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.
Additional Information :
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).