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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001113 | Frama-C | Kernel | public | 2012-03-08 | 2014-02-12 |
| Reporter | pkarpman | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | sometimes |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
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.
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).