0002253: File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h

Notes
(0006280) maroneze (developer) 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 (reporter) 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 "<sys/socket.h>", 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 (developer) 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.

Issue History
Date Modified	Username	Field	Change
2016-10-17 17:36	Jochen	New Issue
2016-10-17 17:36	Jochen	Status	new => assigned
2016-10-17 17:36	Jochen	Assigned To	=> maroneze
2016-10-18 11:36	maroneze	Note Added: 0006280
2016-11-21 12:52	Jochen	Note Added: 0006287
2017-06-14 19:07	maroneze	Note Added: 0006408
2017-06-14 19:09	maroneze	Note Edited: 0006408	View Revisions
2017-06-14 19:12	maroneze	Status	assigned => resolved
2017-06-14 19:12	maroneze	Fixed in Version	=> Frama-C 15 Phosphorus
2017-06-14 19:12	maroneze	Resolution	open => fixed

Relationships