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-02-22 16:10
Reporterarvidj 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
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

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

- 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

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker