[bitc-dev] {,de}allocation

[Pierre THIERRY]

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?

Curiously,
Pierre
-- 
nowhere.man at levallois.eu.org
OpenPGP 0xD9D50D8A
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.coyotos.org/pipermail/bitc-dev/attachments/20070128/1eaf4b16/attachment.bin