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.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: f849b,b8d52151b7b306d2
X-Google-Attributes: gidf849b,public
X-Google-Thread: 103376,a00006d3c4735d70
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-12-29 10:20:56 PST
From: iddw@hotmail.com (Dave Hansen)
Newsgroups: comp.arch.embedded,comp.lang.ada
Subject: Re: Certified C compilers for safety-critical embedded systems
Date: Mon, 29 Dec 2003 17:46:33 GMT
Message-ID: <3ff0686d.528369824@News.CIS.DFN.DE>
References: <3fe00b82.90228601@News.CIS.DFN.DE> <3FE026A8.3CD6A3A@yahoo.com>
 <$km9afA3DB7$EAYO@phaedsys.demon.co.uk>
 <bcEFNEK9esyI@eisner.encompasserve.org>
 <p$OIcVFWHL7$EA6t@phaedsys.demon.co.uk>
 <wccekur4151.fsf@shell01.TheWorld.com>
 <Xns945DE49836882jimmaureenrogers@204.127.36.1>
NNTP-Posting-Host: mail.nartron.com (216.65.187.224)
X-Trace: news.uni-berlin.de 1072719751 148409 216.65.187.224 ([97677])
X-Newsreader: Forte Free Agent 1.21/32.243
Path: 
 archiver1.google.com!news2.google.com!news.maxwell.syr.edu!news-han1.dfn.de!news-fra1.dfn.de!npeer.de.kpn-eurorings.net!rz.uni-karlsruhe.de!news.uni-ulm.de!newsfeed.in-ulm.de!uni-berlin.de!mail.nartron.COM!not-for-mail
Xref: archiver1.google.com comp.arch.embedded:6298 comp.lang.ada:3929
Date: 2003-12-29T17:46:33+00:00
List-Id: <comp.lang.ada>

Perhaps I should read further in the thread before replying, but I
just can't help it:

On Sat, 27 Dec 2003 05:29:44 GMT, James Rogers
<jimmaureenrogers@att.net> wrote:

[...]
>The C standard explicitly permits accessing one element beyond the end
>of an array. Neither the C compiler nor lint can determine if an array
>index is outside the bounds of the array. Ada compilers detect static
>references beyond the end of an array every time.
>
>Examples:
>
>int foo[10];
>
>int i;
>
>for(i = 0; i < 100; ++i)
>{
>   foo[i] = i;
>}
>
>Although human inspection clearly identifies the for loop indices
>to be beyond the bounds of the array, neither the C compiler nor lint
>will detect the problem. Since the problem can be clearly identified

This one's pretty easy for PC-lint.  Consider:

---begin included file---
C:\Dave>type lloop.c

void f(void)
{
    int foo[10];

    int i;

    for(i = 0; i < 100; ++i)
    {
       foo[i] = i;
    }
}

C:\Dave>lint-nt -u lloop.c
PC-lint for C/C++ (NT) Ver. 8.00n, Copyright Gimpel Software 1985-2003

--- Module:   lloop.c
                 _
       foo[i] = i;
lloop.c  10  Warning 662: Possible creation of out-of-bounds pointer
(90 beyond
    end of data) by operator '[' [Reference: file lloop.c: lines 8,
10]
lloop.c  8  Info 831: Reference cited in prior message
lloop.c  10  Info 831: Reference cited in prior message
                 _
       foo[i] = i;
lloop.c  10  Warning 661: Possible access of out-of-bounds pointer (90
beyond
    end of data) by operator '[' [Reference: file lloop.c: lines 8,
10]
lloop.c  8  Info 831: Reference cited in prior message
lloop.c  10  Info 831: Reference cited in prior message
_
}
lloop.c  12  Warning 550: Symbol 'foo' (line 4) not accessed
lloop.c  4  Info 830: Location cited in prior message

C:\Dave>
---end included file---

The "-u" option tells PC-lint to do a "unit" check, i.e., that the
referenced file is not a complete program, so it should suppress
errors like "Function f defined but not called."

Regards,

                               -=Dave
-- 
Change is inevitable, progress is not.