Target project requirements

adacovex assesses an Ada/SPARK project. The target root can be the repository root or a subdirectory (via --target=PATH). For a meaningful report, the target must provide the items that follow. Any missing item shows as N/A.

DAL checks that depend on the missing item report Unmet.

What the target provides

  1. Ada source files (.ads) under the target root – scanned for subprogram declarations, docstrings, and HLR traceability tags. See the docstring spec for the annotation format and coverage rules.

  2. GNATprove output – a gnatprove.out summary, discovered in this order:

    • <target>/obj/gnatprove/gnatprove.out

    • <target>/gnatprove.out

    • <target>/gnatprove/gnatprove.out

    Or run adacovex prove (or the GitHub Action with prove: true) to generate a fresh summary before you assess.

  3. Test results – a test-summary file, auto-discovered from a conventional name at the project root or under docs/ (for example test_result.md, test_results.md, test-result.md, tests.md, test_result.txt, test_results.log, docs/test_result.md, …). Supported formats come from your runner’s log or a summary file:

    • Markdown tables: the native test_runner layout | Category | N | PASS | and the AUnit-report layout | - | Category | N | PASS |

    • TAP (ok/not ok)

    • GNU Automake (PASS:/FAIL:)

    • Maven Surefire (Tests run: N)

    • Unity (N Tests M Failures)

    See the test format spec for the detailed rules (what each line looks like and which line wins when formats mix).

  4. HLR / LLR documents (for DAL assessment) – <target>/docs/compliance/HLR.md and optionally <target>/docs/compliance/LLR.md, following the HLR traceability-tag format.

Missing data

Missing

Effect

No .ads sources

No packages scanned; metrics report zero

No gnatprove.out

SPARK level Stone, proof metrics N/A

No test summary

Test metrics N/A; DAL Tests passing criterion Unmet

No docs/compliance/HLR.md

HLR coverage N/A; DAL traceability criteria Unmet

Language support

adacovex is a tool for Ada/SPARK, and Ada/SPARK is the only first-class language: source scanning, docstring coverage, HLR traceability, DAL assessment, and the proof pipeline are Ada-specific. Every other language joins the SBOM, complexity, and test-dependency tooling at the level that applies to it. The tiers below make the support explicit, so a team knows what to expect before it runs an assessment.

Ada / SPARK – first-class

  • Full source scan of .ads / .adb (subprograms, docstrings, HLR tags).

  • Per-subprogram cyclomatic complexity.

  • SPARK proof analysis and the Platinum-level proof gate.

  • DO-178C / ISO 26262 / IEC 62304 DAL assessment.

  • Alire / GPR manifests build the Ada dependency graph in the SBOM.

This is the only tier whose assessment a project can fully rely on.

Manifest-aware ecosystems – SBOM dependency graph

These languages’ manifests contribute first-class dependency graph entries (with the right PURL type, scope, and licence resolution): package.json (npm), Cargo.toml / Cargo.lock (cargo), go.mod (go), pyproject.toml and requirements*.txt (pypi), composer.json (composer), Gemfile / Gemfile.lock (gem), pom.xml (maven), Package.swift (swift), plus Alire and GPR files for Ada. Each ecosystem gives the resolved dependency its language, PURL, scope (base / dev / test / transitive / vendored), and a licence when the local manifest or registry answers. See sbom.md for the full manifest table.

Extension-detected languages – component language, complexity, test deps

The source extensions below are recognised for three purposes:

  1. Component language detection: vendored trees, vendor/, node_modules, resources, and loose source drops report their language(s) from the extensions actually present (a directory mixes languages and reports its top 3).

  2. The complexity subcommand: per-file lines of code and decision counts for these languages (Ada is the only per-subprogram analysis).

  3. Test-dependency names: the npm/Cargo/Go/Maven/PyPI test-label heuristic works from the dependency name and is language-independent.

The recognised extensions are: Ada (.ads .adb .ada .gpr), JavaScript (.js .mjs .cjs), TypeScript (.ts .tsx), CSS (.css), HTML (.html .htm), Python (.py), Go (.go), Rust (.rs), C (.c .h), C++ (.cpp .cc .cxx .hpp .hh .hxx), C# (.cs), Java (.java), Ruby (.rb), PHP (.php), Swift (.swift), Kotlin (.kt .kts), Scala (.scala), OCaml (.ml .mli), Lua (.lua), Perl (.pl), Haskell (.hs), Elixir (.ex .exs), Erlang (.erl .hrl), Clojure (.clj .cljs), Dart (.dart), Shell (.sh .bash), PowerShell (.ps1), SQL (.sql), Fortran (.f .f90 .f95 .f03), Assembly (.s .asm), R (.r), Julia (.jl), Zig (.zig), VHDL (.vhd .vhdl), and Tcl (.tcl).

The extension is the source of truth: a .py file reports Python even when a Cargo.toml sits next to it. The manifest language only breaks ties.

Python requirements files

The requirements*.txt parser is deliberately flexible: a literal requirements.txt at the target root always wins, and adacovex falls back to the first requirements*.txt in that directory when the fixed name is missing. Entries register as dev-scope pkg:pypi/* components of the root (the real packages – for example sphinx and myst-parser – never become generic system tools). A version pinned in the requirements line wins; the package registry (pip index versions) fills a missing version and the licence/website when it is online. A missing registry or an offline machine keeps a name-only entry – adacovex never guesses a version or licence.

For anything outside these tiers, adacovex still runs its Ada/SPARK assessment on the project’s Ada sources (and reads its Alire manifest) when they exist; a pure-foreign-language repository contributes its SBOM components, language detections, and complexity scores but no Ada metrics.

Vendored code and strict mode

By default (strict mode) adacovex scans and counts every directory except the always-excluded ones. Vendored code is included. For third-party code you cannot modify, use docstring patch files at <target>/.adacovex/patches/<relative-path> (see Architecture – Patch System). Or run in relaxed mode (--relaxed, skip dirs, no patches) (see Strict vs relaxed mode).

Vendored code can also take part in the SPARK proof. A patch carrying SPARK_Mode / Pre / Post / Global aspects is a proof patch. The prove subcommand merges it into a patched tree copy. The copy uses .ads spec contracts and .adb body patches that opt a SPARK-clean vendored body into the proof.

See Proving and writing proofs for how to write them. See Architecture – Proof patches for the design.