[SystemSafety] Critical systems Linux

[Olwen Morgan]

On 23/11/2018 18:45, David Crocker wrote:
> On 23/11/2018 18:01, Olwen Morgan wrote:
<snip>
> The subset doesn't need to be draconian though, a subset of the 
> MISRA-C rules is more than adequate for this purpose. 

<snip>

Probably another area of civil disagreement :-)

It all depends on the tolerance of the verifier. If your verifier can 
cope with less-than-MISRA strictness and still produce accurate 
verification with acceptable run times, that's fine.

My principal motivation for advocating a draconian subset is the laxity 
of the C standard and the latitude it creates for incautious and 
uncontrollable optimisation and the consequent ill-effects in bare-metal 
environments.

What do you have by way of support for a claim that your subset does not 
have holes through which your verifier can fall?


Olwen