Frama-C Bug Tracking System - Frama-C
View Issue Details
0001809Frama-CKernelpublic2014-06-15 05:382019-02-05 15:46
sstewartgallus 
maroneze 
normaltweakN/A
resolvedfixed 
Frama-C Fluorine-20130401 
Frama-C 19-Potassium 
0001809: Frama-C should not have unimplemented headers
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
No tags attached.
Issue History
2014-06-15 05:38sstewartgallusNew Issue
2014-06-18 14:42signolesAssigned To => Matthieu Lemerre
2014-06-18 14:42signolesStatusnew => assigned
2018-11-30 11:36signolesAssigned ToMatthieu Lemerre => maroneze
2019-02-05 15:46maronezeNote Added: 0006742
2019-02-05 15:46maronezeStatusassigned => resolved
2019-02-05 15:46maronezeFixed in Version => Frama-C 19-Potassium
2019-02-05 15:46maronezeResolutionopen => fixed

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