Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001809Frama-CKernelpublic2014-06-15 05:382018-11-30 11:36
Reportersstewartgallus 
Assigned Tomaroneze 
PrioritynormalSeveritytweakReproducibilityN/A
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130401 
Target VersionFixed in Version 
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
There are no notes attached to this issue.

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker