View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000314 | Frama-C | Plug-in > Eva | public | 2009-11-03 17:05 | 2014-02-12 16:56 | ||||
Reporter | akvadrako | ||||||||
Assigned To | pascal | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Beryllium-20090902 | ||||||||
Target Version | Fixed in Version | Frama-C Boron-20100401 | |||||||
Summary | 0000314: malloc.h can't be preprocessed: __func__ is not a macro | ||||||||
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); | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
pascal (reporter) 2009-11-04 12:16 |
Thank you for the suggested patch, but the point of the malloc macro in this header is to make sure that a string that identifies the malloc call in the program is passed to the value analysis built-in function Frama_C_alloc_infinite(). Since snprintf is not handled by the value analysis, this transformation would not help reach the goal. Plus, since you have come this far, you deserve to know that the undocumented Frama_C_alloc_infinite() built-in call works in ways that would it make it quite difficult to make your approach work. We really intended a literal string "computed" by the preprocessor to be passed here. May I recommend that you remove the __func__ part of the macro altogether, and keep identifying malloc calls in the source only by file and line? In principle, it's enough. The function name was there only for readability. A last more general word: we used this malloc.c file only to build difficult examples in a few lines of C (see for instance the benchmark in last section of article http://portal.acm.org/citation.cfm?id=1411308 , I can send you an electronic version if you are interested). You will surely encounter more problems if you try to use it. For instance including malloc.c from two separate files will surely cause issues. We initially focused on embedded C where dynamic allocation was a non-issue but we welcome any suggestions regarding how it can be handled, including this bug report for which we are grateful. |
pascal (reporter) 2009-11-04 16:48 |
Please find below the change I made instead. Do not hesitate to tell us about other problems you may encounter, whether with the malloc modelization or something else. Index: share/malloc.c =================================================================== --- share/malloc.c (revision 6767) +++ share/malloc.c (working copy) @@ -55,13 +55,13 @@ */ #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,__FILE__ "_line_" FRAMA_C_XSTRINGIFY(__LINE__))) #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* file) { + static int counter = 0; counter++; char *base = Frama_C_alloc_infinite(file); char *tag = Frama_C_alloc_infinite(base); |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2009-11-03 17:05 | akvadrako | New Issue | |
2009-11-03 17:05 | akvadrako | Status | new => assigned |
2009-11-03 17:05 | akvadrako | Assigned To | => pascal |
2009-11-04 12:16 | pascal | Note Added: 0000526 | |
2009-11-04 12:16 | pascal | Status | assigned => acknowledged |
2009-11-04 16:48 | pascal | Note Added: 0000531 | |
2009-11-04 16:49 | svn | ||
2009-11-04 16:49 | svn | Status | acknowledged => resolved |
2009-11-04 16:49 | svn | Resolution | open => fixed |
2010-04-13 15:30 | signoles | Status | resolved => new |
2010-04-13 15:31 | signoles | Status | new => closed |
2010-04-13 15:33 | signoles | Fixed in Version | => Frama-C Boron |
2013-12-19 01:13 | pascal | Source_changeset_attached | => framac master 9af4171e |
2013-12-19 01:14 | Source_changeset_attached | => framac master 08ac2c72 | |
2014-02-12 16:55 | pascal | Source_changeset_attached | => framac stable/neon 9af4171e |
2014-02-12 16:56 | Source_changeset_attached | => framac stable/neon 08ac2c72 | |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |