From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <gcc-return-116513-listarch-gcc=gcc.gnu.org@gcc.gnu.org>
Received: (qmail 9889 invoked by alias); 29 Jun 2005 01:14:34 -0000
Mailing-List: contact gcc-help@gcc.gnu.org; run by ezmlm
Precedence: bulk
List-Archive: <http://gcc.gnu.org/ml/gcc/>
List-Post: <mailto:gcc@gcc.gnu.org>
List-Help: <http://gcc.gnu.org/ml/>
Sender: gcc-owner@gcc.gnu.org
Received: (qmail 9866 invoked by uid 22791); 29 Jun 2005 01:14:26 -0000
Received: from smtp-103-wednesday.nerim.net (HELO kraid.nerim.net) (62.4.16.103)
    by sourceware.org (qpsmtpd/0.30-dev) with ESMTP; Wed, 29 Jun 2005 01:14:26 +0000
Received: from uniton.integrable-solutions.net (gdr.net1.nerim.net [62.212.99.186])
	by kraid.nerim.net (Postfix) with ESMTP id E5B8640F56;
	Wed, 29 Jun 2005 03:14:22 +0200 (CEST)
Received: from uniton.integrable-solutions.net (localhost [127.0.0.1])
	by uniton.integrable-solutions.net (8.12.10/8.12.10/SuSE Linux 0.7) with ESMTP id j5T1DjKY006854;
	Wed, 29 Jun 2005 03:13:45 +0200
Received: (from gdr@localhost)
	by uniton.integrable-solutions.net (8.12.10/8.12.10/Submit) id j5T1DjuJ006853;
	Wed, 29 Jun 2005 03:13:45 +0200
To: Robert Dewar <dewar@adacore.com>
Cc: Georg Bauhaus <bauhaus@futureapps.de>, gcc mailing list <gcc@gcc.gnu.org>
Subject: Re: signed is undefined and has been since 1992 (in GCC)
References: <27fdc0d8dc588cfdb3a14a153c5d037c@physics.uc.edu>
	<m3fyv3je0t.fsf@uniton.integrable-solutions.net>
	<6d9fa260f233e519762c7d11276a35ad@physics.uc.edu>
	<m3hdfjhxok.fsf@uniton.integrable-solutions.net>
	<3dbad9a6bd7eb1aea74ff2245eaa1b99@physics.uc.edu>
	<m3br5rhvgm.fsf@uniton.integrable-solutions.net>
	<42C115D5.8070503@adacore.com>
	<m3psu6hfau.fsf@uniton.integrable-solutions.net>
	<42C13D4D.9040604@adacore.com>
	<m3d5q6fyrf.fsf@uniton.integrable-solutions.net>
	<42C14930.40402@adacore.com>
	<m3br5qei15.fsf@uniton.integrable-solutions.net>
	<42C1D610.6030701@futureapps.de>
	<m3zmtakpig.fsf@uniton.integrable-solutions.net>
	<42C1EAEF.8010400@adacore.com>
	<m3oe9qkn6x.fsf@uniton.integrable-solutions.net>
	<42C1EFEA.6020602@adacore.com>
From: Gabriel Dos Reis <gdr@integrable-solutions.net>
In-Reply-To: <42C1EFEA.6020602@adacore.com>
Date: Wed, 29 Jun 2005 01:14:00 -0000
Message-ID: <m31x6mj77a.fsf@uniton.integrable-solutions.net>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-SW-Source: 2005-06/txt/msg01224.txt.bz2

Robert Dewar <dewar@adacore.com> writes:

| Gabriel Dos Reis wrote:
| > Robert Dewar <dewar@adacore.com> writes:
| > | Gabriel Dos Reis wrote:
| > | | >  C is
| > | > trustworthy (and preferred over SML for that curcial part of the proof
| > | > checker) because the mapping of the C code to the generated assembly
| > | > code is straighforward and amenable to inspection.
| > | | This kind of traceability is of course vital for such
| > applications, but
| > | it is by no means unique to C,
| > Nobody claims it is unique to C.  You're after the wrong target.
| > | and there is a big difference between saying
| > | that C is an assembly language, and that the mapping of C to assembly
| > | language is transparent.
| > Oh, you denied any connection in previous message.
| 
| Not at all,

   > Please do remember that this is hardware dependent.  If you have
   > problems with x86, it does not mean you have the same witha PPC or a
   > Sparc.

   But the whole idea of hardware semantics is bogus, since you are
   assuming some connection between C and the hardware which does not
   exist. C is not an assembly language.

[...]

|      You did not read anything even vaguely saying that in what I wrote.

and you, did you?

-- Gaby