SPARK Ada for the MISRA C Developer

Yannick Moy

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. 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 software. 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 to enforce, as it is impossible to enforce the 16 directives and 143 rules (collectively referred to as guidelines) of MISRA C. In particular, 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.

However, static analysis technology is available that can achieve soundness without inundating users with false alarms. One example is the SPARK toolset developed by AdaCore, Altran and Inria, which is based on four principles:

• The base language Ada provides a solid foundation for static analysis through a well-defined language standard, strong typing and rich specification features.

• The SPARK subset of Ada restricts the base language in essential ways to support static analysis, by controlling sources of ambiguity such as side-effects and aliasing.

• The static analysis tools work mostly at the granularity of an individual function, making the analysis more precise and minimizing the possibility of false alarms.

• The static analysis tools are interactive, allowing users to guide the analysis if necessary or desired.

This book presents the SPARK technology – the SPARK subset of Ada and its supporting static analysis tools – through an example-driven comparison with the rules in the widely known MISRA C subset of the C language.

An on-line and interactive version of this document is available at AdaCore's learn.adacore.com site.

By Yannick Moy
Release 1.0, Feb 12, 2019