Frama-C should not have unimplemented headers
ID0001809: This issue was created automatically from Mantis Issue 1809. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001809 | Frama-C | Kernel | public | 2014-06-15 | 2019-07-05 |
| Reporter | sstewartgallus | Assigned To | maroneze | Resolution | fixed |
| Priority | normal | Severity | tweak | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130401 | Target Version | - | Fixed in Version | Frama-C 19-Potassium |
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