<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<div class="moz-cite-prefix">On 16/03/2022 12:56, David Ward wrote:<br>
</div>
<blockquote type="cite"
cite="mid:LO2P123MB468364C404E4E48A05EF5A60C0119@LO2P123MB4683.GBRP123.PROD.OUTLOOK.COM">
<p class="MsoNormal"><span
style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US">Specifically<o:p></o:p></span></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph"
style="color:black;margin-left:-18.0pt;mso-list:l0 level1
lfo1">
<span
style="font-size:10.0pt;font-family:"Arial",sans-serif;mso-fareast-language:EN-US">“System”
is there because some guidelines can’t be checked at the
software unit (or equivalent) level alone e.g. the one about
recursions<o:p></o:p></span></li>
<li class="MsoListParagraph"
style="color:black;margin-left:-18.0pt;mso-list:l0 level1
lfo1">
<span
style="font-size:10.0pt;font-family:"Arial",sans-serif;mso-fareast-language:EN-US">“Undecidable”
is there because compliance to some guidelines cannot be
demonstrated through static analysis alone and other methods
are needed.</span></li>
</ul>
</blockquote>
<p>I've applied a more pragmatic interpretation of those terms in
the context of MISRA.</p>
<p>To me...</p>
<p>"System" means "this rule can't be checked on a
single-translation unit, so it requires whole program analysis,
which will be slow, and you'll only get really reliable results
when you've finished the program, which is a bit late..."</p>
<p>"Undecideable" means "This rule is tough to check, so there will
some mixture of false negatives and false positives. Exactly what
you get depends on the whim of your chosen tool vendor..."</p>
<p>I also can't help noticing that all the _really_ important rules
in MISRA are "System" and "Undecideable" - for example rules 1.3,
9.1, 13.2, 17.5 and 17.8 from MISRA 2012. Admitting false
negatives for 1.3 ("don't have undefined behaviour") is
particularly nasty, since any missed UB effectively undermines
everything else.</p>
<p>SPARK and Rust both take a very different approach.</p>
<p> - Rod</p>
<p><br>
</p>
</body>
</html>