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] Done for function free
[value] DUMPING STATE of file test.c line 17
=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!)