| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001140 | Frama-C | Kernel | public | 2012-04-04 10:58 | 2014-02-12 16:54 | ||||
| Reporter | Anne | ||||||||
| Assigned To | monate | ||||||||
| Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Nitrogen-20111001 | ||||||||
| Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
| Summary | 0001140: Strange declaration mismatch | ||||||||
| 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; } | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
monate (reporter) 2012-04-04 15:40 |
Hi, You should not mix files from share/frama-c/libc/ with files from share/frama-c/ They are not supposed to be compatible at all. Anyway, you should post your preprocessed files because the result of the preprocessor may depend on various things (environment variables, automatic search path of the preprocessor,...) |
|
Anne (reporter) 2012-04-04 15:59 |
Thanks Benjamin. As you can see in the "Additional Information", the test file if very simple: the 3 lines above, and nothing else, but I'll take a look at the preprocessed file and post the result. I usually take the C library from share/frama-c/libc/, but this time, I also needed "builtin.h" to be able to use [Frama_C_nondet] :-/ So you say that I cannot use both ? That is a little annoying... |
|
Anne (reporter) 2012-04-04 16:07 |
Ok, I understand now. There is : # 1 "/usr/local/share/frama-c/libc.h" 1 # 63 "/usr/local/share/frama-c/machine.h" // This is the default for regression tests typedef unsigned long int size_t; and: # 29 "/usr/local/share/frama-c/libc/string.h" 2 # 1 "/usr/local/share/frama-c/libc/stddef.h" 1 # 1 "/usr/local/share/frama-c/libc/__fc_machdep.h" 1 # 26 "/usr/local/share/frama-c/libc/__fc_define_size_t.h" 2 typedef unsigned int size_t; and the two definitions are not compatible of course... I temporally solved my problem by stopping using frama-c/libc/ to be able to use builtin.h. |
|
monate (reporter) 2012-04-04 16:20 |
Ok, thanks for the information. Which function in builtin.h do you need? Isn't it present in libc/__fc_builtin.h? |
|
Anne (reporter) 2012-04-04 16:24 |
As I said, I use Frama_C_nondet. Yes, it is in libc/__fc_builtin.h, but am I suppose to include those __fc_xxx.h ??? |
|
yakobowski (manager) 2012-04-05 21:32 |
@Anne: you're not really supposed to include the __fc_xxx.h files explicitly, the .c file should do that by themselves. It seems that __fc_builtin.c is missing this include. This will be corrected for Nitrogen. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2012-04-04 10:58 | Anne | New Issue | |
| 2012-04-04 15:40 | monate | Note Added: 0002823 | |
| 2012-04-04 15:59 | Anne | Note Added: 0002824 | |
| 2012-04-04 16:07 | Anne | Note Added: 0002825 | |
| 2012-04-04 16:20 | monate | Note Added: 0002828 | |
| 2012-04-04 16:24 | Anne | Note Added: 0002829 | |
| 2012-04-05 09:26 | signoles | Status | new => assigned |
| 2012-04-05 09:26 | signoles | Assigned To | => monate |
| 2012-04-05 20:31 | svn | ||
| 2012-04-05 21:32 | yakobowski | Note Added: 0002838 | |
| 2012-04-05 21:51 | svn | ||
| 2012-04-06 03:31 | monate | Status | assigned => resolved |
| 2012-04-06 03:31 | monate | Fixed in Version | => Frama-C Oxygen-2012xx01 |
| 2012-04-06 03:31 | monate | Resolution | open => fixed |
| 2012-09-19 17:16 | signoles | Status | resolved => closed |
| 2013-12-19 01:12 | yakobowski | Source_changeset_attached | => framac master d2cb892f |
| 2013-12-19 01:12 | svn | Source_changeset_attached | => framac master 95ca626e |
| 2014-02-12 16:54 | yakobowski | Source_changeset_attached | => framac stable/neon d2cb892f |
| 2014-02-12 16:54 | monate | Source_changeset_attached | => framac stable/neon 95ca626e |
| Issue History |