Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001113Frama-CKernelpublic2012-03-08 17:262014-02-12 16:59
Reporterpkarpman 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilitysometimes
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001113: Preprocessing code may yield expanded code with undeclared variables
DescriptionSome 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 InformationMight 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).
TagsNo tags attached.
Attached Filesc file icon nodec.c [^] (149 bytes) 2012-03-08 17:26 [Show Content]

- Relationships

-  Notes
(0002812)
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.
(0004709)

2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
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 Checkin
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
2014-02-12 16:59 Note Added: 0004709
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker