mirror of https://lore.kernel.org/lkml/
 help / color / mirror / Atom feed
From: dewar@gnat.com
To: dewar@gnat.com, mrs@windriver.com, paulus@samba.org
Cc: gcc@gcc.gnu.org, linux-kernel@vger.kernel.org,
	trini@kernel.crashing.org, velco@fadata.bg
Subject: Re: [PATCH] C undefined behavior fix
Date: Tue,  8 Jan 2002 21:18:36 -0500 (EST)	[thread overview]
Message-ID: <20020109021836.53D84F2FFB@nile.gnat.com> (raw)

<<I noticed you failed to answer my question.  Why's that?  The answer
is, the standard is not a formal document.  If it were, you would be
able to point at the line that had the requirement that said it would
not scribble all over memory.  It is just that simple.
>>

Sorry, it *is* a formal document. Your question was with respect to Ada,
so if you are really interested here is the quote:

8   The external effect of the execution of an Ada program is defined in
terms of its interactions with its external environment.  The following are
defined as external interactions:

    9  Any interaction with an external file (see A.7);

   10  The execution of certain code_statements (see 13.8); which code_
       statements cause external interactions is implementation defined.

   11  Any call on an imported subprogram (see Annex B), including any
       parameters passed to it;

   12  Any result returned or exception propagated from a main
       subprogram (see 10.2) or an exported subprogram (see Annex B) to
       an external caller;

   13  Any read or update of an atomic or volatile object (see C.6);

   14  The values of imported and exported objects (see Annex B) at the
       time of any other interaction with the external environment.

Now the question is: does scribbling come under any of these definitions.
One would have to look at the particular definition of scribbling to know.
In particular, the compiler has to prove that such scribbling does not
violate 13 or 14. Rather hard, if you give me a specific example of a
an action performed by a scribbling compiler. I will tell you whether
it is conforming or not.

Note that the Ada standard also has the concept of implementation advice.
So one should also look there. It is not strictly normative, but in practice
has some semi-normative force.

The standard is most certainly a formal document in the legal sense. If
you are complaining that it is not mathematicaly precise, OK, but such
precision comes with other costs, so the intention of both the C and
Ada standards is that they are at an appropriate level of formality.

Of *course* it is the case that a conforming compiler that meets all the
requirements of the standards, and, in the case of Ada, also passes the
ISO approved validation suite (there is no such for C), may still be
complete junk for a given purpose (the original Ada-Ed compiler which
compiled Ada, and then executed it at the rate of about 1 statement 
per second was hardly useful for Mil-Aero applications :-)

             reply	other threads:[~2002-01-09  2:19 UTC|newest]

Thread overview: 202+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2002-01-09  2:18 dewar [this message]
  -- strict thread matches above, loose matches on Subject: below --
2002-01-10 19:01 Bernard Dautrevaux
2002-01-10 12:18 dewar
2002-01-10 12:37 ` Erik Trulsson
2002-01-10 15:27   ` Florian Weimer
2002-01-10  9:03 Bernard Dautrevaux
2002-01-10 10:40 ` David Weinehall
2002-01-10  4:33 dewar
2002-01-10  2:16 dewar
2002-01-10  1:22 dewar
2002-01-10  1:21 dewar
2002-01-10  4:37 ` Tim Hollebeek
2002-01-09 21:54 dewar
2002-01-09 20:32 dewar
2002-01-09 21:43 ` Paul Koning
2002-01-09 20:08 dewar
2002-01-09 19:53 mike stump
2002-01-09 20:12 ` Paul Koning
2002-01-09 10:42 dewar
2002-01-09 10:41 Bernard Dautrevaux
2002-01-09 21:59 ` Gérard Roudier
2002-01-09 10:40 dewar
2002-01-09  9:06 Bernard Dautrevaux
2002-01-09  9:25 ` Bernd Petrovitsch
2002-01-09  2:13 dewar
2002-01-09  1:51 mike stump
2002-01-09  1:19 dewar
2002-01-09  0:51 dewar
2002-01-08 11:12 Bernard Dautrevaux
2002-01-11  9:52 ` Horst von Brand
2002-01-08  9:44 Bernard Dautrevaux
2002-01-08 11:44 ` 'jtv'
2002-01-08  0:16 mike stump
2002-01-08 11:33 ` jtv
2002-01-07 23:46 mike stump
2002-01-07 23:20 dewar
2002-01-07 23:15 dewar
2002-01-07 23:12 dewar
2002-01-07 23:11 dewar
2002-01-07 22:56 mike stump
2002-01-07 22:26 Tim McDaniel
2002-01-07 19:36 mike stump
2002-01-07 21:21 ` Theodore Tso
2002-01-08  0:19 ` Paul Mackerras
2002-01-08  1:02   ` Richard Henderson
2002-01-07 19:18 mike stump
2002-01-07 19:17 Bernard Dautrevaux
2002-01-07 18:38 mike stump
2002-01-07 13:29 Bernard Dautrevaux
2002-01-07 13:24 Bernard Dautrevaux
2002-01-07 21:49 ` jtv
2002-01-07 22:28   ` Tim Hollebeek
2002-01-07 22:16     ` jtv
2002-01-08  0:27       ` J.A. Magallon
2002-01-08 11:41         ` jtv
2002-01-08 12:36           ` Alexandre Oliva
2002-01-08 12:58             ` jtv
2002-01-09 19:47         ` Gérard Roudier
2002-01-09 20:44           ` jtv
2002-01-09 23:49           ` J.A. Magallon
2002-01-10 10:13             ` Matthias Benkmann
2002-01-10  0:19           ` Peter Barada
2002-01-10  1:47             ` Fergus Henderson
2002-01-10 15:30             ` Peter Barada
2002-01-10 10:44           ` Bernd Petrovitsch
2002-01-06 19:32 dewar
2002-01-06 19:29 dewar
2002-01-06 19:29 dewar
2002-01-06 18:37 mike stump
2002-01-06 18:24 mike stump
2002-01-06 20:37 ` Gabriel Dos Reis
2002-01-06 21:59 ` Paul Mackerras
2002-01-06 22:19   ` Jakub Jelinek
2002-01-07  0:09     ` Tom Rini
2002-01-07  1:40       ` Alexandre Oliva
2002-01-06 18:20 mike stump
2002-01-06 16:22 dewar
2002-01-06 16:39 ` Alan Cox
2002-01-06 19:27   ` Laurent Guerby
2002-01-06 19:43     ` Alan Cox
2002-01-06 13:43 dewar
2002-01-06 13:55 ` Laurent Guerby
2002-01-06 13:41 dewar
2002-01-06 16:58 ` Gabriel Dos Reis
2002-01-06 13:16 dewar
2002-01-06 13:22 ` Gabriel Dos Reis
2002-01-06 13:07 dewar
2002-01-06 13:05 dewar
2002-01-06 13:41 ` Laurent Guerby
2002-01-06  7:56 mike stump
2002-01-06  4:26 dewar
2002-01-06  5:32 ` Paul Mackerras
2002-01-06 11:09   ` Momchil Velikov
2002-01-06  0:52 dewar
2002-01-04 22:43 dewar
2002-01-06  3:40 ` Paul Mackerras
2002-01-04 12:15 dewar
2002-01-04 12:14 dewar
2002-01-03 13:28 dewar
2002-01-04  8:38 ` Florian Weimer
2002-01-04 11:35   ` Joseph S. Myers
2002-01-05 19:25     ` jkl
2002-01-05 19:37       ` Joseph S. Myers
2002-01-05 20:06         ` jkl
2002-01-05 21:42           ` Joseph S. Myers
2002-01-05 20:01       ` Florian Weimer
2002-01-05 20:17         ` jkl
2002-01-05 20:51           ` Florian Weimer
2002-01-06  4:09       ` Paul Mackerras
2002-01-03 12:51 dewar
2002-01-03 10:35 Bernard Dautrevaux
2002-01-03 10:05 Bernard Dautrevaux
2002-01-03 10:49 ` Paul Mackerras
2002-01-03 11:59   ` Lars Brinkhoff
2002-01-03 23:53   ` Paul Mackerras
2002-01-04  9:52     ` Lars Brinkhoff
2002-01-05  6:45     ` Paul Mackerras
2002-01-06  0:20       ` Lars Brinkhoff
2002-01-09  9:28   ` Fergus Henderson
2002-01-09 10:58     ` Gabriel Dos Reis
2002-01-03  0:49 dewar
2002-01-03  0:12 dewar
2002-01-03  0:32 ` jtv
2002-01-06 19:37   ` Alexandre Oliva
2002-01-02 23:53 dewar
2002-01-02 23:59 ` Joe Buck
2002-01-03  3:12 ` Paul Mackerras
2002-01-03 15:45   ` Joe Buck
2002-01-02 17:40 Petr Vandrovec
2002-01-02 22:24 ` David Woodhouse
2002-01-02 22:39   ` Joe Buck
2002-01-02 22:59     ` David Woodhouse
2002-01-03 18:44   ` Alexandre Oliva
2002-01-02 10:02 Bernard Dautrevaux
2002-01-02 23:02 ` Paul Mackerras
2002-01-02 23:27   ` Momchil Velikov
2002-01-01 23:03 Momchil Velikov
2002-01-01 23:43 ` Tom Rini
2002-01-02  6:54   ` Momchil Velikov
2002-01-02 15:39     ` Tom Rini
2002-01-02 15:50       ` Jakub Jelinek
2002-01-02 16:45         ` Paul Koning
2002-01-02 14:56   ` Joseph S. Myers
2002-01-02 22:56   ` Paul Mackerras
2002-01-02 23:37     ` Momchil Velikov
2002-01-03  2:51     ` Paul Mackerras
2002-01-03  6:29       ` law
2002-01-03 13:16         ` Lars Brinkhoff
2002-01-04  9:05     ` Florian Weimer
2002-01-04 22:14     ` Paul Mackerras
2002-01-02 10:29 ` Florian Weimer
2002-01-02 10:41   ` Momchil Velikov
2002-01-02 13:11     ` Jakub Jelinek
2002-01-02 15:54       ` Tom Rini
2002-01-02 11:28 ` Aaron Lehmann
2002-01-02 11:40   ` Momchil Velikov
2002-01-02 15:59     ` Tom Rini
2002-01-02 11:48   ` Alan Cox
2002-01-02 19:09 ` Tom Rini
2002-01-02 20:13   ` Joe Buck
2002-01-02 20:42     ` Tom Rini
2002-01-02 21:36   ` Richard Henderson
2002-01-02 22:05     ` Tom Rini
2002-01-02 22:23       ` jtv
2002-01-02 23:12         ` Tom Rini
2002-01-02 23:45           ` jtv
2002-01-03  0:01             ` Tom Rini
2002-01-03  0:07               ` Richard Henderson
2002-01-03  0:16                 ` Tom Rini
2002-01-03  1:12                   ` Richard Henderson
2002-01-03  0:20                 ` jtv
2002-01-03  0:25               ` Alan Cox
2002-01-03  0:35                 ` David Woodhouse
2002-01-03  2:10                   ` Tom Rini
2002-01-03 22:39                     ` Pavel Machek
2002-01-04  9:29                     ` Paul Mackerras
2002-01-03 15:46                   ` Edgar Toernig
2002-01-03 16:48                     ` Momchil Velikov
2002-01-03 17:13                     ` jtv
2002-01-03 21:26                   ` Daniel Jacobowitz
2002-01-03  2:33               ` Paul Mackerras
2002-01-03  8:32                 ` Richard Henderson
2002-01-03 10:03                 ` Geert Uytterhoeven
2002-01-03 10:10                 ` Paul Mackerras
2002-01-03 22:41                   ` Tim Hollebeek
2002-01-04  8:48                   ` Florian Weimer
2002-01-02 22:27       ` Richard Henderson
2002-01-02 22:35         ` Tom Rini
2002-01-02 22:44           ` Richard Henderson
2002-01-02 22:50             ` Tom Rini
2002-01-03 22:40         ` Pavel Machek
2002-01-04  8:42           ` Richard Henderson
2002-01-04  8:42   ` Florian Weimer
2002-01-02 23:11 ` Paul Mackerras
2002-01-02 23:26   ` Tom Rini
2002-01-02 23:28   ` Momchil Velikov
2002-01-02 23:34     ` Tom Rini
2002-01-03  0:19       ` jtv
2002-01-03  0:29         ` Tom Rini
2002-01-03  1:03           ` jtv
2002-01-03  1:17             ` Tom Rini
2002-01-03 17:44               ` jtv

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20020109021836.53D84F2FFB@nile.gnat.com \
    --to=dewar@gnat.com \
    --cc=gcc@gcc.gnu.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=mrs@windriver.com \
    --cc=paulus@samba.org \
    --cc=trini@kernel.crashing.org \
    --cc=velco@fadata.bg \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox

Powered by JetHome