[bitc-dev] {,de}allocation

[Jonathan S. Shapiro]

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.

> >   2. It relies on having asked the right questions.
> 
> Yes. As I was told, the hard thing is not to discharge proofs about
> code, it's being able fo formally specify the expected semantic of the
> code...
-- 
Jonathan S. Shapiro, Ph.D.
Managing Director
The EROS Group, LLC
+1 443 927 1719 x5100