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

------------------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow                                    Provers   Justified   Unproved
------------------------------------------------------------------------------------------------------------------
Data Dependencies                60           60                                          .           .          .
Flow Dependencies                 .            .                                          .           .          .
Initialization                    6            6                                          .           .          .
Non-Aliasing                      .            .                                          .           .          .
Run-time Checks                 234            .    210 (CVC5 83%, Trivial 16%, altergo 0%)           .         24
Assertions                        4            .                                   4 (CVC5)           .          .
Functional Contracts            109            .                 99 (CVC5 90%, Trivial 10%)           .         10
LSP Verification                  .            .                                          .           .          .
Termination                     115          115                                          .           .          .
Concurrency                       .            .                                          .           .          .
------------------------------------------------------------------------------------------------------------------
Total                           528    181 (34%)                                  313 (59%)           .    34 (6%)


max steps used for successful proof: 26495

Analyzed 25 units

in unit dgetrf_pkg, 133 subprograms and packages out of 518 analyzed
  Dgetrf_Pkg at dgetrf_pkg.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dgetrf_Pkg.Compute_Lu_Factorization at dgetrf_pkg.ads:77 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 25 checks out of 47 proved
  Dgetrf_Pkg.Get_Elem at dgetrf_pkg.adb:3 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 0 checks out of 6 proved
  Dgetrf_Pkg.Matrix_Element at dgetrf_pkg.ads:47 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 7 checks out of 8 proved
  Dgetrf_Pkg.Pivot_Element at dgetrf_pkg.ads:59 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (4 checks)
  Dgetrf_Pkg.Set_Elem at dgetrf_pkg.adb:8 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dgetrf_Pkg.Set_Pivot at dgetrf_pkg.adb:15 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dgetrf_Pkg.U_Diagonal_Element at dgetrf_pkg.ads:67 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 2 checks out of 3 proved