Introduction To SPARK

MISRA C appeared in 1998 as a coding standard for C; it focused on avoiding error-prone programming features of the C programming language rather than on enforcing a particular programming style. A study of coding standards for C by Les Hatton found that, compared to ten typical coding standards for C, MISRA C was the only one to focus exclusively on error avoidance rather than style enforcement, and by a very large margin.

The popularity of the C programming language, as well as its many traps and pitfalls, have led to the huge success of MISRA C in domains where C is used for high-integrity sofware. This success has driven tool vendors to propose many competing implementations of MISRA C checkers. Tools compete in particular on the coverage of MISRA C guidelines that they help enforce, as it is impossible to enforce the 16 directives and 143 rules (collectively referred to as guidelines) of MISRA C.

The 16 directives are broad guidelines, and it is not possible to define compliance in a unique and automated way. For example, “all code should be traceable to documented requirements” (Directive 3.1). Thus no tool is expected to enforce directives, as the MISRA C:2012 states in introduction to the guidelines: “different tools may place widely different interpretations on what constitutes a non-compliance.”

The 143 rules on the contrary are completely and precisely defined, and “static analysis tools should be capable of checking compliance with rules”. But the same sentence continues with “subject to the limitations described in Section 6.5”, which addresses “decidability of rules”. It turns out that 27 rules out of 143 are not decidable, so no tool can always detect all violations of these rules without at the same time reporting “false alarms” on code that does not constitute a violation.

An example of an undecidable rule is rule 1.3: “There shall be no occurrence of undefined or critical unspecified behaviour.” Appendix H of MISRA:C 2012 lists hundreds of cases of undefined and critical unspecified behavior in the C programming language standard, a majority of which are not individually decidable. For the most part, MISRA C checkers ignore undecidable rules such as rule 1.3 and instead focus on the 116 rules for which detection of violations can be automated. It is telling in that respect that the MISRA C:2012 document and its accompanying set of examples (which can be downloaded from the MISRA website) does not provide any example for rule 1.3.

However, violations of undecidable rules such as rule 1.3 are known to have dramatic impact on software quality. Violations of rule 1.3 in particular are commonly amplified by compilers using the permission in the C standard to optimize aggressively without looking at the consequences for programs with undefined or critical unspecified behavior. It would be valid to ignore these rules if violations did not occur in practice, but on the contrary even experienced programmers write C code with undefined or critical unspecified behavior. An example comes from the MISRA C Committee itself in its “Appendix I: Example deviation record” of the MISRA C:2012 document, repeated in “Appendix A: Example deviation record” of the MISRA C: Compliance 2016 document, where the following code is proposed as a deviation of rule 10.6 “The value of a composite expression shall not be assigned to an object with wider essential type”:

uint32_t prod = qty * time_step;