0001140: Strange declaration mismatch - Frama-C Bug Tracking System

(0002823)
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,...)

(0002824)
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...

(0002825)
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.

(0002828)
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?

(0002829)
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 ???

(0002838)
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

Notes
(0002823) 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,...)

(0002824) 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...

(0002825) 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.

(0002828) 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?

(0002829) 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 ???

(0002838) 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.

Relationships