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

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.

Issue History
Date Modified	Username	Field	Change
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	Checkin
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
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