|View Issue Details [ Jump to Notes ] [ Related Changesets ] ||[ Issue History ] [ Print ] |
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001113||Frama-C||Kernel||public||2012-03-08 17:26||2014-02-12 16:59|
|Assigned To||virgile|| |
|Product Version||Frama-C Nitrogen-20111001|| |
|Target Version||Fixed in Version||Frama-C Oxygen-20120901|| |
|Summary||0001113: Preprocessing code may yield expanded code with undeclared variables|
|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.:
is transformed as
__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.
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).|
|Tags||No tags attached.|
|Attached Files|| nodec.c [^] (149 bytes) 2012-03-08 17:26 [Show Content]