Frama-C Bug Tracking System - Frama-C
View Issue Details
0000856Frama-CPlug-in > Evapublic2011-06-07 10:362014-02-12 16:58
Assigned Toyakobowski 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000856: non-constant size of 2-dim array leads to crash (some similarities to issue /view.php?id=852)
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[10][a]) instead of variable size (b[1][a]).

But, here you do not obtain the error with frama-c -ftest.c .

TagsNo tags attached.
related to 0000852assigned virgile non-constant size of 2-dim array causes error in recursive procedure 
Attached Filesc ftest.c (97) 2011-06-07 10:36

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

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.
2011-06-14 13:41   
Thank you, I will maybe get back to it.
2013-03-10 13:04   
This bug will be fixed in Fluorine. The contents and the size of b will be completely imprecise, though.
2014-02-12 16:58   
Fix committed to stable/neon branch.

Issue History
2011-06-07 10:36kerstinNew Issue
2011-06-07 10:36kerstinStatusnew => assigned
2011-06-07 10:36kerstinAssigned To => pascal
2011-06-07 10:36kerstinFile Added: ftest.c
2011-06-07 10:50pascalStatusassigned => confirmed
2011-06-07 13:22pascalRelationship addedrelated to 0000852
2011-06-07 13:22pascalNote Added: 0001957
2011-06-07 13:22pascalStatusconfirmed => feedback
2011-06-08 11:06kerstinNote Added: 0001958
2011-06-08 11:49pascalNote Added: 0001959
2011-06-14 13:41kerstinNote Added: 0001974
2013-03-10 13:04yakobowskiStatusfeedback => assigned
2013-03-10 13:04yakobowskiAssigned Topascal => yakobowski
2013-03-10 13:04yakobowskiNote Added: 0003746
2013-03-10 13:06svn
2013-03-10 13:06svnStatusassigned => resolved
2013-03-10 13:06svnResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2013-12-19 01:11yakobowskiSource_changeset_attached => framac master 0d02d7c0
2014-02-12 16:53yakobowskiSource_changeset_attached => framac stable/neon 0d02d7c0
2014-02-12 16:58yakobowskiNote Added: 0004588
2014-02-12 16:58yakobowskiStatusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva