Re: Not intended for use in medical,

[kaz@vision.crest.nt.com (Kaz Kylheku)]

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.