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, LOTS_OF_MONEY 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 23:50:56 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!wn11feed!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> Message-ID: User-Agent: Xnews/5.04.25 Date: Sat, 27 Dec 2003 07:50:56 GMT NNTP-Posting-Host: 12.73.184.169 X-Complaints-To: abuse@worldnet.att.net X-Trace: bgtnsc05-news.ops.worldnet.att.net 1072511456 12.73.184.169 (Sat, 27 Dec 2003 07:50:56 GMT) NNTP-Posting-Date: Sat, 27 Dec 2003 07:50:56 GMT Organization: AT&T Worldnet Xref: archiver1.google.com comp.arch.embedded:6147 comp.lang.ada:3841 Date: 2003-12-27T07:50:56+00:00 List-Id: "Jeff C," wrote in news:yA9Hb.488862$275.1387889@attbi_s53: > While most C compilers and lint won't find this, there are static > analysis tools that can. Granted the > tools may be able to do a better job on Ada code because there is more > information to work with but > simple cases like you presented here (even if the loop was "far away:" > from foo) can be detected > by tools like Programming Research QA C (No Ada Available) and > Polyspace (Ada available).. Of course, static analysis for any language has its limitations. For example, what tool exists for C that will reliably identify the following problem: int foo[10]; int total(int *a) { int i; int sum = 0; for(i = 0; i < 100; ++i) { sum += a[i]; } return sum; } Of course, the common C idiom is to pass a limit value along with the array reference. int total(int *a, int limit) { int i; int sum = 0; for(i = 0; i < limit; +=i) { sum += a[i]; } return sum; } The problem is that there is no explicit relationship between the value passed to the formal parameter "limit" and the number of elements in the array. It is up to the programmer to ensure correctness in this detail. Ada, on the other hand, provides a completely safe syntax to deal with such problems. type my_index is range 0..9; type my_array is array(my_index range <>) of integer; function total(a : my_array) return integer is sum : integer := 0; begin for i in a'range loop sum := sum + a(i); end loop; return sum; end total; The Ada run-time will produce a correct iteration through the array passed to total every time. The compiler will detect any attempt to pass an parameter that is not of the type my_array. This is clearly not a case that can be fully handled using static analysis. Nevertheless, it must be handled correctly for all valid cases. In Ada it can be proven that the iterations will always be correct. In C there is no such proof possible. You must rely upon the skills and attention of the programmer. When reliability engineers encounter a system relying upon human actions the commonly accepted error rate, assuming properly trained humans, is 1 in 1000. Such an error rate is unacceptably low for most safety critical systems. An error rate of 1 in 1000 is a reliability rate of 0.999. Safety critical systems commonly require reliability rates on the order of 0.999999. This is three orders of magnitude higher than can be achieved through reliance on human correctness. Jim Rogers