Frama-C news and ideas

To content | To menu | To search | Frama-C Home

free(): revisited already

If Frama-C doesn't work out, we can always make a comedy team

Facetious colleagues ask me how I make Frama-C's value analysis' messages so informative. "Pascal," one of them says, "in this case study, the generated log contains 8GiB of information! It won't open in Emacs...". I helpfully point out that it is probably a 2^32 thing and that he should use a 64-bit Emacs.

Informativeness with uninitialized variables

Consider the program below:

  int x = 1;
  int y;
  int z = 3;
  int t = 4;
  int u = 5;
  x += y;
  x += z;
  x += t;
  x += u;
  printf("%d\n", x);

A less informative analyzer would predict that the printf() call prints any number, or it might call the printed number "Uninitialized". Either way, the user would be dumbfounded. Ey would have to track the origin of this imprecise diagnostic emself. Going backwards from causes to origins, ey would finally end up to the declaration of local variable y, which ey intended to initialize but forgot to.

The value analysis tells you right there at line 7 (x += y;) that the program is doing something wrong, so that the way back up from cause to origin is much shorter. It's more informative to point out that the program is already doing something wrong at line 7 than to silently propagate a value indicating something wrong has happened somewhere.

Informativeness with dangling pointers

My most facetious colleague Anne wonders whether one shouldn't be allowed to increment q in the program from last post:

  int *p = malloc(12);
  int *q = p;


This program is treated analogously to that program, and by "analogously" I mean that the same functions are called behind the scenes and the same messages are printed:

  int *p;
  int *q;

    int a[3];
    p = a;
    q = p;

Could we allow q to be incremented?

In the example with free(), perhaps. In the example with a local variable a, the standard clearly calls the contents of q indeterminate, and it's allowable for a static analyzer to emit an alarm when indeterminate memory contents are used for anything except copying.

The standard is surprisingly brief when it comes to defining free().

The free function causes the space pointed to by ptr to be deallocated, that is, made available for further allocation. [...] if the argument does not match a pointer earlier returned by the calloc, malloc, or realloc function, or if the space has been deallocated by a call to free or realloc, the behavior is undefined.

Should we allow q to be incremented?

Well, I don't want to, for the same reason as in the uninitialized variable y example. This would postpone the moment the error is pointed out to the user, and give em extra work to track the programming error (which is to do anything with q after the free()/end of block. The informative solution is to warn at q++; And I take informativeness very seriously. (You've been a great audience. I'll be here all week)

I think the standard should say that any pointer previously pointing inside the freed space becomes indeterminate. Anyway, that's how it's treated in Frama-C's value analysis, and if you don't like it, you can use another analyzer, unless you are Anne, in which case you can't and you must use this one.


1. On Thursday, January 5 2012, 22:00 by _Anne_

Ok then :-) I have to agree with you ! I don't know yet if I quite understand why this should be an error instead of a warning, but I am to lazy to make some tests tonight... Good night !

2. On Thursday, January 5 2012, 23:00 by Chucky

As Pascal pointed out in his previous post,
"The value of a pointer becomes indeterminate when the object it points to (or just past) reaches the end of its lifetime." (n1570 6.2.4:2). Since free ends the lifetime of the allocated memory, all pointers that point to it (or just past) are suddenly made indeterminate.

The C99 rationale ( lines 25--32) has an example why this should be the case:
"Consider a hypothetical segmented architecture on which pointers comprise a segment descriptor and an offset. Suppose that segments are relatively small so that large arrays are allocated in multiple segments. While the segments are valid (allocated, mapped to real memory), the hardware, operating system, or C implementation can make these multiple segments behave like a single object: pointer arithmetic and relational operators use the defined mapping to impose the proper order on the elements of the array. Once the memory is deallocated, the mapping is no longer guaranteed to exist. Use of the segment descriptor might now cause an exception, or the hardware addressing logic might return meaningless data."

I think value analysis is doing the right thing here.