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=-0.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM, FREEMAIL_REPLY autolearn=no 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 17:53:38 PST Path: archiver1.google.com!news2.google.com!newsfeed2.dallas1.level3.net!news.level3.com!crtntx1-snh1.gtei.net!news.gtei.net!chcgil2-snh1.gtei.net!news.bbnplanet.com!wn13feed!worldnet.att.net!bgtnsc05-news.ops.worldnet.att.net.POSTED!not-for-mail Newsgroups: comp.arch.embedded,comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems From: James Rogers References: <3fe00b82.90228601@News.CIS.DFN.DE> <3FE026A8.3CD6A3A@yahoo.com> <$km9afA3DB7$EAYO@phaedsys.demon.co.uk> <3ff0686d.528369824@News.CIS.DFN.DE> Message-ID: User-Agent: Xnews/5.04.25 Date: Tue, 30 Dec 2003 01:53:38 GMT NNTP-Posting-Host: 12.73.182.220 X-Complaints-To: abuse@worldnet.att.net X-Trace: bgtnsc05-news.ops.worldnet.att.net 1072749218 12.73.182.220 (Tue, 30 Dec 2003 01:53:38 GMT) NNTP-Posting-Date: Tue, 30 Dec 2003 01:53:38 GMT Organization: AT&T Worldnet Xref: archiver1.google.com comp.arch.embedded:6315 comp.lang.ada:3942 Date: 2003-12-30T01:53:38+00:00 List-Id: iddw@hotmail.com (Dave Hansen) wrote in news:3ff0686d.528369824@News.CIS.DFN.DE: > 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 > 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; > } > } > How well does PC-lint catch the following variation: void f(int *foo) { int i; for(i = 0; i < 100; ++i) { foo[i] = i; } } int main(int argc, char *argv[]) { int bar[10]; f(bar); } The abstract error is the same, yet function f has no visibility to the size of the actual array being passed to it. In fact, function f does not have any assurance that its actual parameter will even point to an array. C syntax simply does not provide the information needed within the called function. Compare that with the Ada syntax for dealing with arrays. procedure main is type small_index is range 1..10; type small_array is array(small_index) of integer; bar : small_array; procedure f(foo : in out small_array) is begin for i in foo'range loop foo(i) := i; end loop; end f; begin f(bar); end main; Ada arrays do not loose their bounds and indexing information when passed to functions or procedures. Furthermore, you can define your own array types and use those types in function and procedure parameters. The Ada syntax foo'range evaluates to the ordered range of index values for array foo. The for loop simply iterates through that ordered range of values. The range of values is taken from the array itself. If I were to make a small change in the for loop as follows: for i in 0..foo'last loop foo(i) := i; end loop; The compiler would identify this as an error. The type small_array was defined with a lowest index value of 1, not 0. 0 is not even a valid value for the small_index type. Many compilers will identify both errors. Jim Rogers