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

------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow                        Provers   Justified   Unproved
------------------------------------------------------------------------------------------------------
Data Dependencies                36           36                              .           .          .
Flow Dependencies                 .            .                              .           .          .
Initialization                    2            2                              .           .          .
Non-Aliasing                      .            .                              .           .          .
Run-time Checks                 170            .    152 (CVC5 75%, Trivial 25%)           .         18
Assertions                        8            .                       4 (CVC5)           .          4
Functional Contracts             60            .     60 (CVC5 90%, Trivial 10%)           .          .
LSP Verification                  .            .                              .           .          .
Termination                      73           73                              .           .          .
Concurrency                       .            .                              .           .          .
------------------------------------------------------------------------------------------------------
Total                           349    111 (32%)                      216 (62%)           .    22 (6%)


max steps used for successful proof: 7325

Analyzed 25 units

in unit ddot_pkg, 77 subprograms and packages out of 308 analyzed
  Ddot_Pkg at ddot_pkg.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Ddot_Pkg.Dot_Product at ddot_pkg.ads:35 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 17 checks out of 35 proved