Re: "Ravenscar-like" profile for C/C++

[Michiel.Salters@logicacmg.com (Michiel Salters)]

Martin Krischik <krischik@users.sourceforge.net> wrote in message news:<1082964421.KuB1viW3U1@linux1.krischik.com>...
> Ioannis Vranos wrote:
>
> The problem with savety critical programming in C or C++ is not what is
> allowed or possible but what should not be allowed and should be
> impossible. And for that I just need two line:
> 
> char X[10];
> X[10]='A';

What's the problem with that code, from a safety perspective? Certainly
a C compiler which is supposed to be suited for safety-critical programs
will diagnose this. The base C and C++ languages have quite a number
of "undefined behavior - no diagnostic required" cases, but a similar
profile may very well tighten that to "undefined behavior - must be 
rejected at compile time". 

The base philosophy in C and C++ is that flexibility can be traded 
for safety, but not vice versa. Certainly, in C++ it is easy to
create a verifiable subset. For instance, it is possible to define
a range template and with it a <int,0,10> type. The toolset would
be hard pressed to prove that the range template is correct and
overflow-free. However, this could be proven by humans. The tool
chain instead only has to check that all possible overflows are
located in this checked range< > code. Together, this would prove
that a body of code is overflow-free.

Regards,
Michiel Salters