2021-03-02 01:59 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000314Frama-CPlug-in > Evapublic2009-11-03 17:052014-02-12 16:56
Reporterakvadrako 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000314: malloc.h can't be preprocessed: __func__ is not a macro
DescriptionHi. 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 InformationPlease 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);
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0000526

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.

~0000531

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);
+Notes

-Issue History
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
+Issue History