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

-----------------------------------------------------------------------------------------------------
SPARK Analysis results        Total        Flow                        Provers   Justified   Unproved
-----------------------------------------------------------------------------------------------------
Data Dependencies                24          24                              .           .          .
Flow Dependencies                 .           .                              .           .          .
Initialization                    3           3                              .           .          .
Non-Aliasing                      .           .                              .           .          .
Run-time Checks                 166           .    152 (CVC5 78%, Trivial 22%)           .         14
Assertions                        2           .                       2 (CVC5)           .          .
Functional Contracts             47           .      46 (CVC5 94%, Trivial 6%)           .          1
LSP Verification                  .           .                              .           .          .
Termination                      52          52                              .           .          .
Concurrency                       .           .                              .           .          .
-----------------------------------------------------------------------------------------------------
Total                           294    79 (27%)                      200 (68%)           .    15 (5%)


max steps used for successful proof: 7325

Analyzed 25 units

in unit daxpy_pkg, 52 subprograms and packages out of 206 analyzed
  Daxpy_Pkg at daxpy_pkg.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Daxpy_Pkg.Daxpy at daxpy_pkg.ads:27 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 39 checks out of 50 proved