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

2019-07-05 11:41

Reporter

sstewartgallus

Assigned To

maroneze

Priority

normal

Severity

tweak

Reproducibility

N/A

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Fluorine-20130401

Target Version

Fixed in Version

Frama-C 19-Potassium

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

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
2019-02-05 15:46	maroneze	Note Added: 0006742
2019-02-05 15:46	maroneze	Status	assigned => resolved
2019-02-05 15:46	maroneze	Fixed in Version	=> Frama-C 19-Potassium
2019-02-05 15:46	maroneze	Resolution	open => fixed
2019-07-05 11:41	signoles	Status	resolved => closed