DO-178C Static Analysis Checks for C Avionics

This article outlines the essential static analysis checks mandated by DO-178C guidelines for avionics software implemented in the C programming language. DO-178C ("Software Considerations in Airborne Systems and Equipment Certification") relies on objective-based verification rather than prescribing specific tools. To satisfy these regulatory objectives for the C language—notorious for undefined behaviors and loose typing—development teams must employ static analysis to verify coding standards compliance, detect run-time errors, validate data and control flow, and ensure predictable resource consumption.

1. Coding Standards Compliance

DO-178C Table A-5, Objective 4 requires verification that the source code conforms to defined software code standards. Because raw C contains undefined and implementation-defined behaviors, certification demands strict adherence to safety-critical subsets such as MISRA C (Guidelines for the Use of the C Language in Critical Systems). Static analysis tools must enforce:

  • Prohibition of Non-Deterministic Constructs: Prevention of dynamic memory allocation (malloc, free) after initialization to avoid heap fragmentation and allocation failure.
  • Restricted Control Structures: Prevention of unstructured control flow, such as goto statements, multiple return points (depending on project standards), and recursion, which can cause unpredictable call-stack growth.
  • Safe Type Casting: Prohibition of dangerous implicit conversions, pointer-to-integer conversions, and invalid type punning that violate strict aliasing rules.

2. Control Flow Analysis

DO-178C Section 6.3.4 requires analysis of source code structure to ensure alignment with software architecture and low-level requirements. Static control flow analysis verifies:

  • Dead and Unreachable Code Detection: Identification of statements that can never be executed (dead code) or code that has no effect on outputs. DO-178C requires that dead code be removed, while deactivated code must be identified and traced.
  • Infinite Loop Analysis: Verification that all loops have deterministic, statically provable termination conditions.
  • Single Entry/Single Exit Properties: Ensuring subroutines follow strict structural entry and exit rules required for architectural determinism.

3. Data Flow Analysis

Data flow analysis tracks variable lifecycles across the execution paths to guarantee integrity:

  • Uninitialized Variables: Ensuring no variable or pointer is read before it is explicitly initialized.
  • Data Coupling Verification: Confirming that data shared between modules strictly follows architectural definitions, particularly when using global variables or shared memory.
  • Race Conditions and Concurrency Checks: Detecting unprotected shared resources across concurrent tasks or interrupt service routines (ISRs).

4. Run-Time Error and Undefined Behavior Prevention

Static analysis engines (especially those employing formal methods and abstract interpretation) must mathematically prove the absence of run-time crashes and undefined behaviors:

  • Array Bounds and Buffer Overflows: Verifying that array indices never exceed allocated boundaries.
  • Pointer Safety: Proving the absence of null-pointer dereferences, wild pointers, and dangling pointers.
  • Arithmetic Faults: Proving that execution paths are immune to division by zero, modulo by zero, and signed/unsigned integer overflows or underflows.

5. Worst-Case Stack and Resource Usage Analysis

Section 6.4.3 emphasizes source code verification against target hardware constraints:

  • Maximum Stack Depth: Statically computing the worst-case call-tree depth and stack memory usage to ensure stack overflow cannot occur during flight operations.
  • Recursion Elimination: Verifying that direct and indirect recursion are entirely absent, as non-deterministic call depths invalidate static stack guarantees.

6. Interface and Type Consistency

For modular C systems split across multiple compilation units, static analysis must ensure:

  • Prototype Verification: Matching function parameter types, return types, and parameter counts between declarations in header files and definitions across source files.
  • Scope and Linkage Enforcement: Restricting variable visibility via the static keyword where global visibility is not required by software architecture.