Frama-C Bug Tracking System - Frama-C
View Issue Details
0001809Frama-CKernelpublic2014-06-15 05:382018-11-30 11:36
sstewartgallus 
maroneze 
normaltweakN/A
assignedopen 
Frama-C Fluorine-20130401 
 
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

There are no notes attached to this issue.