| 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 |
|
| Reporter | pkarpman | |
| Assigned To | virgile | |
| Priority | normal | Severity | minor | Reproducibility | sometimes |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| 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 |  nodec.c [^] (149 bytes) 2012-03-08 17:26 [Show Content] [Hide Content]void funk(int rounds)
{
int k[2*rounds];
int i;
for (i = 0; i < 2*rounds; i++)
{
k[i] = i;
}
}
int main ()
{
funk(17);
return 0;
}
|
|
Relationships 
Relationships