File frama-c/libc/features.h should include definition of the macro __GNUC_PREREQ from file /usr/include/features.h
ID0002253: This issue was created automatically from Mantis Issue 2253. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002253 | Frama-C | Kernel > libc | public | 2016-10-17 | 2017-12-06 |
| Reporter | Jochen | Assigned To | maroneze | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | xubuntu | OS Version | - |
| Product Version | Frama-C Aluminium | Target Version | - | Fixed in Version | Frama-C 16-Sulfur |
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.