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.
- 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