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

--------------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow                               Provers   Justified    Unproved
--------------------------------------------------------------------------------------------------------------
Data Dependencies                36           36                                     .           .           .
Flow Dependencies                 .            .                                     .           .           .
Initialization                    5            5                                     .           .           .
Non-Aliasing                      .            .                                     .           .           .
Run-time Checks                 224            .    184 (CVC5 84%, Trivial 16%, Z3 1%)           .          40
Assertions                       12            .            12 (CVC5 80%, Trivial 20%)           .           .
Functional Contracts             78            .             70 (CVC5 96%, Trivial 4%)           .           8
LSP Verification                  .            .                                     .           .           .
Termination                      75           73                              2 (CVC5)           .           .
Concurrency                       .            .                                     .           .           .
--------------------------------------------------------------------------------------------------------------
Total                           430    114 (27%)                             268 (62%)           .    48 (11%)


max steps used for successful proof: 33746

Analyzed 25 units

in unit dpotrf_pkg, 84 subprograms and packages out of 315 analyzed
  Dpotrf_Pkg at dpotrf_pkg.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dpotrf_Pkg.Compute_Cholesky_Factorization at dpotrf_pkg.ads:121 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 36 checks out of 61 proved
  Dpotrf_Pkg.Get_Elem at dpotrf_pkg.adb:9 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 0 checks out of 6 proved
  Dpotrf_Pkg.Lower_Cholesky_Reconstructs at dpotrf_pkg.ads:79 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 5 checks out of 7 proved
  Dpotrf_Pkg.Lower_Cholesky_Sum_Of_Products at dpotrf_pkg.ads:47 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 8 checks out of 12 proved
  Dpotrf_Pkg.Matrix_Element at dpotrf_pkg.ads:35 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 7 checks out of 8 proved
  Dpotrf_Pkg.Set_Elem at dpotrf_pkg.adb:14 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dpotrf_Pkg.Upper_Cholesky_Reconstructs at dpotrf_pkg.ads:100 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 5 checks out of 7 proved
  Dpotrf_Pkg.Upper_Cholesky_Sum_Of_Products at dpotrf_pkg.ads:63 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 8 checks out of 12 proved