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.

Download PDF Download EPUB

Contents:

• Preface
• Enforcing Basic Program Consistency
  • Taming Text-Based Inclusion
  • Hardening Link-Time Checking
  • Going Towards Encapsulation
• Enforcing Basic Syntactic Guarantees
  • Distinguishing Code and Comments
  • Specially Handling Function Parameters and Result
    • Handling the Result of Function Calls
    • Handling Function Parameters
  • Ensuring Control Structures Are Not Abused
    • Preventing the Semicolon Mistake
    • Avoiding Complex Switch Statements
    • Avoiding Complex Loops
    • Avoiding the Dangling Else Issue
• Enforcing Strong Typing
  • Enforcing Strong Typing for Pointers
    • Pointers Are Not Addresses
    • Pointers Are Not References
    • Pointers Are Not Arrays
    • Pointers Should Be Typed
  • Enforcing Strong Typing for Scalars
    • Restricting Operations on Types
      • Arithmetic Operations on Arithmetic Types
      • Boolean Operations on Boolean
      • Bitwise Operations on Unsigned Integers
    • Restricting Explicit Conversions
    • Restricting Implicit Conversions
• Initializing Data Before Use
  • Detecting Reads of Uninitialized Data
  • Detecting Partial or Redundant Initialization of Arrays and Structures
• Controlling Side Effects
  • Preventing Undefined Behavior
  • Reducing Programmer Confusion
  • Side Effects and SPARK
• Detecting Undefined Behavior
  • Preventing Undefined Behavior in SPARK
  • Proof of Absence of Run-Time Errors in SPARK
• Detecting Unreachable Code and Dead Code
• Conclusion
• References
  • About MISRA C
  • About SPARK
  • About MISRA C and SPARK