Re: Certified C compilers for safety-critical embedded systems

[James Rogers <jimmaureenrogers@att.net>]

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
> <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;
>     }
> }
> 

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