Frama-C Bug Tracking System - Frama-C
View Issue Details
0002253Frama-CKernel > libcpublic2016-10-17 17:362017-12-06 09:10
Jochen 
maroneze 
normalminoralways
closedfixed 
xubuntu
Frama-C Aluminium 
Frama-C 16-Sulfur 
0002253: File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h
The macro __GNUC_PREREQ is used in many system include files. It is defined in referring to "/usr/include/features.h"l. However, a "#include " directive is redirected by Frama-C to (e.g.) "~/.opam/system/share/frama-c/libc/features.h" which doesn't define the macro. Adding the definition there wouldn't cause any harm (? - at least, I can't think of any) and would help to make more system include files work with Frama-C.
No tags attached.
Issue History
2016-10-17 17:36JochenNew Issue
2016-10-17 17:36JochenStatusnew => assigned
2016-10-17 17:36JochenAssigned To => maroneze
2016-10-18 11:36maronezeNote Added: 0006280
2016-11-21 12:52JochenNote Added: 0006287
2017-06-14 19:07maronezeNote Added: 0006408
2017-06-14 19:09maronezeNote Edited: 0006408View Revisions
2017-06-14 19:12maronezeStatusassigned => resolved
2017-06-14 19:12maronezeFixed in Version => Frama-C 15-Phosphorus
2017-06-14 19:12maronezeResolutionopen => fixed
2017-12-06 09:09signolesFixed in VersionFrama-C 15-Phosphorus => Frama-C 16-Sulfur
2017-12-06 09:10signolesStatusresolved => closed

Notes
(0006280)
maroneze   
2016-10-18 11:36   
That could be useful, would you have just one or two examples of files where this would help? Just their names should suffice. Ideally, it'd be even better if the __GNUC_PREREQ would be the only thing currently preventing them from parsing with Frama-C. Note that sometimes these changes have unintended consequences, so they are somewhat slow to be integrated.
(0006287)
Jochen   
2016-11-21 12:52   
The problem occured when I used Linux' "/usr/include/socket.h", since Frama-C's "socket.h" doesn't define "SHUT_RD", "SHUT_WR", or "SHUT_RDWR", which were used as arguments to "shutdown" calls in my code. File "/usr/include/socket.h" includes "", where __GNUC_PREREQ is used in line 68. However, in this example, a lot of other problems are reported by Frama-C, so only defining __GNUC_PREREQ wouldn't make it work.
(0006408)
maroneze   
2017-06-14 19:07   
(edited on: 2017-06-14 19:09)
We are still unsure if defining __GNUC_PREREQ itself would be a good idea, since it potentially opens a whole can of worms (more specifically, which parts of Linux' "features.h" we should import, which compiler macros should be added, should we support Clang features, or MSVC's, etc.). Instead, we fixed the "socket.h" header (which now includes SHUT_RD and similar constants), which has been released in Phosphorus. We are also trying to improve compatibility of our headers with POSIX functions, which should minimize the need for such macros. Still, in some cases they are necessary, so in practical case studies, we often resort to using a special file, __fc_compatibility.h (it is available on the open-source-case-studies repository: https://github.com/Frama-C/open-source-case-studies/blob/master/__fc_compatibility.h ), which is included via -cpp-extra-args="-include__fc_compatibility.h". For instance, in open-source-case-studies, there are a few Makefiles which use it (hiredis, libmodbus, gzip124). By the way, libc-specific issues can also be reported directly to the open-source-case-studies Github repository, especially if the code is open source. That way, it may be integrated into our non-regression test suite to make sure it won't break in future releases.