Support for struct containing flexible array members
ID0002306: This issue was created automatically from Mantis Issue 2306. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002306 | Frama-C | Kernel | public | 2017-05-29 | 2017-12-17 |
| Reporter | evdenis | Assigned To | maroneze | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
Flexible array member is a feature introduced in the C99 standard of the C programming language (in particular, in section §6.7.2.1, item 16, page 103).
Test: struct cgroup { int a; int b[]; }; struct { struct cgroup cgrp; };
Frama-c run: $ frama-c rte_cgrp.c [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing rte_cgrp.c (with preprocessing) rte_cgrp.c:5:[kernel] user error: field cgrp is declared with incomplete type struct cgroup [kernel] user error: stopping on file "rte_cgrp.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input.
Steps To Reproduce :
frama-c rte_cgrp.c