View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001809 | Frama-C | Kernel | public | 2014-06-15 05:38 | 2019-07-05 11:41 | ||||
Reporter | sstewartgallus | ||||||||
Assigned To | maroneze | ||||||||
Priority | normal | Severity | tweak | Reproducibility | N/A | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Fluorine-20130401 | ||||||||
Target Version | Fixed in Version | Frama-C 19-Potassium | |||||||
Summary | 0001809: Frama-C should not have unimplemented headers | ||||||||
Description | Frama-C comes with annotated headers for the C standard library and a few GLibc extensions. Frama-c also comes with unimplemented dummy headers for some GLibc functionality. These unimplemented dummy headers are worse than useless, as well as not giving annotated versions of functions they prevent one from including system unannotated versions of the headers. To work around this issue one can copy headers and remove the useless headers from the copy but this is annoying. Frama-C should remove features.h (as this is highly system specific) and should remove or implement the following: linux/fs.h linux/if_addr.h linux/if_netlink.h linux/netlink.h linux/rtnetlink.h libgen.h libintl.h netinet/in_systm.h netinet/ip.h netinet/ip_icmp.h sys/param.h sys/sysctl.h uchar.h | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
maroneze (administrator) 2019-02-05 15:46 |
Most of the remarks were taken into account, except for features.h (which is still used for some normalizations) and a few files which had prototypes added. The headers without prototypes were removed. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2014-06-15 05:38 | sstewartgallus | New Issue | |
2014-06-18 14:42 | signoles | Assigned To | => Matthieu Lemerre |
2014-06-18 14:42 | signoles | Status | new => assigned |
2018-11-30 11:36 | signoles | Assigned To | Matthieu Lemerre => maroneze |
2019-02-05 15:46 | maroneze | Note Added: 0006742 | |
2019-02-05 15:46 | maroneze | Status | assigned => resolved |
2019-02-05 15:46 | maroneze | Fixed in Version | => Frama-C 19-Potassium |
2019-02-05 15:46 | maroneze | Resolution | open => fixed |
2019-07-05 11:41 | signoles | Status | resolved => closed |