|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0000856||Frama-C||Plug-in > Eva||public||2011-06-07 10:36||2014-02-12 16:58|
|Product Version||Frama-C Carbon-20110201|
|Target Version||Fixed in Version||Frama-C Fluorine-20130401|
|Summary||0000856: non-constant size of 2-dim array leads to crash (some similarities to issue 0000852)|
frama-c -val -main ftest ftest.c leads to a crash.
The program is kind of similar to 0000852, but without recursive call to ftest and variable size (b[a]) instead of variable size (b[a]).
But, here you do not obtain the error with frama-c -ftest.c .
|Tags||No tags attached.|
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.
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.
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.
|Thank you, I will maybe get back to it.|
|This bug will be fixed in Fluorine. The contents and the size of b will be completely imprecise, though.|
|Fix committed to stable/neon branch.|
|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||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|