(0006280)
maroneze (administrator)
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 "", 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 (administrator)
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.
|
Relationships 
Relationships