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:

main(){
  int x = 1;
  int y;
  int z = 3;
  int t = 4;
  int u = 5;
  x += y;
  x += z;
  x += t;
  x += u;
  printf("%d"  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:

main(){
  int *p = malloc(12);
  int *q = p;
  Frama_C_dump_each();
  free(p);
  q++;
  ...
}

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:

main(){
  int *p;
  int *q;
  {
    int a[3];
    p = a;
    q = p;
    Frama_C_dump_each();
  }
  q++;
  ...
}

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.