Certified C compilers for safety-critical embedded systems - Page 5

Do you have a question? Post it now! No Registration Necessary

Translate This Thread From English to

Threaded View
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Close. Ada requires the function return type to match the array index type.
Ada type matching is much more rigorous than C type matching.

Examples:

type my_index is range 1..10;
type beauty_scale is range 1..10;

type my_nums is array(my_index) of integer;

foo : my_nums;

function rand_index return my_index;
function rand_beauty return beauty_scale;


I have defined two distinct integer types above. The type my_index
is not synonymous with the type beauty_scale. Ada provides NO implicit
conversion between the two types. This is what Ada strong typing gives
us, a strong separation of data types.

It is valid to make the following call:

foo(rand_index) := 32;

This is valid because the function rand_index always returns a value
of type my_index, which is also the index type for the foo variable.

It is invalid to make the following call:

foo(rand_beauty) := 32;

This is invalid because the function beauty_index always returns
a value of beauty_scale, while the index type for the foo variable is
my_index.

This error is detected by the compiler.

I am sure you have already noticed that the range of values for both
types are identical. For Ada this structural equivalence is meaningless.
Different types are simply not implicitly converted. The Ada type model
is based upon the type name, not the type structure.

Jim Rogers

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

No. He is saying that Ada types and subtypes typically contain
information about expected values that will be checked at compile time
or run time as appropriate.

If the subtypes "statically match", which does not mean that the bounds
are static, it can be determined at compile time that no run-time check
will be necessary.  And of course, that means you don't have to worry
about what happens if the check fails.  In fact, years ago in Ada 83, I
had a nice tool that detected every place that a run-time bound was
tested by the compiler.  About one-third of the cases were cases where
rearranging the code would allow the compiler to eliminate the check,
one-third were really needed, and the rest were bugs.  Today I use the
SPARK analyzer or other (ASIS) tools to do essentially the same checking.

You are not required to use subtypes which are correctly bounded in Ada.
But it is a big help to (static) debugging and program correctness if
you do.  And in another thread on comp.lang.ada we are discussing that
it is a VERY useful property of Ada, not just because it makes it more
likely that the program will correctly implement the requirements.  It
also often results in missed requirements being detected.

I have lost track of the number of times when a "simple question" about
the right way to declare a subtype or assign a default value in Ada, has
gone back to the design team to write a new requirement, as soon as they
figured out what it should be.

My favorite example of this came from a project which was doing a flight
control system for a fighter aircraft.  They wanted to know if it was
possible to implement the system as a round-robin scheduler in Ada.  I
sent back a template of what the final code would look like, and a set
of questions that needed to be answered before the code could be
written--or the question answered.  A month or so later I called back
and asked whether that had solved their problem.  The answer was that
they had resolved fifteen of the seventeen questions I had asked and
they only had two left!

Eventually, they used hard-deadline scheduling because that way they
could resolve the remaining questions.  Notice that the questions in one
sense had nothing to do with Ada.  Ada had made the need for answers
obvious, but the questions could be stated in terms that were actually
independent of programming language and hardware.

"If the tracking of incoming missles exceeds its time slot should it be
aborted or allowed to delay the navigation function?"

"If the aircraft state update takes longer than expected--read time-outs
on status inquiries due to damage--should it restart where it left off
in the next time-slot, continue execution at low-priority, or reset to
the beginning for the next time slot but skip the failed check?"

These are not easy questions, and there may be no "right" answer in the
sense of one that will always save the aircraft.  But choosing the best
answer may save some aircraft that would otherwise be lost.

--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
:
:> So are you basically saying that Ada requires the function return type to be
:> bounded and can simply check this against the array bound?
:
: No. He is saying that Ada types and subtypes typically contain
: information about expected values that will be checked at compile time
: or run time as appropriate.

I'll try one of Robert's ideas.
Say I do not ignore the compiler's warning that the function used
for array indexing will return values out of range for the array. I
might see that the choice of two subtypes has been inappropriate
and should be replaced with two different types. They will have
overlapping ranges but will allow the same representation in
bits. However, the program cannot be compiled any longer, using
the same buffer:

procedure p is

   type Red_Index is range 90 .. 105;
   type Light_Red_Index is range 100 .. 120;

   buffer: array(Red_Index) of Boolean;

   function some_val return Light_Red_Index is separate;

begin
   if buffer(some_val) then
      null;  -- do something here, in a more real program
   end if;
end p;

    11.    if buffer(some_val) then
                     |
        >>> expected type "Red_Index" defined at line 3
        >>> found type "Light_Red_Index" defined at line 4

That is, I might presume that color Red is not too different from
Light_Red. I might know that the number of bits used for values
in the two types will be the same (char in C terms, say).  Still the
compiler will not let me use Light_Red_Index's value 101 and
Red_Index's value 101 interchangeably.

The range check goes away when both the function and the array
use the same index type (the function is implemented to return
random values from the index type's range (because the generator
has been instantiated with that type.))  The assembly listing shows
8bit register use on i686 when the index range permits, even with
numbers ranging beyond 255 (or > 65535 for that matter).

   type Light_Red_Index is range 92_000 .. 92_200;
   for Light_Red_Index'Size use 8;

In short, convenient, checked at compile time, and efficient :-)

-- Georg

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Well, it would be better to say that the compiler won't let you mix
Light_Red_Index and Red_Index implicitly.  You can always say:

if buffer(Red_Index(some_val)) then...

If the two types are represented the same, then there will be no real
run-time cost for the conversion.  (If both Red_Index and
Light_Red_Index were SUBtypes of Integer, then you could write:

if buffer(some_val) then... and there would be a range check associated
with the indexing operation.  With Red_Index and Light_Red_Index as
separate types, there will be a range check now associated with the
conversion instead of the subscripting.  But assuming that the
representations of the types are identical, the code should be identical.

Quoted text here. Click to load it

Yep, and if you do a type conversion as above, the compiler will add the
bias back in (or add the net difference if there are two different
biases).  This means you can write your code in meaningful units and
allow the compiler to remember and generate any conversions.  This is
real handy when you have a sensor that for example, returns a 12-bit
encoding of an angle.  You can write the code using units of degrees (or
radians or grads if you want) and the compiler will convert your
constants at compile time.  Get a new sensor with a 16-bit ADC, and all
you have to change is the type declaration (and of course, recompile and
test).

--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
: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

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Ah, so Ada is no better than C in that respect?

Ian


Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

No, Ada is much better than C in that respect.  The concept that Ada
supports but C doesn't is best expressed described by example:

function Identity(N: Positive) return Matrix is
   Result: Matrix(1..N, 1..N) := (others => (others => 0.0));
begin
   for I in Matrix(1)'Range loop
     Result(I,I) := 1.0;
   end loop;
   return Result;
end Identity;

The size of the matrix returned will often be determined at run-time,
but both the compiler and any static checking tools can verify that
there are no potential out-of-range assignments here. This sort of
"statically matching" constraints, where the constraints are dynamic but
can be statically determined to be identical is formalized in RM 4.9.1.
  There are certain cases in Ada where statically matching subtypes are
required, but in general Ada programmers tend to use statically matching
subtypes even where they are not required.  It not only makes for more
efficient code, since the compiler can remove constraint checks, but it
means that if the code is changed elsewhere, the change does not need to
be propagated.  This makes code maintenance much easier.

--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
:> Wouldn't that become a famous compiler that finds out, at compile
:> time, which value a certain variable is going to have? :-)
:>
:
: Ah, so Ada is no better than C in that respect?

In the dynamic Matrix example by R. Eachus a number of dynamic things
can indeed be statically studied, it seems. This implies there is a
measure for how much can be "found out" at compile time, given the
features of language X.  (In the above sentence I was only trying to
say that there is _no_ real world compiler that can possibly solve
the general problem of finding variables' values at runtime, for some
program in any programming language, given some input :-) But that is
not relevant here I think.)

Splint is an indicator too.  Considering maxSet/maxRead (array bounds, at
least some), require/ensure (Eiffel contracts), modifies (in, out, in out
parameter modes), etc., I suddenly feel very much at home in the language
that tries to look like C, though not quite.
Splint programs can only be translated by a compiler using the trick
of hiding the new language in C comments. I guess that the additional
information in the comments is then not available to the C compiler,
so the C compiler can only profit from users who try to redesign
their software, but it cannot itself profit from the comments...

Will there be profit if a true Splint compiler will evaluate
the additional information in the comments? Would the language
look like, well, not C, semantically? :-)


-- Georg

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it
ctiticism.
compiler
index


Again, tools like this do exist. One can argue over how well they work but
they do exist.
Tools like Polyspace Verifier can at times tell you statically that you have
a problem in your code.

For example the following psuedo code fragment would likely be flagged as a
potential error by polyspace

A, b : float;
C : integer;
D : array(1 .. 10) of float;

begin
 A := random_float;
 B := cos(a);
 C := integer(C * 9.0) + 1;
  D(C) := 0;
end;


while code like


A, b : float;
C : integer;
D : array(1 .. 10) of float;

begin
 A := random_float;
 B := cos(a);
 C := integer(C * 9.0) + 1;
  if C >= D'first and C <= D'last then
    D(C) := 0;
  end if;
end;


Would not generate an error during static analysis. (at least not for the
obvious error I intended to introduce in the first case ... :)

These tools exist now and have existed for some years.




Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it
ctiticism.
index

The Ada programmer usually uses the range attribute of the array variable
for these cases.

declare
    type My_Integer_Array is array (Positive range <>) of Integer;
    -- Type of array with bounds that are of type Positive (Positive
Integers)

    function Compute_Array return My_Integer_Array is
        -- returns an array of variable size
    ...
    end Compute_Array;

    My_Array : My_Integer_Array := Compute_Array;

    Sum      : Integer := 0;
begin
    -- Summation of add via array iteration
    For I in My_Array'Range loop
        Sum := Sum + My_Array(I);
    end loop;
end;

If you used a literal range in this case, you would trigger a runtime
constraint_error exception (index check failed) if your literal range is not
contained with the array's range.

However, there are other ways that an array range can be computed.

with Ada.Integer_Text_IO;
use  Ada.Integer_Text_IO;

procedure DynamicType is

   LowerBound : Integer;
   UpperBound : Integer;

begin

   Get(LowerBound);
   Get(UpperBound);

   declare

      type New_Bounds is range LowerBound..UpperBound;

      My_Array : array(New_Bounds) of Integer := (others => 1);

      Sum      : Integer := 0;

   begin

      for I in 1..10 loop  -- This will not compile because the compiler
                           -- cannot safety compute the correct type for the
                           -- literal range.
         Sum := My_Array(I);
      end loop;

      Put(Sum);
   end;
end DynamicType;

In practice most Ada programmers don't use literals because array's have
attributes such as 'range, 'first, and 'last, which offer a better
alternative to literals or even constants.



Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

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.

Quoted text here. Click to load it

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.



Re: Certified C compilers for safety-critical embedded systems

[...]

Quoted text here. Click to load it

I guess that PC-Lint _will_ detect this even if you use a pointer to
an array or a upper limit as parameter etc., I already have seen
PC-Lint warnings about possible out of bounds access in similar cases.
If there is any doubt, I can verify it if I'm in the office again.

Quoted text here. Click to load it

Lint can check the whole application, not only single modules.

Oliver
--
Oliver Betz, Muenchen

Re: Certified C compilers for safety-critical embedded systems
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

[...]
Quoted text here. Click to load it

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

C:\Dave>lint-nt -u lloop.c
PC-lint for C/C++ (NT) Ver. 8.00n, Copyright Gimpel Software 1985-2003

--- Module:   lloop.c
                 _
       foo[i] = i;
lloop.c  10  Warning 662: Possible creation of out-of-bounds pointer
(90 beyond
    end of data) by operator '[' [Reference: file lloop.c: lines 8,
10]
lloop.c  8  Info 831: Reference cited in prior message
lloop.c  10  Info 831: Reference cited in prior message
                 _
       foo[i] = i;
lloop.c  10  Warning 661: Possible access of out-of-bounds pointer (90
beyond
    end of data) by operator '[' [Reference: file lloop.c: lines 8,
10]
lloop.c  8  Info 831: Reference cited in prior message
lloop.c  10  Info 831: Reference cited in prior message
_
}
lloop.c  12  Warning 550: Symbol 'foo' (line 4) not accessed
lloop.c  4  Info 830: Location cited in prior message

C:\Dave>
---end included file---

The "-u" option tells PC-lint to do a "unit" check, i.e., that the
referenced file is not a complete program, so it should suppress
errors like "Function f defined but not called."

Regards,

                               -=Dave
--
Change is inevitable, progress is not.

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

not exactly. it permits addressing one beyond the end, but not accessing
so
    int a[10], *after = &a[10];
is OK, but
    a[10]++
isn't

The rule lets you do bounds checks on pointers, even with empty ranges.


--
    mac the naf

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

And in C++, you must write
     int a[10], *after = a + 10
as &a[10] is illegal. C99 gave special dispensation to remove &*
(a[10] is rewritten as *(a+10) so &a[10] is &*(a+10) becoming (a+10))
but C++ did not, even on built-in types.


Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

But the compiler won't isue an exception when you actualy do. First C does
not have exception handling (Ada has) and then it just not allowed but
almost no compiler will stop you doing it Especialy when a function call is
in between declaration and use.

Quoted text here. Click to load it


With Regards


Martin

--
mailto:// snipped-for-privacy@users.sourceforge.net
http://www.ada.krischik.com


Re: Certified C compilers for safety-critical embedded systems
snipped-for-privacy@hotmail.com (Dave Hansen) wrote in

Quoted text here. Click to load it

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

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it


He is a LINT-user    :-|

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

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.

Re: 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.

Quoted text here. Click to load it

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

Quoted text here. Click to load it

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.

--
mailto:// snipped-for-privacy@users.sourceforge.net
http://www.ada.krischik.com



Site Timeline