Summary of SPARK analysis
=========================

-------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow                        Provers   Justified    Unproved
-------------------------------------------------------------------------------------------------------
Data Dependencies                36           36                              .           .           .
Flow Dependencies                 .            .                              .           .           .
Initialization                    1            1                              .           .           .
Non-Aliasing                      .            .                              .           .           .
Run-time Checks                 213            .    178 (CVC5 81%, Trivial 19%)           .          35
Assertions                        2            .                       2 (CVC5)           .           .
Functional Contracts             74            .      63 (CVC5 93%, Trivial 7%)           .          11
LSP Verification                  .            .                              .           .           .
Termination                      73           73                              .           .           .
Concurrency                       .            .                              .           .           .
-------------------------------------------------------------------------------------------------------
Total                           399    110 (28%)                      243 (61%)           .    46 (12%)


max steps used for successful proof: 7325

Analyzed 25 units

in unit dgemv_pkg, 82 subprograms and packages out of 313 analyzed
  Dgemv_Pkg at dgemv_pkg.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dgemv_Pkg.A_At at dgemv_pkg.ads:55 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 8 checks out of 10 proved
  Dgemv_Pkg.Dgemv at dgemv_pkg.ads:112 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 15 checks out of 41 proved
  Dgemv_Pkg.Logical_X_Index at dgemv_pkg.ads:34 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 16 checks out of 19 proved
  Dgemv_Pkg.Matvec_Element at dgemv_pkg.ads:90 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (1 checks)
  Dgemv_Pkg.Partial_Dot at dgemv_pkg.ads:67 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 0 checks out of 8 proved
  Dgemv_Pkg.X_Logical at dgemv_pkg.ads:42 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 4 checks out of 7 proved