SPARK Ada for the MISRA C Developer
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.
This document was prepared by Yannick Moy, with contributions and review from Ben Brosgol.
The code examples in this course use an 80-column limit, which is a typical limit for Ada code. Note that, on devices with a small screen size, some code examples might be difficult to read.
- Enforcing Basic Program Consistency
- Enforcing Basic Syntactic Guarantees
- Distinguishing Code and Comments
- Specially Handling Function Parameters and Result
- Ensuring Control Structures Are Not Abused
- Enforcing Strong Typing
- Enforcing Strong Typing for Pointers
- Enforcing Strong Typing for Scalars
- Initializing Data Before Use
- Controlling Side Effects
- Detecting Undefined Behavior
- Detecting Unreachable Code and Dead Code