malloc.h can't be preprocessed: __func__ is not a macro
ID0000314: This issue was created automatically from Mantis Issue 314. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0000314 | Frama-C | Plug-in > Eva | public | 2009-11-03 | 2014-02-12 |
Reporter | akvadrako | Assigned To | pascal | Resolution | fixed |
Priority | normal | Severity | minor | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | Frama-C Boron-20100401 |
Description :
Hi. The included sample malloc.h does not compile because func is not a macro, but a static string variable. I am using clang/LLVM to preprocess my code. Also, please add "int" to the counter declaration, to avoid warnings. Thanks
C99, 6.4.2.2 #1 says:
The identifier func shall be implicitly declared by the translator as if, immediately following the opening brace of each function definition, the declaration
static const char func[] = "function-name";
Additional Information :
Please apply this patch. It's not ideal, because it uses snprintf. But at least the code is valid C:
--- tmp/frama-c-Beryllium-20090902-why-2.21/share/malloc.c 2009-09-23 15:21:30.000000000 +0000 +++ /usr/local/share/frama-c/malloc.c 2009-11-03 15:46:47.000000000 +0000 @@ -55,13 +55,15 @@ */ #define FRAMA_C_STRINGIFY(x) #x #define FRAMA_C_XSTRINGIFY(x) FRAMA_C_STRINGIFY(x) -#define malloc(x) (Frama_C_malloc_at_pos(x,FILE "function" func "line" FRAMA_C_XSTRINGIFY(LINE))) +#define malloc(x) (Frama_C_malloc_at_pos(x,func,LINE,FILE)) #define FRAMA_C_LOCALIZE_WARNING(x) (x " file " FILE " line " FRAMA_C_XSTRINGIFY(LINE)) #define FRAMA_C_VALID 1 #define FRAMA_C_FREED 2
- static void Frama_C_malloc_at_pos(size_t size,const char file) {
- static counter = 0;
- static void *Frama_C_malloc_at_pos(size_t size,const char func,int line,const char file) {
- char pos[100];
- snprintf(pos, 100, "%s_function_%s_line_%i", file, func, line);
- static int counter = 0; counter++; char *base = Frama_C_alloc_infinite(file); char *tag = Frama_C_alloc_infinite(base);