View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001834 | Frama-C | Plug-in > E-ACSL | public | 2014-07-15 16:09 | 2018-07-11 15:59 | ||||
Reporter | arvidj | ||||||||
Assigned To | signoles | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | |||||||||
Target Version | Fixed in Version | Frama-C 17-Chlorine | |||||||
Summary | 0001834: Cannot compile variable length arrays | ||||||||
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. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
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)." |
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) |
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. |
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. |
signoles (manager) 2018-07-11 15:34 Last edited: 2018-07-11 15:42 |
Fixed in Frama-C Chlorine. |
![]() |
|||
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 |