2021-01-25 09:00 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000856Frama-CPlug-in > Evapublic2014-02-12 16:58
Assigned Toyakobowski 
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 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[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.
Attached Files
  • c file icon 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 
    c file icon ftest.c (97 bytes) 2011-06-07 10:36 +

related to 0000852assignedvirgile non-constant size of 2-dim array causes error in recursive procedure 



pascal (reporter)

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.


kerstin (reporter)

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.



pascal (reporter)

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.


kerstin (reporter)

Thank you, I will maybe get back to it.


yakobowski (manager)

This bug will be fixed in Fluorine. The contents and the size of b will be completely imprecise, though.


yakobowski (manager)

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