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

--------------------------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow                                           Provers   Justified    Unproved
--------------------------------------------------------------------------------------------------------------------------
Data Dependencies                36           36                                                 .           .           .
Flow Dependencies                 .            .                                                 .           .           .
Initialization                    6            6                                                 .           .           .
Non-Aliasing                      .            .                                                 .           .           .
Run-time Checks                 220            .    178 (CVC5 80%, Trivial 19%, Z3 1%, altergo 0%)           .          42
Assertions                       14            .                                         14 (CVC5)           .           .
Functional Contracts             82            .                         70 (CVC5 95%, Trivial 5%)           .          12
LSP Verification                  .            .                                                 .           .           .
Termination                      74           73                                          1 (CVC5)           .           .
Concurrency                       .            .                                                 .           .           .
--------------------------------------------------------------------------------------------------------------------------
Total                           432    115 (27%)                                         263 (61%)           .    54 (13%)


max steps used for successful proof: 32413

Analyzed 25 units

in unit dgeqrf_pkg, 87 subprograms and packages out of 318 analyzed
  Dgeqrf_Pkg at dgeqrf_pkg.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dgeqrf_Pkg.Compute_Qr_Factorization at dgeqrf_pkg.ads:111 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 43 checks out of 75 proved
  Dgeqrf_Pkg.Encodes_Orthogonal_Reflector at dgeqrf_pkg.ads:93 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 1 checks out of 4 proved
  Dgeqrf_Pkg.Get_Elem at dgeqrf_pkg.adb:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 0 checks out of 6 proved
  Dgeqrf_Pkg.Matrix_Element at dgeqrf_pkg.ads:37 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 7 checks out of 8 proved
  Dgeqrf_Pkg.R_Factor_Element at dgeqrf_pkg.ads:102 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 0 checks out of 1 proved
  Dgeqrf_Pkg.Reflector_Norm_Squared at dgeqrf_pkg.ads:88 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 0 checks out of 1 proved
  Dgeqrf_Pkg.Reflector_V_Component at dgeqrf_pkg.ads:57 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 2 checks out of 3 proved
  Dgeqrf_Pkg.Set_Elem at dgeqrf_pkg.adb:12 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dgeqrf_Pkg.Sign_Of at dgeqrf_pkg.adb:19 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Dgeqrf_Pkg.Sum_Of_Reflector_Squares at dgeqrf_pkg.ads:72 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 7 checks out of 12 proved
  Dgeqrf_Pkg.Tau_Element at dgeqrf_pkg.ads:49 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (4 checks)