2021-01-27 12:08 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002253Frama-CKernel > libcpublic2016-10-17 17:362017-12-06 09:10
ReporterJochen 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSxubuntuOS Version
Product VersionFrama-C Aluminium 
Target VersionFixed in VersionFrama-C 16-Sulfur 
Summary0002253: File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h
DescriptionThe 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.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~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 "<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 (administrator)

2017-06-14 19:07

Last edited: 2017-06-14 19:09

View 2 revisions

 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.
+Notes

-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
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
+Issue History