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;
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.
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).