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-26 21:29:44 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!wn14feed!worldnet.att.net!bgtnsc04-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> Message-ID: User-Agent: Xnews/5.04.25 Date: Sat, 27 Dec 2003 05:29:44 GMT NNTP-Posting-Host: 12.73.181.50 X-Complaints-To: abuse@worldnet.att.net X-Trace: bgtnsc04-news.ops.worldnet.att.net 1072502984 12.73.181.50 (Sat, 27 Dec 2003 05:29:44 GMT) NNTP-Posting-Date: Sat, 27 Dec 2003 05:29:44 GMT Organization: AT&T Worldnet Xref: archiver1.google.com comp.arch.embedded:6144 comp.lang.ada:3838 Date: 2003-12-27T05:29:44+00:00 List-Id: Robert A Duff wrote in news:wccekur4151.fsf@shell01.TheWorld.com: > Chris Hills writes: >> So it all has to be enforced by the compiler? > > No, it doesn't. I agree with you that (in principle) there's nothing > wrong with running 'lint' or whatever in addition to the compiler. > However, 'lint' (in the case of C) doesn't have enough information > to perform the checks that are routinely done by Ada compilers. Two simple examples are array bounds checking and scalar range checking. 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 using human inspection one might assume this is a problem one would never see. Unfortunately, the definition of the array may occur many dozens or even hundreds of lines of code away from the "for" loop. The definition and the "for" loop may even be located in different source files, making the likelihood of human identification very low. type my_index is range 0..9; type My_Array_Type is array(my_index) of integer; foo : My_Array_Type; for num in 0..99 loop foo(num) := num; end loop; All Ada compilers will correctly identify the error in the for loop. The type of "num" is not the same as the type of the index, because the range of values defined for "num" are not all within the range of values in my_index. This detection will happen properly no matter how far the definition is separated from the "for" loop. Another problem, at least in my uses of lint in the past, was the settings for lint. You can set lint sensitivity from very low to very high. The lowest settings for lint miss a number of errors, while the highest settings for lint often produce a number of false error indications. It is not always obvious which lint setting to use for the best level of error identification with a minimum of false error messages. Jim Rogers