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

------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total        Flow                        Provers   Justified    Unproved
------------------------------------------------------------------------------------------------------
Data Dependencies                12          12                              .           .           .
Flow Dependencies                 .           .                              .           .           .
Initialization                    .           .                              .           .           .
Non-Aliasing                      .           .                              .           .           .
Run-time Checks                 135           .    126 (CVC5 75%, Trivial 25%)           .           9
Assertions                        6           .                       3 (CVC5)           .           3
Functional Contracts             32           .     19 (CVC5 90%, Trivial 10%)           .          13
LSP Verification                  .           .                              .           .           .
Termination                      31          31                              .           .           .
Concurrency                       .           .                              .           .           .
------------------------------------------------------------------------------------------------------
Total                           216    43 (20%)                      148 (69%)           .    25 (12%)


max steps used for successful proof: 7325

Analyzed 25 units

in unit dscal_pkg, 27 subprograms and packages out of 104 analyzed
  Dscal_Pkg at dscal_pkg.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dscal_Pkg.Scale_Vector at dscal_pkg.ads:15 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 25 checks out of 46 proved