0000856: non-constant size of 2-dim array leads to crash (some similarities to issue #852)

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Tags

No tags attached.

Attached Files

ftest.c (97 bytes) 2011-06-07 10:36

void ftest(int a,int b[10][a])
{
  //ftest(a,b); // the recursive call would lead to bug #852 
}

ftest.c (97 bytes) 2011-06-07 10:36

Relationships

related to

0000852

assigned

virgile

non-constant size of 2-dim array causes error in recursive procedure

Relationships

Notes
~0001957 pascal (reporter) 2011-06-07 13:22	This is a case of variable length array. Even simpler cases of variable length arrays are not very well supported in Frama-C in general (the front-end transforms them into something else, which is not very convenient for handling them). Is there a reason you are interested in this example in particular? Note that even if 852 and this bug were both fixed, recursive calls would still not be supported in the value analysis.

~0001958 kerstin (reporter) 2011-06-08 11:06	We just stumbled over this variable length arrays issue while analyzing a more or less complex piece of program. (which also contained some recursion that we eliminated, because we know it is not supported) Reducing it I got this crash which I wanted to report in addition to the bug report that Jochen already submitted. Maybe variable length arrays are not that important, I would say. But with our program it turns out to be a bit of a limitation though. Regards, Kerstin

~0001959 pascal (reporter) 2011-06-08 11:49	Oh, ok. But in this example, the bug is specifically because the variable length array is an argument of the main function (the function whose name is indicated to option -main). I can fix that, but I do not think it is the problem in your program (unless you are experimenting with analyzing functions one by one with the value analysis using -lib-entry). So if you have other, more representative, issues where the VLA is not an argument of the main() function, feel free to report them too, and I'll look at them in priority. One thing I knew the front-end did and wasn't supported well was transform local VLA into calls to alloca(). The case of argument VLA is different, and I'm certain it doesn't work now, but it should be easier to make it work soon.

~0001974 kerstin (reporter) 2011-06-14 13:41	Thank you, I will maybe get back to it.

~0003746 yakobowski (manager) 2013-03-10 13:04	This bug will be fixed in Fluorine. The contents and the size of b will be completely imprecise, though.

~0004588 yakobowski (manager) 2014-02-12 16:58	Fix committed to stable/neon branch.

Notes

Date Modified	Username	Field	Change
Issue History
2011-06-07 10:36	kerstin	New Issue
2011-06-07 10:36	kerstin	Status	new => assigned
2011-06-07 10:36	kerstin	Assigned To	=> pascal
2011-06-07 10:36	kerstin	File Added: ftest.c
2011-06-07 10:50	pascal	Status	assigned => confirmed
2011-06-07 13:22	pascal	Relationship added	related to 0000852
2011-06-07 13:22	pascal	Note Added: 0001957
2011-06-07 13:22	pascal	Status	confirmed => feedback
2011-06-08 11:06	kerstin	Note Added: 0001958
2011-06-08 11:49	pascal	Note Added: 0001959
2011-06-14 13:41	kerstin	Note Added: 0001974
2013-03-10 13:04	yakobowski	Status	feedback => assigned
2013-03-10 13:04	yakobowski	Assigned To	pascal => yakobowski
2013-03-10 13:04	yakobowski	Note Added: 0003746
2013-03-10 13:06	svn
2013-03-10 13:06	svn	Status	assigned => resolved
2013-03-10 13:06	svn	Resolution	open => fixed
2013-04-19 11:05	signoles	Fixed in Version	=> Frama-C Fluorine
2013-04-19 11:05	signoles	Status	resolved => closed
2013-12-19 01:11	yakobowski	Source_changeset_attached	=> framac master 0d02d7c0
2014-02-12 16:53	yakobowski	Source_changeset_attached	=> framac stable/neon 0d02d7c0
2014-02-12 16:58	yakobowski	Note Added: 0004588
2014-02-12 16:58	yakobowski	Status	closed => resolved
2018-01-12 14:26	signoles	Category	Plug-in > value analysis => Plug-in > Eva

Issue History