Certified C compilers for safety-critical embedded systems

"singed" char? Perhaps there is a distinction between sung and unsung chars.

Reply to
Frank J. Lhota
Loading thread data ...

Yep. We are agreeing. I was going to use the tape drive example but you beat me to it.

Interesting...I had always suspected that this had to happen in practice, but I didn't actually know how professionals (at least a set of professionals;) reacted to these sorts of impasses. Thank you, I bet this bit of information will turn up useful to me sometime in the future.

-CRM

Reply to
Chad R. Meiners

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 naïf
Reply to
Alex Colvin

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.

Reply to
Hyman Rosen

Martin...

The link in my sig leads to another that'll take you directly to the ANSI on-line store where (for US$18) you can download it in PDF format. I keep mine on a business card sized CD-ROM with copies of Acrobat Reader and xpdf.

--
Morris Dovey
West Des Moines, Iowa USA
C links at http://www.iedu.com/c
Read my lips: The apple doesn't fall far from the tree.
Reply to
Morris Dovey

snipped-for-privacy@hotmail.com (Dave Hansen) wrote in news: snipped-for-privacy@News.CIS.DFN.DE:

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

Reply to
James Rogers

I seriously doubt that Pentium volume exceeds PIC volume. A lot of this discussion depends on how you describe a component. A car is a component of a fleet, while a wheel is a component of a car, etc. You can never measure reliability, only calculate probabilities. In some cases you derive these from components, in others you use experimental sampling, in still others you rely on educated guesswork.

--
Chuck F (cbfalconer@yahoo.com) (cbfalconer@worldnet.att.net)
   Available for consulting/temporary embedded and systems.
     USE worldnet address!
Reply to
CBFalconer

Thanks.

--
mailto://krischik@users.sourceforge.net
http://www.ada.krischik.com
Reply to
Martin Krischik

Grin.

Well in C you can have signed char where char'Pos is range -128 .. +127 and unsigned char where char'Pos ist 0 .. 255. One of the top 10 mistakes K&R did. It leads to a lot of misunderstandings and signed char is only used when Short_Short_Integer is needed.

Which is yet another example where in C you have to say "A" when realy you want "B". How a static analysis tool will deal with this I never know.

With Regards

Martin

--
mailto://krischik@users.sourceforge.net
http://www.ada.krischik.com
Reply to
Martin Krischik

Grin. But most C programmers are to lazy for to type unsigned.

That is why Ada 'Size gives you the size in bits. No misunderstanding here.

You allwas learn something new. But unint_least8_t is not helpfull for safety-critical embedded systems. You might need exaclty 8 bit.

Which brings me back to the original Question. How will you do this in C:

type Month is new Integer range 1 .. 12; for Month'Size is 8;

Or even better:

type Display_Element is Interger range 0 .. 9; for Display_Element'Size use 4;

type Display_Array is array (Integer range 1 .. 6) of Display_Element; pragma Pack (Display_Array);

Display : Display_Array; for Display'Address use 16#12_3456#;

We are talking "safety-critical embedded systems". The Plane might crash if

11 is ever stored in a Display_Element.

With Regards

Martin.

--
mailto://krischik@users.sourceforge.net
http://www.ada.krischik.com
Reply to
Martin Krischik

It doesn't AFAIK the last sets of figures I saw (broadly similar from more than one silicon vendor) the x86 class only make up around 5% of the MUC/MCP's produced. Around 25% are 8051 types.

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

formatting link
\/\/ \/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/

Reply to
Chris Hills

Do you have a reference? Many years ago I read an article about microcontrollers being responsible by 95% of the market despite all the hype created around either Intel or AMD release of a new top microprocessor. I think the figure was related to market share ($$$), not units shipped. The former makes more sense to me as nowadays there are microcontrollers (from 4 to 32 bitters) in nearly every electricity powered stuff you may think of. If I am right, then the figures for units shipped are even more impressive due to cost per unit.

Regards.

Elder.

Reply to
Elder Costa

[...re: plain, signed, and unsigned char...]

In C, CHAR_BIT gives you the number of bits in [[un]signed] char. It must be >= 8.

If a platform supports uint8_t (unsigned integer exactly 8 bits wide) the compiler must provide the type. If the platform does not support the type, you have to choose another platform.

You could do something like

typedef struct month{ value:8; } Month;

typedef struct display_element{ value:4; } Display_Element;

typedef struct display_array{ elt0: 4; elt1: 4; elt2: 4; elt3: 4; elt4: 4; elt5: 4; } Display_Array;

Display_Array *Display = (Display_Array *) 0x123456;

Though in no case would the ranges be enforced. Heck, enumerations aren't enforced in any way either:

enum { Red, Green, Blue } color; int number;

color = 42; number = Red;

Is perfectly fine as far as the compiler is concerned.

Then don't do that. ;-)

Regards,

-=Dave

--
Change is inevitable, progress is not.
Reply to
Dave Hansen

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.

With Regards

Martin

--
mailto://krischik@users.sourceforge.net
http://www.ada.krischik.com
Reply to
Martin Krischik

I had my array start at 1 not 0. In C all numbers start with 0 but in the real world they usualy start with 1.

Display_Array *const Display = (Display_Array *) 0x123456;

But is it not much better if the compiler stoped you from doing that mistake?

Anyway, all above is is just plain C and it is not at all as save as the Ada code. Nor is it as easy to read (safety-critical software in my book should be code reviewed). And this is just

The claim here in the group is that by use of a static analysis tool the C code can be made as secure as the Ada code. So let me expand my question: How with the static analysis tool find out the the follwing might lead to the plane crashing.

Ada:

Display (1) = 11; -- Compiler will warn you compile time Display (2) = Value + 2; -- exeption if Value is greater 7

C:

Display->elt0 = 11; Display->elt1 = Value + 2;

This example might be over primitive but humans somtimes make this little mistakes.

With Regards

Martin

--
mailto://krischik@users.sourceforge.net
http://www.ada.krischik.com
Reply to
Martin Krischik

The "real world" doesn't have arrays. Only computer programs do.

Reply to
Hyman Rosen

In article , Martin Krischik writes

Interesting point. Apparently 0 is the first positive integer. Everything starts at 0. Otherwise things would start with 1 or -1 there would be nothing (not 0) between them :-)

Zero is a valid number.

runs for cover and turns off email system :-) /\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\ \/\/\/\/\ Chris Hills Staffs England /\/\/\/\/\ /\/\/ snipped-for-privacy@phaedsys.org

formatting link
\/\/ \/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/

Reply to
Chris Hills

In article , Chad R. Meiners writes

No. I was thinking about Lint initially but I am sure that some of the better (more expensive :-) tools will test to various criteria etc and AFAIK do what you are suggesting but I am not certain on this. any one using QAC or LDRA's tool like to comment?

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

formatting link
\/\/ \/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/

Reply to
Chris Hills

In article , Russ writes

Yes if you are an IEE member with access to the library

Yes.

Judging by some of the code I have seen the two may not be unrelated :-)

I was arguing that the larger problem is the engineering process rather than which language. However (catch 22 time again) if you have a good engineering process you are less likely to make errors and be more meticulous because the sort of people that would set up and ruin a good engineering process will by definition try and "do things right"

So a good team with a good system will do a good program irrespective of if it is C or Ada... Ie if C they would use a C subset, static analysis coding standards, code reviews, full test plans etc...

If Ada they would use SPARK

However a bad team using a poor engineering system is likely not to worry too much about the rest of it. SO in that case the enforced parts of Spark Ada probabluy would be an advantage over C

That was a generalisation!!!! I know everyone can pull up their own exception!

The Arriane 5 rocket show the problem. Ada but from what I understand the corners were cut on the testing due to management pressure to do with launch windows.... Good language. "adjustments" to the system the rocket failed.

Maintenance is that which is done by other people after we have all finished the design and implementation and moved on to the next excepting project.

Ditto testing :-)

Ditto documentation :-)

But will get blamed for it :-(

Definitely. C is not strongly typed. You can chuck a long into a char and nothing will complain. So IN THIS PARTICULAR CASE an error would not have been raised and the rocket continued..... However in the 99 similar cases you would have wanted it to flag an error and it would not have done so :-)

There are many who point out that had it been written in C it would not have lifted off anyway due to other errors that would inevtiabley been in the system.(and the crash would not have occurred ergo C is safe :-)

I was making the point that a language, no matter how theoretically good is only as good as the implementation of the tools to support it. Ada has less of a problem as compilers can be validated and certified. Not something that happens with C.

I would agree that the choice of language does have an effect on the sw and development process. Ada AFAIk is usually taught and used in a strong safety critical and Enginering way. C is often badly taught and certainly not (usually) with any sort of Engineering or safety critical ethos. In fact often due to it's history quick and dirty and hacking seem more related :-(

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

formatting link
\/\/ \/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/

Reply to
Chris Hills

In article , Elder Costa writes

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

formatting link
\/\/ \/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/\/

Reply to
Chris Hills

ElectronDepot website is not affiliated with any of the manufacturers or service providers discussed here. All logos and trade names are the property of their respective owners.