2021-03-02 02:41 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001140Frama-CKernelpublic2014-02-12 16:54
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityhave not tried
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




monate (reporter)

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)

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)

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;
  # 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)

Ok, thanks for the information. Which function in builtin.h do you need? Isn't it present in libc/__fc_builtin.h?


Anne (reporter)

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)

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