adacovex 1.5.0

Date: 2026-08-05

Version bumped 1.4.0 -> 1.5.0.

Changes

C1: More standard docstring styles

The source scanner now recognises additional standard docstring conventions, so third-party and code-generated Ada is counted correctly:

  • Comment prefixes: besides the canonical --  (two dashes + two spaces), the single-space -- and tab-separated (--<TAB>) styles are recognised as docstrings. A bare -- or --- divider is still not a docstring.

  • Tag aliases: @parameter == @param, @returns == @return.

  • Summary tags: @brief and @summary mark a subprogram as documented.

C2: More test-result formats

Adacovex.Parsers.Tests now also parses the following standard formats (additively with the existing Markdown-table parser):

  • TAP – ok N - name / not ok N - name lines

  • Automake test-suite – PASS: name / FAIL: name lines

  • Maven Surefire – Tests run: N, Failures: M, Errors: E summaries (failed = failures + errors)

  • Unity – N Tests M Failures summaries (the count may be separated from the word by spaces)

C3: Longer source lines

Max_Line is raised from 8192 to 262144 characters, so single-line declarations from heavily code-generated projects (previously drained silently) are parsed in full.

C4: Dev-manifest proof swap (prove subcommand)

When the target project declares gnatprove only in alire-dev.toml (keeping the publishing alire.toml clean), the prove subcommand now runs the proof through a temporary shell wrapper that backs up alire.toml / alire.lock / alire/, swaps the dev manifest over the publishing one, runs alr exec -- gnatprove -P <gpr>, and restores everything (via trap ... EXIT INT TERM) even on failure or interruption. The assessment and SBOM pipeline always scans the publishing alire.toml, so dev-only tool declarations never leak into dependency graphs or SBOMs. This fixes make run-ada-crdt / make prove against projects (e.g.

Ada_CRDT) that keep gnatprove out of their publishing manifest.

C5: IR layer – bounded target type profiles

New src/ir/ layer implements the first stage of an intermediate representation for cross-compilation assessments:

  • Adacovex.Target_Profiles (SPARK On): bounded machine-integer types IR_Int8..IR_Int64 (fixed-width signed ranges with Size clauses) and IR_UInt8..IR_UInt64 (modular unsigned), plus Word_Size and a Target_Config record carrying Host_Bits / Target_Bits / Pointer_Bits. Checked_Add32 / Checked_Add64 perform overflow-checked addition on the bounded types.

  • Adacovex.IR_Synthesiser (SPARK Off, string generation): IR_Type_Name, Lower_Type_Name (case-sensitive: int8_t..uint64_t, size_t/usize -> unsigned target-width, isize -> signed target-width, ptrdiff_t / uintptr_t -> pointer-width), and Synthesize_Package that splits a comma/whitespace-separated type list into synthesized bounded Ada declarations.

  • Adacovex.IR_Bounds (SPARK On): a gnatprove fixture that derives int32_t / int64_t from the bounded IR types and proves the overflow checks on Add32 / Add64 – absence of integer overflow on the lowered types is machine-checked.

C6: Google / Sphinx docstring styles

The source scanner now also recognises the two most common non-Ada docstring conventions, so the same subprogram can be documented in Ada, Google, or Sphinx style:

  • Google: Args: / Args: ... headers open a parameter block (deeper-indented following comment lines count as parameters); a Returns: header marks the return-value description.

  • Sphinx: :param Name:, :parameter Name:, :type Name:, :return:, :returns:, and :rtype: fields are all recognised.

Fixes

H1: Unity summary count separated by a space

Number_Before_Word only looked at the character immediately before the keyword, so 1 Failures (number + space + word) parsed as zero failures and overwrote the correct totals. It now skips spaces back to the preceding digit run.

Test Suite

Test suite extended: Source scanner 40 -> 68 checks (comment-style variants, tag aliases, Google/Sphinx styles, 12000-char single-line declaration); Test-result parser 27 -> 35 checks (TAP, Automake, Surefire, Unity); new IR synthesis category (26 checks). The suite is now 284 tests.

Proof Results

Self-assessment: Platinum (36/36 VCs proved, AoRTE-free) – the four overflow-checked adds on the bounded IR types (Target_Profiles.Checked_Add32/64, IR_Bounds.Add32/64) are all machine proved. Ada_CRDT proof run verified end-to-end via the dev-manifest swap (279 VCs, 5 justified).

Traceability

New HLR HLR-IR (IR type profiles, host/target config, and foreign type-name lowering) covers the new src/ir/ packages. Existing tags continue to cover the changed packages (-- HLR-SCAN on Adacovex. Parsers. Source, -- HLR-TEST on `Adacovex.

Parsers. Tests, – HLR-PROVEonAdacovex. Core. Prove`).