Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001140Frama-CKernelpublic2012-04-04 10:582014-02-12 16:54
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001140: Strange declaration mismatch
DescriptionDeclarations 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; }
TagsNo tags attached.
Attached Files

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

- 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 Checkin
2012-04-05 21:32 yakobowski Note Added: 0002838
2012-04-05 21:51 svn Checkin
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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker