SPARK Annotation Metrics

Analyze SPARK Ada codebases and quantify how much of the source is devoted to verification annotations. The motivation for writing this tool was to compare the "annotation" density of verified SPARK programs with that of other formal verification languages, like Frama-C.

What it does

• Recursively walks one or more directories, picking up every .ads and .adb file.
• Parses each compilation unit with Libadalang, skipping files that contain syntax errors.
• Counts both the number of occurrences and the number of occupied lines for the SPARK verification aspects and pragmas described in the SPARK 2014 LRM.
• Computes the ratio of annotation lines to total source lines of code (SLOC) so you can gauge annotation density.

Requirements

• Alire package manager (installs Libadalang and its dependencies automatically).
• A GNAT toolchain supported by Alire (e.g., gnat_native).

Alternatively, you can build it withot Alire if you remove the Alire-generated with "config/spark_annotation_metrics_config.gpr"; in spark_annotation_metrics.gpr and add the Libadalang project file from your installation. You'll also need a GNAT toolchain, from your Linux distribution, for example.

Build

alr build

The resulting executable is placed under bin/.

Run

bin/spark_annotation_metrics <directory> [<directory> ...]

• You must supply at least one directory. Each directory is traversed recursively.
• Non-Ada files are ignored; files that fail to parse are reported and skipped.

Sample output

This is the output for my coap_spark project, including code generated by RecordFlux.

$ spark_annotation_metrics src client/src server/src generated
SPARK Verification Annotation Report
------------------------------------
- Total SLOC:  18434
- PRE_COND: 588 (lines: 1739)
- POST_COND: 381 (lines: 2146)
- REFINED_POST: 0 (lines: 0)
- CONTRACT_CASES: 1 (lines: 4)
- GLOBAL_ASPECT: 23 (lines: 27)
- REFINED_GLOBAL_ASPECT: 0 (lines: 0)
- DEPENDS_ASPECT: 29 (lines: 29)
- REFINED_DEPENDS_ASPECT: 0 (lines: 0)
- INITIALIZES_ASPECT: 2 (lines: 2)
- INITIAL_CONDITION_ASPECT: 0 (lines: 0)
- DEFAULT_INIT_COND: 9 (lines: 62)
- ABSTRACT_STATE_ASPECT: 2 (lines: 2)
- REFINED_STATE_ASPECT: 1 (lines: 1)
- PART_OF_ASPECT: 0 (lines: 0)
- EXTERNAL_ASPECT: 0 (lines: 0)
- TYPE_INVARIANT_ASPECT: 0 (lines: 0)
- PACKAGE_INVARIANT: 0 (lines: 0)
- PREDICATE_ASPECT: 0 (lines: 0)
- DYNAMIC_PREDICATE_ASPECT: 18 (lines: 51)
- GHOST_CODE: 52 (lines: 52)
- LOOP_INVARIANT: 53 (lines: 102)
- LOOP_VARIANT: 1 (lines: 1)
- PRAGMA_ASSERT: 317 (lines: 323)
- PRAGMA_ASSUME: 0 (lines: 0)
- PRAGMA_ANNOTATE: 0 (lines: 0)
- PRAGMA_ALWAYS_TERMINATES: 28 (lines: 28)
- PRAGMA_ASYNC_READERS: 0 (lines: 0)
- PRAGMA_ASYNC_WRITERS: 0 (lines: 0)
- PRAGMA_CONSTANT_AFTER_ELABORATION: 0 (lines: 0)
- PRAGMA_EFFECTIVE_READS: 0 (lines: 0)
- PRAGMA_EFFECTIVE_WRITES: 0 (lines: 0)
- PRAGMA_EXCEPTIONAL_CASES: 0 (lines: 0)
- PRAGMA_EXTENSIONS_VISIBLE: 0 (lines: 0)
- PRAGMA_NO_CACHING: 0 (lines: 0)
- PRAGMA_SIDE_EFFECTS: 2 (lines: 2)
- PRAGMA_SPARK_MODE: 110 (lines: 110)
- PRAGMA_VOLATILE_FUNCTION: 0 (lines: 0)
- Total verification annotations:  1617
- Total verification annotation lines:  4681
- Annotation-lines/SLOC ratio:  0.25

Numbers will differ for your project, but the structure remains the same:

• Each counter reports both occurrences and line spans.
• The totals consolidate everything, and the ratio uses line counts only, making it a reliable indicator of verification density.

AI Assistance

This program was written with the assistance of GPT-5.1-Codex. All the changes done by the agent has been manually reviewed and improved.