2021-03-02 03:08 CET
  

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 
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 Files
  • c file icon bug-vla.c (382 bytes) 2014-07-15 16:09 - 
    #include <stdio.h>
#include <stdlib.h>
#include <string.h>

int main(int argc, char **argv) {
  int len = 4;
  int data[len];
  return 0;
}


/* Local Variables: */
/* compile-command: "frama-c -add-path ../../e-acsl -machdep x86_64 -e-acsl bug-vla.c -e-acsl-share ~/dev/e-acsl/share/e-acsl -then-on e-acsl -print -ocode bug-vla.gen.c" */
/* compile-read-command: nil */
/* End: */
    c file icon bug-vla.c (382 bytes) 2014-07-15 16:09 +

-Relationships
has duplicate 0002381closedsignoles E-ACSL: vla handling 
+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.

~0006582

signoles (manager)

2018-07-11 15:34

Last edited: 2018-07-11 15:42

View 2 revisions

 Fixed in Frama-C Chlorine.
+Notes

-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
+Issue History