Frama-C Bug Tracking System - Frama-C
View Issue Details
0000915Frama-CPlug-in > Evapublic2011-08-05 15:332014-02-12 16:54
Frama-C Carbon-20110201 
Frama-C Fluorine-20130401 
0000915: interest for a built-in memset function
The following command produces perfectly precise results on the attached example:
frama-c frama-c-lib.c $(frama-c -print-path)/libc.c -val -cpp-command 'gcc -C -E -I$(frama-c -print-path)' -main F1

On the contrary, analysing -main F2 instead of F1 yields unprecise results, unless unrolling is used. It would be of great interest, both for precision and performance, to have a Frama-C built-in for the memset library function, at least in the frequent case where the abstract value of the second parameter is just the {0} singleton.
No tags attached.
c frama-c-lib.c (334) 2011-08-05 15:33
Issue History
2011-08-05 15:33ddelmasNew Issue
2011-08-05 15:33ddelmasStatusnew => assigned
2011-08-05 15:33ddelmasAssigned To => pascal
2011-08-05 15:33ddelmasFile Added: frama-c-lib.c
2011-08-05 19:07pascalNote Added: 0002122
2011-08-05 19:07pascalNote Edited: 0002122
2011-08-05 23:21pascalNote Edited: 0002122
2012-04-05 22:44yakobowskiNote Added: 0002841
2012-05-19 18:38svnCheckin
2012-10-23 23:48yakobowskiAssigned Topascal => yakobowski
2012-10-25 14:48yakobowskiStatusassigned => resolved
2012-10-25 14:48yakobowskiResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

2011-08-05 19:07   
(edited on: 2011-08-05 23:21)
The 0 case is not really harder than other values. 0 repeats every bit. Other values repeats every 8 bits. The span of memory that should be written is a multiple of both 1 and 8 by construction, so it does not really make a difference.

Making a built-in that is as precise as possible (or even just works) for all possible abstract arguments passed to it is extremely difficult because of the variety of abstract values. It's not all "just" intervals, as some people on the internet may dismissively describe the value analysis' abstract values hierarchy.

You can build the use case you'll need implemented by implementing and analyzing with a memset() like this:

void* memset_c (void* dest, int val, size_t len)
  unsigned char *ptr = (unsigned char*)dest;
  while (len-- > 0)
    *ptr++ = val;
  return dest;

void* memset (void* dest, int val, size_t len)
  Frama_C_show_each_memset_args(dest, val, len);
  return memset_c(dest, val, len);

Making us implement a built-in that works only for simple arguments will be counter-productive for everyone, as you probably noticed in the case of the memcpy() built-in. We need the entire list of arguments you will be interested in for your project. (We'll assume for the moment that the existing contents for dest do not matter. They do, in fact: if len is not a singleton, they may make the task harder, for instance if they repeat every more than 8 bits)

Then, there is the issue of derived analyses. To make a long story short, when the other analyses (deps, in, out, ...) encounter the Frama_C_memset() built-in, they assume it's a library function because they do not know anything about it (only the value analysis knows about built-ins at this point) and treat it as a library function. This is not always what you might want, especially for a side-effecting built-in. Indeed, you may need a deps-computation Frama_C_memset() built-in if that's the analysis you use, or a out-computation built-in, ...

So what analyses you'll need is something else that we will need to know.

Making the complete built-in that pleases everyone is simply too much work and would stall more important developments.

2012-04-05 22:44   
Surprisingly, we have found that writing a really good memset builtin is even more difficult than writing one for memcpy. A bzero builtin will ship with Nitrogen, with the following restrictions:
- destination must be completely precise
- size must be completely precise

A memset builtin will be available with the commercial version of Frama-C. With a non-zero value for the parameter val, it will actually be more precise than the C version (on top of being considerably faster).