0001113: Preprocessing code may yield expanded code with undeclared variables

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

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 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

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