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

------------------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total         Flow                                    Provers   Justified   Unproved
------------------------------------------------------------------------------------------------------------------
Data Dependencies                60           60                                          .           .          .
Flow Dependencies                 .            .                                          .           .          .
Initialization                   12           12                                          .           .          .
Non-Aliasing                      .            .                                          .           .          .
Run-time Checks                 340            .    294 (CVC5 85%, Trivial 15%, altergo 0%)           .         46
Assertions                        4            .                                   4 (CVC5)           .          .
Functional Contracts            130            .                 128 (CVC5 91%, Trivial 9%)           .          2
LSP Verification                  .            .                                          .           .          .
Termination                     115          115                                          .           .          .
Concurrency                       .            .                                          .           .          .
------------------------------------------------------------------------------------------------------------------
Total                           661    187 (28%)                                  426 (64%)           .    48 (7%)


max steps used for successful proof: 27946

Analyzed 25 units

in unit fftpack_cfft_pkg, 139 subprograms and packages out of 524 analyzed
  Fftpack_Cfft_Pkg at fftpack_cfft_pkg.ads:7 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and proved (0 checks)
  Fftpack_Cfft_Pkg.Build_Factor_Table at fftpack_cfft_pkg.ads:152 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 5 checks out of 6 proved
  Fftpack_Cfft_Pkg.Build_Twiddle_Table at fftpack_cfft_pkg.ads:168 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 3 checks out of 6 proved
  Fftpack_Cfft_Pkg.Butterfly_Generic at fftpack_cfft_pkg.ads:273 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 13 checks out of 16 proved
  Fftpack_Cfft_Pkg.Butterfly_Radix_2 at fftpack_cfft_pkg.ads:183 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 7 checks out of 9 proved
  Fftpack_Cfft_Pkg.Butterfly_Radix_3 at fftpack_cfft_pkg.ads:201 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 8 checks out of 10 proved
  Fftpack_Cfft_Pkg.Butterfly_Radix_4 at fftpack_cfft_pkg.ads:222 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 9 checks out of 11 proved
  Fftpack_Cfft_Pkg.Butterfly_Radix_5 at fftpack_cfft_pkg.ads:246 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 10 checks out of 12 proved
  Fftpack_Cfft_Pkg.DFT_Coefficient_Imag at fftpack_cfft_pkg.ads:54 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 16 checks out of 20 proved
  Fftpack_Cfft_Pkg.DFT_Coefficient_Real at fftpack_cfft_pkg.ads:45 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 16 checks out of 20 proved
  Fftpack_Cfft_Pkg.Forward_Fft at fftpack_cfft_pkg.ads:94 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 37 checks out of 50 proved
  Fftpack_Cfft_Pkg.Forward_Fft_Driver at fftpack_cfft_pkg.ads:124 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 15 checks out of 19 proved
  Fftpack_Cfft_Pkg.Initialise_Fft at fftpack_cfft_pkg.ads:73 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 8 checks out of 10 proved
  Fftpack_Cfft_Pkg.Product_Of_Factors at fftpack_cfft_pkg.ads:63 flow analyzed (0 errors, 0 checks, 0 warnings and 0 pragma Assume statements) and not proved, 4 checks out of 6 proved