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: 0006582View Revisions
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 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.