2021-01-16 00:23 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001113Frama-CKernelpublic2012-03-08 17:262014-02-12 16:59
Reporterpkarpman 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilitysometimes
StatusclosedResolutionfixed 
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 Files
  • c file icon nodec.c (149 bytes) 2012-03-08 17:26 - 
    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;
}
    c file icon nodec.c (149 bytes) 2012-03-08 17:26 +

-Relationships
+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.
+Notes

-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
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
+Issue History