Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002306Frama-CKernelpublic2017-05-29 19:412017-12-17 20:47
Reporterevdenis 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002306: Support for flexible array members
DescriptionFlexible 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 Reproduceframa-c rte_cgrp.c
TagsNo tags attached.
Attached Filesc file icon rte_cgrp.c [^] (73 bytes) 2017-05-29 19:41 [Show Content]

- Relationships

-  Notes
(0006399)
yakobowski (manager)
2017-05-30 15:02

This is actually not valid C, and is flagged as such by gcc -pedantic or clang -pedantic. 6.7.2.1:2 specifies: > A structure or union shall not contain a member with incomplete or function type [...], except that the last member of a structure with more than one named member may have incomplete array type; such a structure (and any union containing, possibly recursively, a member that is such a structure) shall not be a member of a structure or an element of an array. Proper support for nested flexible array members would be hard to implement in Frama-C. Is this feature crucial for the verification you intend to conduct?
(0006405)
evdenis (reporter)
2017-05-31 15:32

It isn't crucial. Error message confused me, so I decided to report the issue. Such a code can be found in Linux kernel. http://elixir.free-electrons.com/linux/v4.11.3/source/include/linux/cgroup-defs.h#L308 Some clarification on how this issue can be mitigated: In most cases, an incomplete (int b[]) field can be commented out because such structures (just a common definition) are not used directly in a code you want to analyze. So to run Frama-C you should strip out these (incomplete) fields and all the static inline functions that can depend on them from the code.

- Issue History
Date Modified Username Field Change
2017-05-29 19:41 evdenis New Issue
2017-05-29 19:41 evdenis File Added: rte_cgrp.c
2017-05-30 15:02 yakobowski Note Added: 0006399
2017-05-30 15:02 yakobowski Assigned To => yakobowski
2017-05-30 15:02 yakobowski Status new => feedback
2017-05-31 15:32 evdenis Note Added: 0006405
2017-05-31 15:32 evdenis Status feedback => assigned
2017-12-17 20:47 yakobowski Assigned To yakobowski => maroneze


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker