[bitc-dev] {,de}allocation

[Sandro Magi]

Jonathan S. Shapiro wrote:
> On Mon, 2007-01-29 at 11:49 +0100, Pierre THIERRY wrote:
>> Scribit Jonathan S. Shapiro dies 28/01/2007 hora 19:18:
>>> There are two problems with the proof discharge story in general:
>>>
>>>   1. It requires whole-program analysis
>> Why? The few things I learned so far about proof of programs lead me to
>> think that usually you discharge proofs about post-conditions based on
>> pre-conditions, and about pre-conditions being verified at call sites.
>>
>> Can't that be made function by function and module by module?
> 
> In this case, no. Demonstrating that "free" is safe requires showing
> that the pointer value is unreachable. This requires whole-program flow
> analysis.

But only if the reference escapes the module scope, right?

Sandro