|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001113||Frama-C||Kernel||public||2012-03-08 17:26||2014-02-12 16:59|
|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.|
|For information, contrary to what I said in the additional info, Carbon seems to exhibit the bug as well.|
|Fix committed to stable/neon branch.|
|2012-03-08 17:26||pkarpman||New Issue|
|2012-03-08 17:26||pkarpman||File Added: nodec.c|
|2012-03-08 18:42||signoles||Status||new => assigned|
|2012-03-08 18:42||signoles||Assigned To||=> virgile|
|2012-03-30 09:20||pkarpman||Note Added: 0002812|
|2012-03-30 15:29||svn||Status||assigned => resolved|
|2012-03-30 15:29||svn||Resolution||open => fixed|
|2012-09-19 17:15||signoles||Fixed in Version||=> Frama-C Oxygen-20120901|
|2012-09-19 17:16||signoles||Status||resolved => closed|
|2013-12-19 01:12||Source_changeset_attached||=> framac master 514721ad|
|2014-02-12 16:54||Source_changeset_attached||=> framac stable/neon 514721ad|
|2014-02-12 16:59||Note Added: 0004709|
|2014-02-12 16:59||Status||closed => resolved|