Re: Certified C compilers for safety-critical embedded systems

[James Rogers <jimmaureenrogers@att.net>]

Robert A Duff <bobduff@shell01.TheWorld.com> wrote in 
news:wccekur4151.fsf@shell01.TheWorld.com:

> Chris Hills <chris@phaedsys.org> 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