Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #146
Closed
Open
Issue created Jun 15, 2014 by mantis-gitlab-migration@mantis-gitlab-migration

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking