Certified C compilers for safety-critical embedded systems

I wonder how you can speak about a programing languages if you can't even spell there names properly.

It's Modula-2. If you are to lazy to type additional four characters you should not be writing savety critical software.

Ada is the name if a woman and not the American Denitist Association and as such spelled capital "A", lower "d", lower "a" - "Ada".

With Regards

Martin.

It's "too" and "an" and "safety". If you are too lazy to use a spelling and grammar checker, you should not be writing comments criticizing other peoples' writing.

Certainly there is an excuse -- it is not enforced by the compiler.

That is quite different from the situation with Ada.

In article , Larry Kilgallen writes

So it all has to be enforced by the compiler?

The main difference between C and ADa is that the average ADA programmer is in a safety critical environment. The average C programmer is not.

If C program development was *normally* taught as though it was going to be used in a safety critical environment I think things would change.

/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\ \/\/\/\/\ Chris Hills Staffs England /\/\/\/\/\ /\/\/ snipped-for-privacy@phaedsys.org

:-)

Well said, Hyman.

It's true that Ada is correctly spelt "Ada", not "ADA" or "ADa", but come on. Why do we need to make a big deal about it? Ada has some advantages over C, but beating people up over the spelling isn't going to convince anybody of anything.

- Bob

P.S. for those interested in Ada trivia: In the December 22 issue of Newsweek, there's a photo of Tony Blair standing in front of a portrait of Ada. That's the Ada for whom the language was named. Page 32.

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.

The issue is not (primarily) which tool does the analysis (the compiler versus lint). The issue is how much information about the intent of the programmer is contained in the source code.

I think it's a mistake to assume that that "average" Ada programmer is doing safety critical work. Ada (and/or SPARK) are good in that environment, but Ada is also quite good for writing run-of-the-mill non-safety-critical programs, too. I don't know the statistics, so I can't say about "average", but the program I'm working on right now is not safety critical, or even real-time or embedded, but I get some productivity benefit from Ada's ability to allow me to express various (compile-time-checkable) constraints.

So I don't agree that the "main" difference between C and Ada is their environment.

(Boy, I guess the spelling police will really get after you for spelling "Ada" wrong twice in the same sentence -- "ADa" and "ADA". Sheesh. ;-))

Probably. But to learn Ada, you have to first learn to write "Hello, world", and then learn some more simple stuff, and so on. Same with C. Nobody learns to write real-time/embedded/high-integrity/safety-critical stuff on the first try.

- Bob

Whereas I think that so long as the infrastructure leaves certain things to be done "by hand" there will be skimping.

Consider all the regulation and oversight required for drug safety tests.

Several people have asserted the argument that the large number of users of a given tool implies quality in that tool.

I don't buy it. By this logic, MS Windows should be absolutely flawproof, and the infamous Pentium Divide bug should never have happened.

No amount of usage can make up for design flaws. Popularity is much less about technical qualities than it is about marketing. C, Windows, x86 chips have substantial market share, which is not the same as saying that they have substantial quality by design.

dave

That's interesting, and I should probably look up this paper (is it online?). After thinking about it a bit, however, this result is not too surprising. After all, it seems to me that "specification fault" is a rather general term. What does it mean? Is it perhaps a catch-all term for everything other than the software development process itself?

I work in an engineering environment. Engineers come up with ideas, which are then often translated into software. Sometimes the translation process (design/programming) is done directly by the engineer, but more often it is done by communicating the idea to a programmer or software engineer. Any defect in the idea itself or in its communication to the programmer falls under the category of "specification fault," it seems to me. Being an aerospace engineer myself, I like to think of myself as an important part of the process. If our portion of the errors was too small, I'd think that perhaps we engineers were not taking enough risks with our ideas. So I'm proud that we're at the 44% level. ;^)

What I am getting at, in a roundabout way, is that, as you probably realize, "specification faults" have nothing to do with the choice of programming language. That's an engineering problem. So it is as irrelevant to the choice of language as, say, drug abuse in the workplace, just to give an off-the wall example. Would you argue that the choice of programming language is of minimal importance if half of the critical errors were due to drugged programmers? Of course not. So why are you implying that language choice is unimportant because engineering is important?

Is that what we sometimes call "maintenance"? My impression is that Ada excels in this stage.

Of course it isn't. If the engineering isn't done right, the best programmers and software engineers in the world are unlikely to salvage the project.

Are you claiming that the Arianne 5 wouldn't have failed catastrophically if the same bug had occurred in C code? If so, that's definitely interesting. I'm certainly not knowledgable enough here to comment, but I'm sure others on this forum are.

You lost me there. As I explained above, I agree that the choice of language has little effect on the engineering. But the point is that the choice of language has a strong effect on the software design and development process. Isn't that what we're talking about here? If not, sorry, wrong number.

->savety critical software.

Robert A Duff wrote in news: snipped-for-privacy@shell01.TheWorld.com:

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

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)..

Perhaps even by the LDRA static analysis tools (Ada available) though I have less to go on for this tool.

"Jeff C," wrote in news:yA9Hb.488862$275.1387889@attbi_s53:

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

snip

I know nothing about ada so this is a genuine query rather than a ctiticism. The above example is fine as long as literals are used - even a C compiler could be devised to make this check - but what happens when the array index is computed?

Ian

Careful! All that the standard guarantees is that the address of the one element beyond the should compare in the expected fashion with the addresses of the other array elements. For example, if we have

int foo[10]; int* bar = foo + 10;

then the C standard will guarantee that

bar > foo + i

for any i in the range 0 .. 9 inclusive. Although the standard guarantees the behavior of a pointer one past the end of an array, it explicitly does NOT guarantee anything about accessing an element past the end of an array. An attempt to read or write *bar leads to unpredictable results.

It depends. I would imagine that some C compilers and lint might catch something like this:

int foo[10]; ... j = foo[10];

The real problem is that once an array is passed to a function, length information is lost. This is one area where the C++ vector template made a real advance. Of course, Ada had the approach to arrays all along, in that it never divorced the length from the array data.

In article , David Emery writes

We are in comp.arch.embedded...... Ms Desktop tools are not relevant. Besides AFAIK their license excludes any safety critical use.

Correct for the desktop tools but among *Embedded* tools it does especially where the aim is to go for the high reliability market.

/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\ \/\/\/\/\ Chris Hills Staffs England /\/\/\/\/\ /\/\/ snipped-for-privacy@phaedsys.org

You mean as in

type my_index is range 0 .. some_variable;

-- yes, Ada compilers will perform the check.

Actually the code wasn't actually compiled by whoever posted it, a crime on c.l.a: you either have to say

for Num in 0 .. 99 loop Foo (My_Index (Num)) := Num; end loop;

(which GNAT doesn't see as a problem until execution time) or

for Num in My_Index range 0 .. 99 loop Foo (Num) := Integer (Num); end loop;

to which GNAT says

constraints.adb:10:35: warning: static value out of range of type "My_Index" defined at line 3 constraints.adb:10:35: warning: "Constraint_Error" will be raised at run time

(this is the "99").

In comp.lang.ada Ian Bell wrote: :James Rogers> 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. :> [...] : : I know nothing about ada so this is a genuine query rather than a ctiticism. : The above example is fine as long as literals are used - even a C compiler : could be devised to make this check - but what happens when the array index : is computed?

Wouldn't that become a famous compiler that finds out, at compile time, which value a certain variable is going to have? :-)

If you want a hole in your foot, you can make one, though it might not be easy:

with Interfaces; with Ada.Integer_Text_IO; use Ada;

procedure t is -- read a positive value from standard input and create an -- array of that size, which is filled (hopping excessively)

procedure rubber_buffer(limit: Positive) is

subtype Index is Positive range 1 .. limit; -- a range constraint on Positive, determined at call time

buffer: array(Index) of Interfaces.Unsigned_8; -- storage for 1 .. limit 8bit quantities

begin -- demonstration of constraint_error

off_buffer: -- k grows too large for a buffer index

for k in Index'first .. 2 * Index'last loop buffer(k) := 42; -- index check failed, at run time end loop off_buffer;

off_index_range: -- k gets too large for Index subtype's range

for k in Index'first .. Index(2 * Index'last) -- range check failed, at run time loop buffer(k) := 42; end loop off_index_range;

end rubber_buffer;

n: Positive; -- upper limit of 1-based buffer, read at run time

begin Integer_Text_IO.get(n); rubber_buffer(n); end t;

That's why language-defined array constructs such as the 'range attribute are useful. You can write

for k in buffer'range loop buffer(k) := 42; end loop;

(or in this case more simply, using language defined `others'

buffer := (others => 42);)

no matter what the buffer's index range currently is.

-- Georg

That was not what I had in mind and seems to me to be rather dodgy code. i was thinking more of the return value of some function being used as an index to the array.

Ian