[bitc-dev] {,de}allocation

[Jonathan S. Shapiro]

On Sun, 2007-01-28 at 23:22 +0100, Pierre THIERRY wrote:
> Scribit Jonathan S. Shapiro dies 28/01/2007 hora 11:15:
> > The "free" keyword is reserved, but allowing it to be invoked without
> > discharge creates safety issues. Having said that, I should admit a
> > sleazy hidden fact: the prover will need DEFAXIOM to allow programmers
> > to introduce facts that cannot be proved. In particular, DEFAXIOM is
> > needed to describe the behavior of assembly support routines. So free
> > can be used badly if desired.
> 
> But shouldn't adding axioms be rarely needed, and controlled?

Rarely needed? yes. Controlled? how?

There are two problems with the proof discharge story in general:

  1. It requires whole-program analysis
  2. It relies on having asked the right questions.

In the current case, the right thing is to avoid using free in the first
place whenever that is possible.

shap