From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,d1df6bc3799debed
X-Google-Attributes: gid103376,public
From: kaz@vision.crest.nt.com (Kaz Kylheku)
Subject: Re: Not intended for use in medical,
Date: 1997/04/29
Message-ID: <5k5ifi$8db@bcrkh13.bnr.ca>#1/1
X-Deja-AN: 238229660
References: <3.0.32.19970423164855.00746db8@mail.4dcomm.com>
 <3364C8EC.4879@DIE_SPAMMER.dasd.honeywell.com> <dewar.862270256@merv>
Organization: Prism Systems Inc.
Newsgroups: comp.lang.ada
Date: 1997-04-29T00:00:00+00:00
List-Id: <comp.lang.ada>


In article <dewar.862270256@merv>, Robert Dewar <dewar@merv.cs.nyu.edu> wrote:
>John said
>
><<If it were me designing life support systems for medical use I'd:
>Make use of Appendix H (Safety and Security) in Ada95.
>Review the object code.
>And then test the hell out of it like my life depended on it.>>
>
>This sounds like depending on testing too much, and on formal methods
>too little -- there is a balance sure, but the above seems unbalanced.

Reviewing the object code is (or can be) a formal method. Maybe the
use of the word ``hell'' shifts the perception of balance. :)

It's a pity that this discussion was confined to comp.lang.ada, because I
missed a lot of it, even though I sparked it with quote from the Intel
document.

Reviewing object code is important. I do it all the time, no matter what
langauge I'm using. Compiler bugs do exist; I have discovered a few in
GNU C. (just read gnu.gcc.bug over some time and you will see).

For example, here is one I found myself:

/*
 * Program demonstrating bug in GCC 2.7.2 (i386, -O2 -Wall -ansi)
 *
 * Sample output:
 *
 * foo(0,5) = 0; bar(0,5) = 0
 * foo(1,5) = 1; bar(1,5) = 1
 * foo(2,5) = 1; bar(2,5) = 1
 * foo(3,5) = 1; bar(3,5) = 1
 * foo(4,5) = 1; bar(4,5) = 0	<--- should be same for foo() and bar()
 * foo(5,5) = 0; bar(5,5) = 0
 * foo(6,5) = 0; bar(6,5) = 0
 * foo(7,5) = 0; bar(7,5) = 0
 * foo(8,5) = 0; bar(8,5) = 0
 */

#include <stdio.h>

int foo(int x, int y)

{
	return ((x < y) && x++) && ((x < y) && x++);
}

int bar(int x, int y)

{
	return (x < y) && x++ && (x < y) && x++;
}

/*
 * GCC seems to illegaly optimize foo() by factoring the (x < y)
 * as a common subexpression ignoring the x++ side effect, e.g:
 *
 *     return ((x < y) && x++) && x++;
 *
 * A more complex version of this expression has caused a serious
 * failure in some of my code.
 */

int main(void)
{
    int i;

    for (i = 0; i < 9; i++)
	printf("foo(%d,5) = %d; bar(%d,5) = %d\n", i, foo(i,5), i, bar(i,5));

    return 0;
}


I readily discovered this problem when my program was behaving oddly, and
a thorough code inspection failed to turn up any error in the source.


Heck, I've even seen serious bugs in _assemblers_.  This is quite surprising,
given that an assembler is at most a one-man project lasting several weeks,
unless you are doing it _in_ assembly :).  I used an assembler once which,
under peculiar circumstances, failed to synchronize its two passes.  It would
insert some padding ``no operations'' in one pass which were not accounted for
in its back-patching. All relative references crossing that NOOP, and all
absolute references to any labels _after_ the NOOP, were offset by the
length of the instruction.  Fortunately, this was detected easily.