Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001834Frama-CPlug-in > E-ACSLpublic2014-07-15 16:092018-07-11 15:59
Reporterarvidj 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C 17-Chlorine 
Summary0001834: Cannot compile variable length arrays
DescriptionThe 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.
TagsNo tags attached.
Attached Filesc file icon bug-vla.c [^] (382 bytes) 2014-07-15 16:09 [Show Content]

- Relationships
has duplicate 0002381closedsignoles E-ACSL: vla handling 

-  Notes
(0005259)
signoles (manager)
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 (manager)
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 (manager)
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 (manager)
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 (manager)
2018-07-11 15:34
edited on: 2018-07-11 15:42

 Fixed in Frama-C Chlorine.

- Issue History
Date Modified Username Field Change
2014-07-15 16:09 arvidj New Issue
2014-07-15 16:09 arvidj Status new => assigned
2014-07-15 16:09 arvidj Assigned To => signoles
2014-07-15 16:09 arvidj File Added: bug-vla.c
2014-07-15 16:21 signoles Status assigned => confirmed
2014-07-15 17:49 signoles Note Added: 0005259
2014-07-15 17:59 signoles Note Added: 0005260
2014-07-15 18:00 signoles Note View State: 0005260: public
2014-07-15 18:00 signoles Note View State: 0005259: public
2014-07-15 18:01 signoles Note Added: 0005261
2015-06-09 13:55 signoles Note Added: 0005936
2015-10-29 11:16 signoles Assigned To signoles => kvorobyov
2015-10-29 11:16 signoles Status confirmed => assigned
2017-10-24 17:42 signoles Assigned To kvorobyov => signoles
2018-02-22 16:10 signoles Status assigned => resolved
2018-02-22 16:10 signoles Resolution open => fixed
2018-07-11 15:33 signoles Fixed in Version => Frama-C 16-Sulfur
2018-07-11 15:34 signoles Status resolved => closed
2018-07-11 15:34 signoles Note Added: 0006582
2018-07-11 15:40 signoles Fixed in Version Frama-C 16-Sulfur => Frama-C 17-Chlorine
2018-07-11 15:42 signoles Note Edited: 0006582 View Revisions
2018-07-11 15:59 signoles Relationship added has duplicate 0002381

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker