g++ and aliasing bools

[Robert Dewar]

<<Undecidability is not just based on run-time behavior of the program.
It's also undecidable in the static case.
may-alias is undecidable statically, as is must-alias (Unless i'm
misremembering).
>>

This is confused.

May-alias is a predicate with many possible solutions. One not very useful
solution is that anything may alias anything else. We are not interested
in whether something actually IS aliased at run time. We are interested
just in the subset of cases that we can prove do NOT alias. 

The problem before us is to narrow down the may-alias relationship as far
as possible statically. There is no issue of undecidability here. If we
propose that may-alias (a,b) is false, then either we can prove it or
we cannot. If we cannot, then we cannot proceed on the basis that
may-alias (a,b) is false.

I mean by prove here: demonstrate in a manner that generates sufficient
confidence.

A very formal mathematical proof might or might not suffice (if a proof is
too complex, it does not generate confidence, since, like a complex program
it may have a hard to find bug). We can hardly talk about machine verified
proofs in this context.

A demonstration MIGHT come from a test suite if the test suite was
sufficiently comprehensive in some appropriate sense (after all, testing
is the main method for proof of reliability of safety critical software,
such as is used in nuclear power plants and avionics, but it is pretty
formal comprehensive testing, requiring e.g. full coverage testing, including
full MCDC testing).

I think what is being said here is that people do not feel that the existing
test suite, which was not designed at all to test reliability of aliasing
analysis, is anywhere near meeting the criterion of generating sufficient
confidence.