Adacovex.Compliance.DAL

Run DAL compliance assessment for any DAL level (A-E). Evaluates HLR trace coverage, orphan tag absence, test pass rate, and minimum SPARK proof level (per-level criteria). The routine populates Assessment with pass/fail results and detailed failure reasons. @param Level Target DAL level (A-E). @param Target_Dir Project root directory. @param Packages Scanned package vector. @param Proof_Summary GNATprove proof results. @param Test_Summary Test run results. @param Assessment Output DAL assessment record. @param Use_Cache When True the HLR.md/LLR.md parses are served from the on-disk result cache when unchanged; when False they are always re-parsed (–no-cache).

See also: DAL Levels | Standards

Note: All items in this package are public.

Functions

function Is_DAL_Achieved (Assessment : Adacovex.Types.Implementation.DAL_Assessment) return Standard.Boolean [Global]

Parameter	Description
Assessment	DAL assessment record.

Returns: True if Assessment.Status = Achieved.

function Min_SPARK_For (Level : Adacovex.Types.DAL_Level) return Adacovex.Types.SPARK_Level [Post] [Global] [SPARK]

Parameter	Description
Level	Target DAL level (A-E).

Returns: The minimum SPARK level that satisfies the criteria of the level.

function Need_Tests (Level : Adacovex.Types.DAL_Level) return Standard.Boolean [Post] [Global] [SPARK]

Parameter	Description
Level	Target DAL level (A-E).

Returns: True unless Level is DAL-E.

Procedures

procedure Assess_DAL (Level : Adacovex.Types.DAL_Level; Target_Dir : Standard.String; Packages : Adacovex.Types.Implementation.Package_Vectors.Vector; Proof_Summary : Adacovex.Types.Proof_Summary; Test_Summary : Adacovex.Types.Implementation.Test_Summary; Assessment : Adacovex.Types.Implementation.DAL_Assessment; Use_Cache : Standard.Boolean)

Parameter	Description
Assessment	Output DAL assessment record.
Level	Target DAL level (A-E).
Packages	Scanned package vector.
Proof_Summary	GNATprove proof results.
Target_Dir	Project root directory.
Test_Summary	Test run results.
Use_Cache	When True the HLR.md/LLR.md parses are served from

procedure Assess_Standard (Standard : Adacovex.Types.Compliance_Standard; Level : Adacovex.Types.DAL_Level; Target_Dir : Standard.String; Packages : Adacovex.Types.Implementation.Package_Vectors.Vector; Proof_Summary : Adacovex.Types.Proof_Summary; Test_Summary : Adacovex.Types.Implementation.Test_Summary; Assessment : Adacovex.Types.Implementation.DAL_Assessment; Use_Cache : Standard.Boolean)

Parameter	Description
Assessment	Output assessment record (Standard field set).
Level	Rigor tier (reused DAL level A-E).
Packages	Scanned package vector.
Proof_Summary	GNATprove proof results.
Standard	Compliance standard (DO_178C, ISO_26262, IEC_62304).
Target_Dir	Project root directory.
Test_Summary	Test run results.
Use_Cache	When True the HLR.md/LLR.md parses are served from