0001809: Frama-C should not have unimplemented headers

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001809

Frama-C

Kernel

public

2014-06-15 05:38

2018-11-30 11:36

Reporter

sstewartgallus

Assigned To

maroneze

Priority

normal

Severity

tweak

Reproducibility

N/A

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Frama-C Fluorine-20130401

Target Version

Fixed in Version

Summary

0001809: Frama-C should not have unimplemented headers

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

Tags

No 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