[bitc-dev] {,de}allocation

[Jonathan S. Shapiro]

On Mon, 2007-01-29 at 11:52 -0500, Sandro Magi wrote:
> 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:

Yes, there are simple cases. Merely solving the simple cases isn't good
enough.
-- 
Jonathan S. Shapiro, Ph.D.
Managing Director
The EROS Group, LLC
+1 443 927 1719 x5100