Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001809Frama-CKernelpublic2014-06-15 05:382019-07-05 11:41
Reportersstewartgallus 
Assigned Tomaroneze 
PrioritynormalSeveritytweakReproducibilityN/A
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130401 
Target VersionFixed in VersionFrama-C 19-Potassium 
Summary0001809: Frama-C should not have unimplemented headers
DescriptionFrama-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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006742)
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.

- Issue History
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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker