From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 17351 invoked by alias); 25 Jan 2002 15:17:17 -0000 Mailing-List: contact gcc-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Archive: List-Post: List-Help: Sender: gcc-owner@gcc.gnu.org Received: (qmail 17318 invoked from network); 25 Jan 2002 15:17:15 -0000 Received: from unknown (HELO nile.gnat.com) (205.232.38.5) by sources.redhat.com with SMTP; 25 Jan 2002 15:17:15 -0000 Received: by nile.gnat.com (Postfix, from userid 338) id 6AA02F28AD; Fri, 25 Jan 2002 10:17:15 -0500 (EST) To: dan@dberlin.org, kenner@vlsi1.ultra.nyu.edu Subject: Re: g++ and aliasing bools Cc: gcc@gcc.gnu.org Message-Id: <20020125151715.6AA02F28AD@nile.gnat.com> Date: Fri, 25 Jan 2002 07:51:00 -0000 From: dewar@gnat.com (Robert Dewar) X-SW-Source: 2002-01/txt/msg01624.txt.bz2 <> 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.