View Issue Details [ Jump to Notes ] | [ 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 | ||||
Reporter | pkarpman | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | minor | Reproducibility | sometimes | ||||
Status | closed | Resolution | fixed | ||||||
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.: 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). | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
pkarpman (reporter) 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. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
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 | ||
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 |