|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002253||Frama-C||Kernel > libc||public||2016-10-17 17:36||2017-12-06 09:10|
|Product Version||Frama-C Aluminium|
|Target Version||Fixed in Version||Frama-C 16-Sulfur|
|Summary||0002253: File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h|
|Description||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 <features.h>" 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.
|Tags||No tags attached.|
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.
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.
Last edited: 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.
|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|
|2017-12-06 09:09||signoles||Fixed in Version||Frama-C 15-Phosphorus => Frama-C 16-Sulfur|
|2017-12-06 09:10||signoles||Status||resolved => closed|