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

-----------------------------------------------------------------------------------------------------
SPARK Analysis results        Total        Flow                        Provers   Justified   Unproved
-----------------------------------------------------------------------------------------------------
Data Dependencies                24          24                              .           .          .
Flow Dependencies                 .           .                              .           .          .
Initialization                    5           5                              .           .          .
Non-Aliasing                      .           .                              .           .          .
Run-time Checks                 161           .    139 (CVC5 74%, Trivial 26%)           .         22
Assertions                        4           .                       4 (CVC5)           .          .
Functional Contracts             46           .      45 (CVC5 94%, Trivial 6%)           .          1
LSP Verification                  .           .                              .           .          .
Termination                      52          52                              .           .          .
Concurrency                       .           .                              .           .          .
-----------------------------------------------------------------------------------------------------
Total                           292    81 (28%)                      188 (64%)           .    23 (8%)


max steps used for successful proof: 7325

Analyzed 25 units

in unit dnrm2_pkg, 54 subprograms and packages out of 208 analyzed
  Dnrm2_Pkg at dnrm2_pkg.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dnrm2_Pkg.Euclidean_Norm at dnrm2_pkg.ads:49 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 16 checks out of 26 proved
  Dnrm2_Pkg.Selected_Value at dnrm2_pkg.ads:27 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 7 checks out of 11 proved
  Dnrm2_Pkg.Sum_Of_Squares at dnrm2_pkg.ads:38 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 4 checks out of 9 proved