Double free(), no such thing

I have been able to divert a few hours yesterday and today for programming. It was well worth it, as I have discovered a theorem. It is new to me, and I wonder whether it was ever published. The theorem is, a C program cannot double free() a block even if it tries! I thought this deserved an announcement. Some students I know would be glad to hear that.

Indeed, a C program can at most pass an indeterminate value to a function. This is highly objectionable in itself. Students, don't write programs that do this either!

Allow me to demonstrate on the following program:

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

You might think that the program above double-frees the block allocated and referenced by p. But it doesn't: after the first call to free(), the contents of q are indeterminate, so that it's impossible to free the block a second time. I will insert a few calls to primitive function Frama_C_dump_each() to show what happens:

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

$ frama-c -val this_is_not_a_double_free.c 

The analysis follows the control flow of the program. First a block is allocated, and a snapshot of the memory state is printed a first time in the log:

... 
[value] computing for function malloc <- main. 
        Called from test.c:12. 
[value] Recording results for malloc 
[value] Done for function malloc 
[value] DUMPING STATE of file test.c line 15 
        p ∈ {{ &Frama_C_alloc }} 
        q ∈ {{ &Frama_C_alloc }} 
        =END OF DUMP== 
... 

Then free() is called and a second snapshot is logged:

... 
[value] computing for function free <- main. 
        Called from test.c:16. 
[value] Recording results for free 
[value] Done for function free 
[value] DUMPING STATE of file test.c line 17 
        p ∈ ESCAPINGADDR 
        q ∈ ESCAPINGADDR 
        =END OF DUMP== 
... 

And then, at the critical moment, the program passes an indeterminate value to a function:

... 
test.c:18:[kernel] warning: accessing left-value q that contains escaping addresses; 
                      assert(Ook) 
test.c:18:[kernel] warning: completely undefined value in {{ q -> {0} }} (size:<32>). 
test.c:18:[value] Non-termination in evaluation of function call expression argument 
        (void *)q 
... 
[value] Values at end of function main: 
          NON TERMINATING FUNCTION 

Note how the last call to Frama_C_dump_each() is not even printed. Execution stops at the time of calling the second free(). Generalizing this reasoning to all attempts to call free() twice, we demonstrate it is impossible to double-free a memory block.

QED

Question: does it show too much that this detection uses the same mechanism as the detection for addresses of local variables escaping their scope? I can change the message if it's too confusing. What would a better formulation be?

As I hope I have made clear, the message will be displayed as soon as the program does anything at all with a pointer that has been freed — and indeed, I have not implemented any special check for double frees. The program below is forbidden just the same, and does not get past the q++;

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

On the other hand, I still have to detect that the program does not free a global variable, something the analysis currently allows to great comical effect. (Hey, I have only had a couple of hours!)

Please leave your thoughts in the comments.