Cannot compile variable length arrays
ID0001834: This issue was created automatically from Mantis Issue 1834. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001834 | Frama-C | Plug-in > E-ACSL | public | 2014-07-15 | 2018-07-11 |
| Reporter | arvidj | Assigned To | signoles | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C 17-Chlorine |
Description :
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.