Frama-C Bug Tracking System - Frama-C
View Issue Details
0001834Frama-CPlug-in > E-ACSLpublic2014-07-15 16:092018-07-11 15:59
arvidj 
signoles 
normalminoralways
closedfixed 
 
Frama-C 17-Chlorine 
0001834: Cannot compile variable length arrays
The resulting C-code from running Frama-C with E-ACSL on the following program (same as attached):
  
  int main(int argc, char **argv) {
    int len = 4;
    int data[len];
    return 0;
  }

cannot be compiled, giving the following error:

  bug-vla.c:(.text+0xa74): undefined reference to `alloca'

the code generated is:
 
  [...]
  void *alloca(unsigned long);
  [...]


  int len;
  int *data;
  unsigned long __lengthofdata;
  len = 4;
  {
    /*sequence*/
    __lengthofdata = (unsigned long)len;
    data = (int *)alloca(sizeof(*data) * __lengthofdata);
  }
  [...]

This code does not compile with GCC and the flag -std=c99.
No tags attached.
has duplicate 0002381closed signoles E-ACSL: vla handling 
c bug-vla.c (382) 2014-07-15 16:09
https://bts.frama-c.com/file_download.php?file_id=795&type=bug
Issue History
2014-07-15 16:09arvidjNew Issue
2014-07-15 16:09arvidjStatusnew => assigned
2014-07-15 16:09arvidjAssigned To => signoles
2014-07-15 16:09arvidjFile Added: bug-vla.c
2014-07-15 16:21signolesStatusassigned => confirmed
2014-07-15 17:49signolesNote Added: 0005259
2014-07-15 17:59signolesNote Added: 0005260
2014-07-15 18:00signolesNote View State: 0005260: public
2014-07-15 18:00signolesNote View State: 0005259: public
2014-07-15 18:01signolesNote Added: 0005261
2015-06-09 13:55signolesNote Added: 0005936
2015-10-29 11:16signolesAssigned Tosignoles => kvorobyov
2015-10-29 11:16signolesStatusconfirmed => assigned
2017-10-24 17:42signolesAssigned Tokvorobyov => signoles
2018-02-22 16:10signolesStatusassigned => resolved
2018-02-22 16:10signolesResolutionopen => fixed
2018-07-11 15:33signolesFixed in Version => Frama-C 16-Sulfur
2018-07-11 15:34signolesStatusresolved => closed
2018-07-11 15:34signolesNote Added: 0006582
2018-07-11 15:40signolesFixed in VersionFrama-C 16-Sulfur => Frama-C 17-Chlorine
2018-07-11 15:42signolesNote Edited: 0006582bug_revision_view_page.php?bugnote_id=6582#r354
2018-07-11 15:59signolesRelationship addedhas duplicate 0002381

Notes
(0005259)
signoles   
2014-07-15 17:49   
This behaviour is actually specified:
- documentation of Gcc indicates that "You can use the function alloca to get an effect much like variable-length arrays." (https://gcc.gnu.org/onlinedocs/gcc/Variable-Length.html [^])
- documentation of alloca (man alloca) indicates:
  * "This function is not in POSIX."
  * "Normally, gcc(1) translates calls to alloca() with inlined code. This is not done when either the -ansi, -std=c89, -std=c99, or the -fno-builtin option is given (and the header <alloca.h> is not included)."
(0005260)
signoles   
2014-07-15 17:59   
To be C99 compliant, you can still link the generated code against an implementation of alloca (e.g. the OpenBSD one: http://dev.hypertriton.com/fabbsd/trunk/lib/libc/gen/alloca.c [^])
(0005261)
signoles   
2014-07-15 18:01   
The remaining issue is that the E-ACSL generated code is incorrect wrt the semantics of alloca: it should monitore the allocation/de-allocation correctly.
(0005936)
signoles   
2015-06-09 13:55   
The generated code is gcc-compliant if you use "-machdep gcc_x86_64" (on x86 64bit arch).

It still remains to monitor the allocation.
(0006582)
signoles   
2018-07-11 15:34   
(edited on: 2018-07-11 15:42)
Fixed in Frama-C Chlorine.