adacovex Verification Report

Source Overview

Metric

Value

Packages Scanned

26

Total Subprograms

59

Documented Subprograms

59

Docstring Coverage

100%

SPARK Proof Analysis

Check Type

Count

Proved

SPARK Level

Platinum

-

Flow Dependencies

0

0

Initialization

13

13

Runtime Checks

358

358

Assertions

60

60

Functional Contracts

13

13

Termination

44

32

Total

500

500

Test Results

Category

Tests

Status

Total

** 295**

Passed: 295, Failed: 0

DO-178C Compliance

Criterion

Status

Target DAL

C

Overall Status

Achieved

HLR Traced

47 / 47

Orphan Tags

No

Tests Passing

Yes

Min SPARK Level

Yes