Strange declaration mismatch
ID0001140: This issue was created automatically from Mantis Issue 1140. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001140 | Frama-C | Kernel | public | 2012-04-04 | 2014-02-12 |
| Reporter | Anne | Assigned To | monate | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
Declarations from different include files do not match, but it seems to me that they are the same. For example:
- in frama-c/libc/string.h: extern void *memset(void *s, int c, size_t n);
- in frama-c/libc.h: void* memset (void* dest, int val, size_t len);
/usr/local/share/frama-c/libc.h:30:[kernel] user error: Declaration of memset does not match previous declaration from /usr/local/share/frama-c/libc/string.h:81 (different integer types).
How could I use both builtin.h (which includes libc.h) and string.h then ?
Additional Information :
$ frama-c toto.c
with the following toto.c:
#include "/usr/local/share/frama-c/libc/string.h" #include "/usr/local/share/frama-c/libc.h" int main (void) { return 0; }