-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================

--------------------------------------------------------------------------------
--Synopsis:                                                                   --
--                                                                            --
--Package providing data structure to store running totals, and a procedure   --
--to print them.                                                              --
--                                                                            --
--------------------------------------------------------------------------------

with Banner;
with CommandLine;
with E_Strings;
with FatalErrors;
with Heap;
with VCHeap;
with VCDetails;

use type VCDetails.VC_State_T;
use type VCDetails.DPC_State_T;

package body Total
--# own State is The_Totals;
is

   type VC_Counter is array (VCDetails.Terminal_Point_Type) of Natural;
   type Error_Type_Counter is array (VCDetails.Error_Type) of Natural;

   Null_VC_Counter : constant VC_Counter := VC_Counter'(others => 0);

   -- if adding more entries to this type, you must alter the procedure
   -- Output below to display the results, and add code in the appropriate
   -- analysis routines to increment the counter(s). You must also alter
   -- the aggregate in Initialize below to initialize the new counter
   type Total_Type is record

      -- Subprograms without errors (all subprograms have vcs).
      Subprograms_With_VCs : Natural;

      -- Subprograms with errors.
      Subprograms_Where_Error                  : Error_Type_Counter;
      Subprograms_Where_VC_Analysis_Abandoned  : Natural;
      Subprograms_Where_DPC_Analysis_Abandoned : Natural;

      -- A subprogram with At Least One (ALO) Undischarged VC.
      Subprograms_With_ALO_Undischarged_VC : Natural;

      -- The following fields record the number of subprograms,
      -- which are not necessarily fully proved, but have at least
      -- one VC proved by each of the following strategies:

      -- A subprogram with At Least One (ALO) VC proved by
      -- the Examiner.
      Subprograms_With_ALO_Examiner_VC : Natural;

      -- A subprogram with At Least One (ALO) VC proved by the
      -- simplifier without a user defined rule.
      Subprograms_With_ALO_Simplifier_VC : Natural;

      -- A subprogram with At Least One (ALO) VC proved using
      -- a using proof by contradiction.
      Subprograms_With_ALO_Contradiction_VC : Natural;

      -- A subprogram with At Least One (ALO) VC proved using
      -- a user defined rule.
      Subprograms_With_ALO_User_Rule_VC : Natural;

      -- A subprogram with At Least One (ALO) VC proved by Victor
      Subprograms_With_ALO_Victor_VC : Natural;

      -- A subprogram with At Least One (ALO) VC proved by Riposte
      Subprograms_With_ALO_Riposte_VC : Natural;

      -- A subprogram with At Least One (ALO) VC proved using
      -- the Checker.
      Subprograms_With_ALO_Checker_VC : Natural;

      -- A subprogram with At Least One (ALO) VC discharged by review
      Subprograms_With_ALO_Review_VC : Natural;

      -- A subprogram with At Least One (ALO) false VC.
      Subprograms_With_ALO_False_VC : Natural;

      -- The following fields represent the use of a hierachy of
      -- proof strategies:
      --   Examiner -> Simplifier -> User Rules -> ViCToR -> Checker -> Review
      -- When a subprogram is proved, the strategy latest in the hierarchy
      -- is considered to have been used to complete the proof, even
      -- if earlier strategies have also been applied.
      -- The hierachy gives a measure of the extent of the strategies
      -- required in proving a subprogram.
      -- The definitions of the hierarchical strategies is given below:
      -- A subprogram proof is completed by the examiner if:
      --    o at LEAST one VC was proved by the examiner and
      --    o ZERO VCs were proved by the simplifier,
      --      Victor, Riposte, the checker, review file or left Undischarged and
      --    o the subprogram has no false VCs.
      Subprograms_Proved_By_Examiner : Natural;

      -- A subprogram proof is completed by the simplifier if:
      --    o at LEAST one VC was proved by the simplifier and
      --    o ZERO VCs were proved by Victor, Riposte,, the checker, review file
      --      or left Undischarged and
      --    o the subprogram has no false VCs.
      Subprograms_Proved_By_Simplifier : Natural;

      -- A subprogram proof is completed by a user defined proof rule if:
      --    o at least one VC was proved by the simplifier and
      --    o at least one user defined rule has been used in the proof of a VC and
      --    o ZERO VCs were proved by Victor, Riposte, the checker, review file
      --      or left Undischarged and
      --    o the subprogram has no false VCs.
      Subprograms_Proved_With_User_Proof_Rule : Natural;

      -- A subprogram proof is completed by ViCToR if:
      --    o at least one VC was proved by ViCToR and
      --    o ZERO VCs were proved by the Riposte, checker, review file,
      --      or left Undischarged and
      --    o the subprogram has no false VCs.
      Subprograms_Proved_By_Victor : Natural;

      -- A subprogram proof is completed by Riposte if:
      --    o at least one VC was proved by Riposte and
      --    o ZERO VCs were proved by the checker, review file
      --      or left Undischarged and
      --    o the subprogram has no false VCs.
      Subprograms_Proved_By_Riposte : Natural;

      -- A subprogram proof is completed by the checker if:
      --    o at LEAST one VC was proved by the checker and
      --    o ZERO VCs were proved by the review file or
      --      left Undischarged and
      --    o the subprogram has no false VCs.
      Subprograms_Proved_By_Checker : Natural;

      -- A subprogram proof is completed by review if:
      --    o at LEAST one VC was proved in the review file and
      --    o ZERO VCs were left Undischarged and
      --    o the subprogram has no false VCs.
      Subprograms_Proved_By_Review : Natural;

      -- The following fields record the number of VCs proved by
      -- each strategy grouped by the sort of origin (the terminal point)
      -- of the VC.
      VCs_Total                       : VC_Counter;
      VCs_Proved_By_Examiner          : VC_Counter;
      VCs_Proved_By_Simplifier        : VC_Counter;
      VCs_Proved_With_User_Proof_Rule : VC_Counter;
      VCs_Proved_By_Victor            : VC_Counter;
      VCs_Proved_By_Riposte           : VC_Counter;
      VCs_Proved_By_Checker           : VC_Counter;
      VCs_Proved_By_Review            : VC_Counter;
      VCs_Proved_False                : VC_Counter;
      VCs_Undischarged                : VC_Counter;

      -- Record number of subprograms with DPCs
      Subprograms_With_DPCs : Natural;

      -- The following fields record the number of dead paths ZombieScope
      -- has found.
      Number_Of_Dead_Paths        : Natural;
      Subprograms_With_Dead_Paths : Natural;
   end record;

   The_Totals : Total_Type;

   function Sum (T : in VC_Counter) return Natural is
      Result : Natural := 0;
   begin
      for I in VCDetails.Terminal_Point_Type loop
         Result := Result + T (I);
      end loop;
      return Result;
   end Sum;

   procedure Calculate_Percentages
     (The_Totals                     : in     Total_Type;
      Percent_Undischarged_Str       :    out E_Strings.T;
      Percent_Proved_By_Examiner_Str :    out E_Strings.T;
      Percent_Proved_By_Victor_Str   :    out E_Strings.T;
      Percent_Proved_By_Riposte_Str  :    out E_Strings.T;
      Percent_Proved_By_Checker_Str  :    out E_Strings.T;
      Percent_Proved_By_Review_Str   :    out E_Strings.T;
      Percent_Simplified_Str         :    out E_Strings.T;
      Percent_With_User_Rule_Str     :    out E_Strings.T;
      Percent_Proved_False_Str       :    out E_Strings.T)
   --# derives Percent_Proved_By_Checker_Str,
   --#         Percent_Proved_By_Examiner_Str,
   --#         Percent_Proved_By_Review_Str,
   --#         Percent_Proved_By_Riposte_Str,
   --#         Percent_Proved_By_Victor_Str,
   --#         Percent_Proved_False_Str,
   --#         Percent_Simplified_Str,
   --#         Percent_Undischarged_Str,
   --#         Percent_With_User_Rule_Str     from The_Totals;
   --# pre Sum (The_Totals.VCs_Total) /= 0;
   is
      subtype Percentage is Natural range 0 .. 100;

      VCs_Total : Natural;

      procedure Total_And_Value_To_Percentage
        (Overall_Total : in     Natural;
         Value         : in     Natural;
         Percent       :    out Percentage;
         Percent_C     :    out Character)
      --# derives Percent,
      --#         Percent_C from Overall_Total,
      --#                        Value;
      --# pre (Overall_Total/=0);
      is
         Percise_Percent_Value : Float;
         Rounded_Percent_Value : Percentage;
      begin
         Percise_Percent_Value := (Float (Value) * 100.0) / Float (Overall_Total);
         Rounded_Percent_Value := Percentage (Percise_Percent_Value);

         case Rounded_Percent_Value is

            -- If the rounded percentage value is zero, but the actual
            -- value is non-zero, then the rounded value is forced to be 1.
            -- This behaviour ensures that a zero percentage really means
            -- zero.
            when 0 =>
               if (Value /= 0) then
                  Percent := 1;

                  -- If the actual percent is less than 0.5 then this is
                  -- indicated with an appropriate leading character.
                  if (Percise_Percent_Value < 0.5) then
                     Percent_C := '<';
                  else
                     Percent_C := ' ';
                  end if;
               else
                  Percent   := 0;
                  Percent_C := ' ';
               end if;

               -- If the rounded percentage value is 100, but the actual value
               -- is not equal to the total, then the rounded value is forced
               -- to be 99. This behaviour ensures that a hundred percent
               -- really means all.
            when 100 =>
               if (Value /= Overall_Total) then
                  Percent := 99;

                  -- If the actual percent is greater than 99.5 then this is
                  -- indicated with an appropriate leading character.
                  if (Percise_Percent_Value > 99.5) then
                     Percent_C := '>';
                  else
                     Percent_C := ' ';
                  end if;
               else
                  Percent   := 100;
                  Percent_C := ' ';
               end if;

               -- In all other cases, accept the rounding approximation.
            when 1 .. 99 =>
               Percent   := Rounded_Percent_Value;
               Percent_C := ' ';
         end case;
      end Total_And_Value_To_Percentage;

      procedure Generate_Percent_String (Percent     : in     Percentage;
                                         Percent_C   : in     Character;
                                         Percent_Str :    out E_Strings.T)
      --# derives Percent_Str from Percent,
      --#                          Percent_C;
      is
         Percent_Part : E_Strings.T;
      begin
         --Initialise to empty string.
         Percent_Str := E_Strings.Empty_String;

         --For alingment: if percent is one digit, add two spaces.
         --             : if percent is two digits, add one spaces.
         case Percent is
            when 0 .. 9 =>
               E_Strings.Append_String (E_Str => Percent_Str,
                                        Str   => "  ");
            when 10 .. 99 =>
               E_Strings.Append_String (E_Str => Percent_Str,
                                        Str   => " ");
            when 100 =>
               null;
         end case;

         --Append the: '>','<',' ' prefix. (max length "X": 1)
         E_Strings.Append_Char (E_Str => Percent_Str,
                                Ch    => Percent_C);

         --Append the: percent number. (max length "XYYY": 4)
         E_Strings.Put_Int_To_String (Dest     => Percent_Part,
                                      Item     => Percent,
                                      Start_Pt => 1,
                                      Base     => 10);
         E_Strings.Append_Examiner_String (E_Str1 => Percent_Str,
                                           E_Str2 => E_Strings.Trim (E_Str => Percent_Part));

         --Append the: symbol '%'. (max length "XYYY%": 5)
         E_Strings.Append_Char (E_Str => Percent_Str,
                                Ch    => '%');

      end Generate_Percent_String;

      function Make_Percent_String (N_Actual, N_Total : in Natural) return E_Strings.T
      --# pre N_Total /= 0;
      is
         Percent   : Percentage;
         Size_Char : Character;  -- For the ordering relation character in >99% or <1%
         Retval    : E_Strings.T;
      begin
         Total_And_Value_To_Percentage (Overall_Total => N_Total,
                                        Value         => N_Actual,
                                        Percent       => Percent,
                                        Percent_C     => Size_Char);
         Generate_Percent_String (Percent     => Percent,
                                  Percent_C   => Size_Char,
                                  Percent_Str => Retval);
         return Retval;
      end Make_Percent_String;

   begin

      VCs_Total := Sum (The_Totals.VCs_Total);

      Percent_Undischarged_Str       := Make_Percent_String (Sum (The_Totals.VCs_Undischarged), VCs_Total);
      Percent_Proved_By_Examiner_Str := Make_Percent_String (Sum (The_Totals.VCs_Proved_By_Examiner), VCs_Total);
      Percent_Proved_By_Victor_Str   := Make_Percent_String (Sum (The_Totals.VCs_Proved_By_Victor), VCs_Total);
      Percent_Proved_By_Riposte_Str  := Make_Percent_String (Sum (The_Totals.VCs_Proved_By_Riposte), VCs_Total);
      Percent_Proved_By_Checker_Str  := Make_Percent_String (Sum (The_Totals.VCs_Proved_By_Checker), VCs_Total);
      Percent_Proved_By_Review_Str   := Make_Percent_String (Sum (The_Totals.VCs_Proved_By_Review), VCs_Total);
      Percent_Simplified_Str         := Make_Percent_String (Sum (The_Totals.VCs_Proved_By_Simplifier), VCs_Total);
      Percent_With_User_Rule_Str     := Make_Percent_String (Sum (The_Totals.VCs_Proved_With_User_Proof_Rule), VCs_Total);
      Percent_Proved_False_Str       := Make_Percent_String (Sum (The_Totals.VCs_Proved_False), VCs_Total);

   end Calculate_Percentages;

   -- Never returns from this subprogram.
   -- Null dependency relation used to avoid propagation
   -- of FatalErrors.State impacting existing clients of Total.
   -- FatalErrors.State is of little interest in this context.
   procedure Fatal_Error (Error : in FatalErrors.Error_Type)
   --# derives null from Error;
   is
      --# hide Fatal_Error;
   begin
      FatalErrors.Process (Error, E_Strings.Empty_String);
   end Fatal_Error;

   function Totals_Are_Balanced return Boolean
   --# global in The_Totals;
   is
      Total_Subprograms_Proved                             : Natural;
      Total_Subprograms_At_Least_One_False_VC              : Natural;
      Total_Subprograms_No_False_At_Least_One_Undischarged : Natural;
      Total_Subprograms                                    : Natural;
   begin
      -- Total all of the subprogram that have been fully proved.
      Total_Subprograms_Proved :=
        ((((((The_Totals.Subprograms_Proved_By_Examiner + The_Totals.Subprograms_Proved_By_Simplifier) +
               The_Totals.Subprograms_Proved_With_User_Proof_Rule) +
              The_Totals.Subprograms_Proved_By_Checker) +
             The_Totals.Subprograms_Proved_By_Review) +
            The_Totals.Subprograms_Proved_By_Victor) +
           The_Totals.Subprograms_Proved_By_Riposte);

      -- Total all of the subprogram that have at least one false vc.
      Total_Subprograms_At_Least_One_False_VC := The_Totals.Subprograms_With_ALO_False_VC;

      -- Total all of the subprogram that have no false vcs, and at least one
      -- undischarged vc.
      Total_Subprograms_No_False_At_Least_One_Undischarged := The_Totals.Subprograms_With_ALO_Undischarged_VC;

      -- Total all of the subprograms.
      Total_Subprograms :=
        ((Total_Subprograms_Proved + Total_Subprograms_At_Least_One_False_VC) +
           Total_Subprograms_No_False_At_Least_One_Undischarged);

      -- Return true if the total matches the recorded total number of Subprograms
      -- with VCs and false otherwise.
      return (Total_Subprograms = The_Totals.Subprograms_With_VCs);
   end Totals_Are_Balanced;

   procedure Update_Totals (VCG : in Boolean;
                            DPC : in Boolean)
   --# global in     VCHeap.State;
   --#        in out The_Totals;
   --# derives The_Totals from *,
   --#                         DPC,
   --#                         VCG,
   --#                         VCHeap.State;
   is
      Subprogram_Is_Undischarged                    : Boolean;
      Subprogram_Has_VC_Proved_By_Examiner          : Boolean;
      Subprogram_Has_VC_Proved_By_Simplifier        : Boolean;
      Subprogram_Has_VC_Proved_By_Contradiction     : Boolean;
      Subprogram_Has_VC_Proved_With_User_Proof_Rule : Boolean;
      Subprogram_Has_VC_Proved_By_Victor            : Boolean;
      Subprogram_Has_VC_Proved_By_Riposte           : Boolean;
      Subprogram_Has_VC_Proved_By_Checker           : Boolean;
      Subprogram_Has_VC_Proved_By_Review            : Boolean;
      Subprogram_Has_VC_Proved_False                : Boolean;
      Subprogram_Contains_Dead_Paths                : Boolean;
      More_VCs                                      : Boolean;

      Heap_Index : Heap.Atom;
      Next_Index : Heap.Atom;

      Unused_VC_Name    : E_Strings.T;
      Unused_Path_Start : E_Strings.T;
      Unused_Path_End   : E_Strings.T;
      End_Type          : VCDetails.Terminal_Point_Type;

      VC_State  : VCDetails.VC_State_T;
      DPC_State : VCDetails.DPC_State_T;

      --  Return true if there was an error analysing any of the .vcg
      --  derived files (i.e. .siv, .vct, etc.). Note that corrupted
      --  files related to ZombieScope are handeled separately.
      function Something_Is_Corrupt_In_VC return Boolean
      --# global in VCHeap.State;
      is
         Tmp : Boolean;
      begin
         for X in VCDetails.Error_Type_Corrupt_VC_Files loop
            Tmp := VCHeap.Error_Raised (Error_Kind => X);
            exit when Tmp;
         end loop;
         return Tmp;
      end Something_Is_Corrupt_In_VC;

      --  Return true if there was an error analysing any of the .dpc
      --  derived files (i.e. .sdp, etc.).
      function Something_Is_Corrupt_In_DPC return Boolean
      --# global in VCHeap.State;
      is
         Tmp : Boolean;
      begin
         for X in VCDetails.Error_Type_Corrupt_DPC_Files loop
            Tmp := VCHeap.Error_Raised (Error_Kind => X);
            exit when Tmp;
         end loop;
         return Tmp;
      end Something_Is_Corrupt_In_DPC;

   begin
      --  Initialisation.
      Subprogram_Is_Undischarged                    := False;
      Subprogram_Has_VC_Proved_By_Examiner          := False;
      Subprogram_Has_VC_Proved_By_Simplifier        := False;
      Subprogram_Has_VC_Proved_By_Contradiction     := False;
      Subprogram_Has_VC_Proved_With_User_Proof_Rule := False;
      Subprogram_Has_VC_Proved_By_Victor            := False;
      Subprogram_Has_VC_Proved_By_Riposte           := False;
      Subprogram_Has_VC_Proved_By_Checker           := False;
      Subprogram_Has_VC_Proved_By_Review            := False;
      Subprogram_Has_VC_Proved_False                := False;
      Subprogram_Contains_Dead_Paths                := False;

      --  Keep count of all the errors.
      for X in VCDetails.Error_Type loop
         if VCHeap.Error_Raised (Error_Kind => X) then
            The_Totals.Subprograms_Where_Error (X) := The_Totals.Subprograms_Where_Error (X) + 1;
         end if;
      end loop;

      --# assert True;

      --  Only perform detailed analysis of subprogram if it did not
      --  have an associated corrupt file.

      if Something_Is_Corrupt_In_VC then
         The_Totals.Subprograms_Where_VC_Analysis_Abandoned := The_Totals.Subprograms_Where_VC_Analysis_Abandoned + 1;
      end if;

      if Something_Is_Corrupt_In_DPC then
         The_Totals.Subprograms_Where_DPC_Analysis_Abandoned := The_Totals.Subprograms_Where_DPC_Analysis_Abandoned + 1;
      end if;

      --# assert True;

      --  We count VCs only if the .vcg file is not corrupt. If
      --  something else is corrupt we don't care here.

      if VCG and then not VCHeap.Error_Raised (Error_Kind => VCDetails.Corrupt_VCG_File) then
         The_Totals.Subprograms_With_VCs := The_Totals.Subprograms_With_VCs + 1;
      end if;

      if DPC and then not VCHeap.Error_Raised (Error_Kind => VCDetails.Corrupt_DPC_File) then
         The_Totals.Subprograms_With_DPCs := The_Totals.Subprograms_With_DPCs + 1;
      end if;

      --# assert True;

      More_VCs   := True;
      Heap_Index := VCHeap.First_Entry;

      while More_VCs and not Heap.IsNullPointer (Heap_Index) loop

         -- Get the details for the next VC.
         --# accept F, 10, Unused_Path_End, "Unused_Path_End unused here" &
         --#        F, 10, Unused_Path_Start, "Unused_Path_Start unused here" &
         --#        F, 10, Unused_VC_Name, "Unused_VC_Name unused here" ;
         VCHeap.Details
           (List_Index => Heap_Index,
            VC_Name    => Unused_VC_Name,
            Path_Start => Unused_Path_Start,
            Path_End   => Unused_Path_End,
            End_Type   => End_Type,
            VC_State   => VC_State,
            DPC_State  => DPC_State);
         --# end accept;

         --# assert True;

         --# accept F, 41, "Expression is stable";
         --  If we have a corrupt VCG file we don't do anything.
         if VCG and then not VCHeap.Error_Raised (Error_Kind => VCDetails.Corrupt_VCG_File) then
            --# end accept;
            The_Totals.VCs_Total (End_Type) := The_Totals.VCs_Total (End_Type) + 1;

            --# accept F, 41, "Expression is stable";
            --  We only sum up totals if we don't have anything corrupted.
            if Something_Is_Corrupt_In_VC then
               --# end accept;
               The_Totals.VCs_Undischarged (End_Type) := The_Totals.VCs_Undischarged (End_Type) + 1;
               Subprogram_Is_Undischarged             := True;
            else
               case VC_State is
                  when VCDetails.VC_False =>
                     The_Totals.VCs_Proved_False (End_Type) := The_Totals.VCs_Proved_False (End_Type) + 1;
                     Subprogram_Has_VC_Proved_False         := True;
                     Subprogram_Is_Undischarged             := True;
                  when VCDetails.VC_Proved_By_Examiner =>
                     Subprogram_Has_VC_Proved_By_Examiner         := True;
                     The_Totals.VCs_Proved_By_Examiner (End_Type) := The_Totals.VCs_Proved_By_Examiner (End_Type) + 1;
                  when VCDetails.VC_Proved_By_Inference =>
                     Subprogram_Has_VC_Proved_By_Simplifier         := True;
                     The_Totals.VCs_Proved_By_Simplifier (End_Type) := The_Totals.VCs_Proved_By_Simplifier (End_Type) + 1;
                  when VCDetails.VC_Proved_By_Contradiction =>
                     Subprogram_Has_VC_Proved_By_Contradiction      := True;
                     Subprogram_Has_VC_Proved_By_Simplifier         := True;
                     The_Totals.VCs_Proved_By_Simplifier (End_Type) := The_Totals.VCs_Proved_By_Simplifier (End_Type) + 1;
                  when VCDetails.VC_Proved_By_Checker =>
                     Subprogram_Has_VC_Proved_By_Checker         := True;
                     The_Totals.VCs_Proved_By_Checker (End_Type) := The_Totals.VCs_Proved_By_Checker (End_Type) + 1;
                  when VCDetails.VC_Proved_By_Victor =>
                     Subprogram_Has_VC_Proved_By_Victor         := True;
                     The_Totals.VCs_Proved_By_Victor (End_Type) := The_Totals.VCs_Proved_By_Victor (End_Type) + 1;
                  when VCDetails.VC_Proved_By_Riposte =>
                     Subprogram_Has_VC_Proved_By_Riposte         := True;
                     The_Totals.VCs_Proved_By_Riposte (End_Type) := The_Totals.VCs_Proved_By_Riposte (End_Type) + 1;
                  when VCDetails.VC_Proved_By_Review =>
                     Subprogram_Has_VC_Proved_By_Review         := True;
                     The_Totals.VCs_Proved_By_Review (End_Type) := The_Totals.VCs_Proved_By_Review (End_Type) + 1;
                  when VCDetails.VC_Proved_Using_User_Proof_Rules =>
                     Subprogram_Has_VC_Proved_With_User_Proof_Rule         := True;
                     Subprogram_Has_VC_Proved_By_Simplifier                := True;
                     The_Totals.VCs_Proved_With_User_Proof_Rule (End_Type) :=
                       The_Totals.VCs_Proved_With_User_Proof_Rule (End_Type) + 1;
                     The_Totals.VCs_Proved_By_Simplifier (End_Type)        := The_Totals.VCs_Proved_By_Simplifier (End_Type) + 1;
                  when VCDetails.VC_SIV_Not_Present | VCDetails.VC_Undischarged =>
                     The_Totals.VCs_Undischarged (End_Type) := The_Totals.VCs_Undischarged (End_Type) + 1;
                     Subprogram_Is_Undischarged             := True;

                  when VCDetails.VC_Not_Present =>
                     null;
               end case;
            end if;
         end if;

         --# assert True;

         --# accept F, 41, "Expression is stable";
         --  If we have a corrupt DPC file or anything related we don't do anything.
         if DPC and then not Something_Is_Corrupt_In_DPC then
            --# end accept;

            if DPC_State = VCDetails.DPC_Dead then
               -- Update the total number of subprograms containing
               -- dead paths.
               if not Subprogram_Contains_Dead_Paths then
                  The_Totals.Subprograms_With_Dead_Paths := The_Totals.Subprograms_With_Dead_Paths + 1;
               end if;
               Subprogram_Contains_Dead_Paths := True;
               -- Update the total number of dead paths found.
               The_Totals.Number_Of_Dead_Paths := The_Totals.Number_Of_Dead_Paths + 1;
            end if;

         end if;

         --# assert True;

         VCHeap.Next (After_This => Heap_Index,
                      Success    => More_VCs,
                      Next_One   => Next_Index);

         Heap_Index := Next_Index;

      end loop;

      --# assert True;

      --  Update the 'At Least One' counts.
      if Subprogram_Is_Undischarged then
         if Subprogram_Has_VC_Proved_False then
            The_Totals.Subprograms_With_ALO_False_VC := The_Totals.Subprograms_With_ALO_False_VC + 1;
         else
            The_Totals.Subprograms_With_ALO_Undischarged_VC := The_Totals.Subprograms_With_ALO_Undischarged_VC + 1;
         end if;
      end if;

      --# assert True;

      if Subprogram_Has_VC_Proved_By_Examiner then
         The_Totals.Subprograms_With_ALO_Examiner_VC := The_Totals.Subprograms_With_ALO_Examiner_VC + 1;
      end if;

      --# assert True;

      if Subprogram_Has_VC_Proved_By_Simplifier then
         The_Totals.Subprograms_With_ALO_Simplifier_VC := The_Totals.Subprograms_With_ALO_Simplifier_VC + 1;
      end if;

      --# assert True;

      if Subprogram_Has_VC_Proved_By_Contradiction then
         The_Totals.Subprograms_With_ALO_Contradiction_VC := The_Totals.Subprograms_With_ALO_Contradiction_VC + 1;
      end if;

      --# assert True;

      if Subprogram_Has_VC_Proved_With_User_Proof_Rule then
         The_Totals.Subprograms_With_ALO_User_Rule_VC := The_Totals.Subprograms_With_ALO_User_Rule_VC + 1;
      end if;

      --# assert True;

      if Subprogram_Has_VC_Proved_By_Victor then
         The_Totals.Subprograms_With_ALO_Victor_VC := The_Totals.Subprograms_With_ALO_Victor_VC + 1;
      end if;

      --# assert True;

      if Subprogram_Has_VC_Proved_By_Riposte then
         The_Totals.Subprograms_With_ALO_Riposte_VC := The_Totals.Subprograms_With_ALO_Riposte_VC + 1;
      end if;

      --# assert True;

      if Subprogram_Has_VC_Proved_By_Checker then
         The_Totals.Subprograms_With_ALO_Checker_VC := The_Totals.Subprograms_With_ALO_Checker_VC + 1;
      end if;

      --# assert True;

      if Subprogram_Has_VC_Proved_By_Review then
         The_Totals.Subprograms_With_ALO_Review_VC := The_Totals.Subprograms_With_ALO_Review_VC + 1;
      end if;

      --# assert True;

      --  Update the proof strategy use hierarchy (See declaration of Total_Type)
      --  Examiner -> Simplifier -> User Rules -> ViCToR -> Checker -> Review
      if not Subprogram_Is_Undischarged then
         if Subprogram_Has_VC_Proved_By_Review then
            The_Totals.Subprograms_Proved_By_Review := The_Totals.Subprograms_Proved_By_Review + 1;

         elsif Subprogram_Has_VC_Proved_By_Checker then
            The_Totals.Subprograms_Proved_By_Checker := The_Totals.Subprograms_Proved_By_Checker + 1;

         elsif Subprogram_Has_VC_Proved_By_Victor then
            The_Totals.Subprograms_Proved_By_Victor := The_Totals.Subprograms_Proved_By_Victor + 1;

         elsif Subprogram_Has_VC_Proved_By_Riposte then
            The_Totals.Subprograms_Proved_By_Riposte := The_Totals.Subprograms_Proved_By_Riposte + 1;

         elsif Subprogram_Has_VC_Proved_With_User_Proof_Rule then
            The_Totals.Subprograms_Proved_With_User_Proof_Rule := The_Totals.Subprograms_Proved_With_User_Proof_Rule + 1;

         elsif Subprogram_Has_VC_Proved_By_Simplifier then
            The_Totals.Subprograms_Proved_By_Simplifier := The_Totals.Subprograms_Proved_By_Simplifier + 1;

         elsif Subprogram_Has_VC_Proved_By_Examiner then
            The_Totals.Subprograms_Proved_By_Examiner := The_Totals.Subprograms_Proved_By_Examiner + 1;
         end if;
      end if;

      --# assert True;

      --# accept F, 33, Unused_Path_End, "Unused_Path_End unused here" &
      --#        F, 33, Unused_Path_Start, "Unused_Path_Start unused here" &
      --#        F, 33, Unused_VC_Name, "Unused_VC_Name unused here";
   end Update_Totals;

   procedure Output
     (Report_File             : in     SPARK_IO.File_Type;
      Temp_File               : in out SPARK_IO.File_Type;
      Temp_False_File         : in out SPARK_IO.File_Type;
      Temp_Contra_File        : in out SPARK_IO.File_Type;
      Temp_Victor_File        : in out SPARK_IO.File_Type;
      Temp_Riposte_File       : in out SPARK_IO.File_Type;
      Temp_User_File          : in out SPARK_IO.File_Type;
      Temp_Rlu_Error_File     : in out SPARK_IO.File_Type;
      Temp_Rlu_Used_File      : in out SPARK_IO.File_Type;
      Temp_PR_Verr_File       : in out SPARK_IO.File_Type;
      Temp_Warn_Error_File    : in out SPARK_IO.File_Type;
      Temp_SDP_Error_File     : in out SPARK_IO.File_Type;
      Temp_DPC_Error_File     : in out SPARK_IO.File_Type;
      Temp_Victor_Error_File  : in out SPARK_IO.File_Type;
      Temp_Riposte_Error_File : in out SPARK_IO.File_Type)
   --# global in     CommandLine.Data;
   --#        in     The_Totals;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys       from *,
   --#                                      CommandLine.Data,
   --#                                      Report_File,
   --#                                      Temp_Contra_File,
   --#                                      Temp_DPC_Error_File,
   --#                                      Temp_False_File,
   --#                                      Temp_File,
   --#                                      Temp_PR_Verr_File,
   --#                                      Temp_Riposte_Error_File,
   --#                                      Temp_Riposte_File,
   --#                                      Temp_Rlu_Error_File,
   --#                                      Temp_Rlu_Used_File,
   --#                                      Temp_SDP_Error_File,
   --#                                      Temp_User_File,
   --#                                      Temp_Victor_Error_File,
   --#                                      Temp_Victor_File,
   --#                                      Temp_Warn_Error_File,
   --#                                      The_Totals &
   --#         Temp_Contra_File,
   --#         Temp_DPC_Error_File,
   --#         Temp_False_File,
   --#         Temp_File,
   --#         Temp_PR_Verr_File,
   --#         Temp_Riposte_Error_File,
   --#         Temp_Riposte_File,
   --#         Temp_Rlu_Error_File,
   --#         Temp_Rlu_Used_File,
   --#         Temp_SDP_Error_File,
   --#         Temp_User_File,
   --#         Temp_Victor_Error_File,
   --#         Temp_Victor_File,
   --#         Temp_Warn_Error_File    from *;
   is
      Percent_Undischarged_Str       : E_Strings.T;
      Percent_Proved_By_Examiner_Str : E_Strings.T;
      Percent_Proved_By_Victor_Str   : E_Strings.T;
      Percent_Proved_By_Riposte_Str  : E_Strings.T;
      Percent_Proved_By_Checker_Str  : E_Strings.T;
      Percent_Proved_By_Review_Str   : E_Strings.T;
      Percent_Simplified_Str         : E_Strings.T;
      Percent_With_User_Rule_Str     : E_Strings.T;
      Percent_Proved_False_Str       : E_Strings.T;

      Total_Subprograms_Proved : Natural;

      subtype Valid_Column_Size is Integer range 4 .. Integer'Last;

      Name_Column_Width : constant Valid_Column_Size := 14;
      Column_Width      : constant Valid_Column_Size := 11;

      subtype Rowname_String_Positions_T is E_Strings.Positions range E_Strings.Positions'First .. Name_Column_Width;
      subtype Colname_String_Positions_T is E_Strings.Positions range E_Strings.Positions'First .. Column_Width;

      subtype Table_Rowname_String_T is String (Rowname_String_Positions_T);
      subtype Table_Colname_String_T is String (Colname_String_Positions_T);

      -- Don't count the 0th column, only the data columns
      type Table_Column_Index is range 1 .. 10;

      type Table_Column_T is record
         Name     : Table_Colname_String_T;
         Width    : Valid_Column_Size;
         Brackets : Boolean;
      end record;

      type Table_Row_T is record
         Name         : Table_Rowname_String_T;
         Nonzero_Only : Boolean;
      end record;

      type Table_Format_T is array (Table_Column_Index) of Table_Column_T;
      type Table_Row_Format_T is array (VCDetails.Terminal_Point_Type) of Table_Row_T;
      type Table_Column_Enabled_T is array (Table_Column_Index) of Boolean;

      --  Rationale for the widths: Total, Examiner and Simplifier
      --  will have big numbers (think iFACTS). The other colums
      --  should be much smaller; except maybe the Undischarged column
      --  as that is what you get from a pogs run on an unsimplified
      --  tree.
      Table_Format : constant Table_Format_T :=
        Table_Format_T'
        (1  => Table_Column_T'("Total      ", Column_Width, False),
         2  => Table_Column_T'("Examiner   ", Column_Width, False),
         3  => Table_Column_T'("Simplifier ", Column_Width, False),
         4  => Table_Column_T'("(User)     ", 7, True),
         5  => Table_Column_T'("Victor     ", 7, False),
         6  => Table_Column_T'("Riposte    ", 8, False),
         7  => Table_Column_T'("Checker    ", 8, False),
         8  => Table_Column_T'("Review     ", 7, False),
         9  => Table_Column_T'("False      ", 6, False),
         10 => Table_Column_T'("Undisc.    ", Column_Width, False));

      Table_Column_Enabled : Table_Column_Enabled_T;

      Table_Row_Format : constant Table_Row_Format_T :=
        Table_Row_Format_T'
        (VCDetails.Assert_Point             => Table_Row_T'("Assert/Post   ", False),
         VCDetails.Precondition_Check_Point => Table_Row_T'("Precondition  ", False),
         VCDetails.Check_Statement_Point    => Table_Row_T'("Check stmnt.  ", False),
         VCDetails.Runtime_Check_Point      => Table_Row_T'("Runtime check ", False),
         VCDetails.Refinement_VC_Point      => Table_Row_T'("Refinem. VCs  ", False),
         VCDetails.Inheritance_VC_Point     => Table_Row_T'("Inherit. VCs  ", False),
         VCDetails.Undetermined_Point       => Table_Row_T'("Undetermined  ", True));

      Overall_Errors   : Boolean := False;
      Overall_Warnings : Boolean := False;

      function Align_Right (E_Str : E_Strings.T;
                            Width : E_Strings.Lengths) return E_Strings.T is
         Retval : E_Strings.T;
      begin
         Retval := E_Strings.Empty_String;
         if E_Strings.Get_Length (E_Str) < Width then
            for I in E_Strings.Lengths range E_Strings.Get_Length (E_Str) + 1 .. Width loop
               E_Strings.Append_Char (Retval, ' ');
            end loop;
         end if;
         E_Strings.Append_Examiner_String (Retval, E_Str);
         return Retval;
      end Align_Right;

      function Align_Left (E_Str : E_Strings.T;
                           Width : E_Strings.Lengths) return E_Strings.T is
         Retval : E_Strings.T;
      begin
         Retval := E_Str;
         if E_Strings.Get_Length (E_Str) < Width then
            for I in E_Strings.Lengths range E_Strings.Get_Length (E_Str) + 1 .. Width loop
               E_Strings.Append_Char (Retval, ' ');
            end loop;
         end if;
         return Retval;
      end Align_Left;

      --  This procedure prints a table row containing integers. If
      --  Show_Warn_Tag is specified, it will also print the '<<<'
      --  look-out tag at the end of the row if there are any
      --  undischarged or false VCs.
      procedure Print_Table_Row
        (Title                                                                                                  : in String;
         The_Total, Examiner, Simplifier, User_Rules, Victor, Riposte, Checker, Review, False_VCs, Undischarged : in Integer;
         Show_Warn_Tag                                                                                          : in Boolean)
      --# global in     Report_File;
      --#        in     Table_Column_Enabled;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Checker,
      --#                                Examiner,
      --#                                False_VCs,
      --#                                Report_File,
      --#                                Review,
      --#                                Riposte,
      --#                                Show_Warn_Tag,
      --#                                Simplifier,
      --#                                Table_Column_Enabled,
      --#                                The_Total,
      --#                                Title,
      --#                                Undischarged,
      --#                                User_Rules,
      --#                                Victor;
      is
         Value : Integer;
      begin
         --  Row name.
         E_Strings.Put_String (Report_File, Align_Left (E_Strings.Copy_String (Title), Name_Column_Width));

         --  Other columns.
         for I in Table_Column_Index loop
            if Table_Column_Enabled (I) then
               case I is
                  when 1 =>
                     Value := The_Total;
                  when 2 =>
                     Value := Examiner;
                  when 3 =>
                     Value := Simplifier;
                  when 4 =>
                     Value := User_Rules;
                  when 5 =>
                     Value := Victor;
                  when 6 =>
                     Value := Riposte;
                  when 7 =>
                     Value := Checker;
                  when 8 =>
                     Value := Review;
                  when 9 =>
                     Value := False_VCs;
                  when 10 =>
                     Value := Undischarged;
               end case;
               if Table_Format (I).Brackets then
                  if Value > 0 then
                     SPARK_IO.Put_Char (Report_File, '(');
                     SPARK_IO.Put_Integer (Report_File, Value, Table_Format (I).Width - 2, 10);
                     SPARK_IO.Put_Char (Report_File, ')');
                  else
                     E_Strings.Put_String (Report_File, Align_Left (E_Strings.Empty_String, Table_Format (I).Width));
                  end if;
               else
                  SPARK_IO.Put_Integer (Report_File, Value, Table_Format (I).Width, 10);
               end if;
            end if;
         end loop;

         --  Print the 'look-out' tag, if necessary.
         if Show_Warn_Tag and (Undischarged > 0 or False_VCs > 0) then
            SPARK_IO.Put_String (Report_File, " <<<", 0);
         end if;

         --  Final EOL.
         SPARK_IO.New_Line (Report_File, 1);
      end Print_Table_Row;

      --  This procedure prints a table row containing strings.
      procedure Print_Table_String_Row
        (Title                                                                                                  : in String;
         The_Total, Examiner, Simplifier, User_Rules, Victor, Riposte, Checker, Review, False_VCs, Undischarged : in E_Strings.T)
      --# global in     Report_File;
      --#        in     Table_Column_Enabled;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Checker,
      --#                                Examiner,
      --#                                False_VCs,
      --#                                Report_File,
      --#                                Review,
      --#                                Riposte,
      --#                                Simplifier,
      --#                                Table_Column_Enabled,
      --#                                The_Total,
      --#                                Title,
      --#                                Undischarged,
      --#                                User_Rules,
      --#                                Victor;
      is
         Value : E_Strings.T;
      begin
         --  Row name.
         E_Strings.Put_String (Report_File, Align_Left (E_Strings.Copy_String (Title), Name_Column_Width));

         --  Other columns.
         for I in Table_Column_Index loop
            if Table_Column_Enabled (I) then
               case I is
                  when 1 =>
                     Value := The_Total;
                  when 2 =>
                     Value := Examiner;
                  when 3 =>
                     Value := Simplifier;
                  when 4 =>
                     Value := User_Rules;
                  when 5 =>
                     Value := Victor;
                  when 6 =>
                     Value := Riposte;
                  when 7 =>
                     Value := Checker;
                  when 8 =>
                     Value := Review;
                  when 9 =>
                     Value := False_VCs;
                  when 10 =>
                     Value := Undischarged;
               end case;
               if Table_Format (I).Brackets then
                  if not E_Strings.Is_Empty (Value) then
                     SPARK_IO.Put_Char (Report_File, '(');
                     E_Strings.Put_String (Report_File, Align_Right (Value, Table_Format (I).Width - 2));
                     SPARK_IO.Put_Char (Report_File, ')');
                  else
                     E_Strings.Put_String (Report_File, Align_Left (E_Strings.Empty_String, Table_Format (I).Width));
                  end if;
               else
                  E_Strings.Put_String (Report_File, Align_Right (Value, Table_Format (I).Width));
               end if;
            end if;
         end loop;

         --  Final EOL.
         SPARK_IO.New_Line (Report_File, 1);
      end Print_Table_String_Row;

      --  This procedure prints the table column names.
      procedure Print_Table_Head
      --# global in     Report_File;
      --#        in     Table_Column_Enabled;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Report_File,
      --#                                Table_Column_Enabled;
      is
         Tmp : E_Strings.T;
      begin
         -- Skip the 'row name' column
         for I in Integer range 1 .. Name_Column_Width loop
            SPARK_IO.Put_Char (Report_File, ' ');
         end loop;

         -- Other columns
         for I in Table_Column_Index loop
            if Table_Column_Enabled (I) then
               Tmp :=
                 E_Strings.Trim
                 (E_Strings.Section
                    (E_Str     => E_Strings.Copy_String (Table_Format (I).Name),
                     Start_Pos => E_Strings.Positions'First,
                     Length    => Table_Format (I).Width));
               E_Strings.Put_String (Report_File, Align_Right (Tmp, Table_Format (I).Width));
            end if;
         end loop;

         -- Final EOL
         SPARK_IO.New_Line (Report_File, 1);
      end Print_Table_Head;

      procedure Print_Table_Separator
      --# global in     Report_File;
      --#        in     Table_Column_Enabled;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Report_File,
      --#                                Table_Column_Enabled;
      is
      begin
         -- Fill the 'name' column
         for I in Integer range 1 .. Name_Column_Width loop
            SPARK_IO.Put_Char (Report_File, '=');
         end loop;

         -- Other columns
         for I in Table_Column_Index loop
            if Table_Column_Enabled (I) then
               for J in Integer range 1 .. Table_Format (I).Width loop
                  SPARK_IO.Put_Char (Report_File, '=');
               end loop;
            end if;
         end loop;

         -- Final EOL
         SPARK_IO.New_Line (Report_File, 1);
      end Print_Table_Separator;

      procedure Print_Final_Summary
      --# global in     Overall_Errors;
      --#        in     Overall_Warnings;
      --#        in     The_Totals;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Overall_Errors,
      --#                                Overall_Warnings,
      --#                                The_Totals;
      is
         Total_VCs  : Natural;
         False_VCs  : Natural;
         Undisc_VCs : Natural;
      begin
         Total_VCs  := Sum (The_Totals.VCs_Total);
         False_VCs  := Sum (The_Totals.VCs_Proved_False);
         Undisc_VCs := Sum (The_Totals.VCs_Undischarged);

         SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "----- BEGIN PROOF SUMMARY -----", 0);

         SPARK_IO.Put_String (SPARK_IO.Standard_Output, "VCs discharged:   ", 0);
         SPARK_IO.Put_Integer (SPARK_IO.Standard_Output, Total_VCs - (False_VCs + Undisc_VCs), 8, 10);
         SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);

         SPARK_IO.Put_String (SPARK_IO.Standard_Output, "VCs false:        ", 0);
         SPARK_IO.Put_Integer (SPARK_IO.Standard_Output, False_VCs, 8, 10);
         SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);

         SPARK_IO.Put_String (SPARK_IO.Standard_Output, "VCs undischarged: ", 0);
         SPARK_IO.Put_Integer (SPARK_IO.Standard_Output, Undisc_VCs, 8, 10);
         SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);

         SPARK_IO.Put_String (SPARK_IO.Standard_Output, "Warnings: ", 0);
         if Overall_Warnings then
            SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "YES", 0);
         else
            SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "No", 0);
         end if;

         SPARK_IO.Put_String (SPARK_IO.Standard_Output, "Errors:   ", 0);
         if Overall_Errors then
            SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "YES", 0);
         else
            SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "No", 0);
         end if;

         SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "----- END PROOF SUMMARY -----", 0);

      end Print_Final_Summary;

      --  The purpose of this procedure is to read back one of the
      --  various temporary files created and produce a simple
      --  listing.
      --  There are two main file formats, one with number of VCs and
      --  one without. The Has_Numbers parameter indicates which one
      --  to expect.
      procedure Regurgitate_Temp_File
        (The_Temp_File : in out SPARK_IO.File_Type;
         The_String_1  : in     String;
         The_String_2  : in     String;
         Has_Numbers   : in     Boolean)
      --# global in     Report_File;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Has_Numbers,
      --#                                Report_File,
      --#                                The_String_1,
      --#                                The_String_2,
      --#                                The_Temp_File &
      --#         The_Temp_File     from *;
      is
         Temp_Store_Int    : Integer;
         Temp_Store_String : E_Strings.T;
         Temp_Store_Bool   : Boolean;
         Temp_Status       : SPARK_IO.File_Status;
      begin
         --# accept F, 10, Temp_Status, "Temp_Status not used here" &
         --#        F, 10, Temp_Store_Bool, "Temp_Store_Bool not used here";
         SPARK_IO.Reset (The_Temp_File, SPARK_IO.In_File, Temp_Status);
         if not SPARK_IO.End_Of_File (The_Temp_File) then
            SPARK_IO.Put_Line (Report_File, The_String_1, 0);
            if The_String_2 /= "" then
               SPARK_IO.Put_Line (Report_File, The_String_2, 0);
            end if;
            SPARK_IO.New_Line (Report_File, 1);
            while not SPARK_IO.End_Of_File (The_Temp_File) loop
               --# accept F, 41, "No need to write two loops here.";
               if Has_Numbers then
                  SPARK_IO.Get_Integer (The_Temp_File, Temp_Store_Int, 4, Temp_Store_Bool);
                  SPARK_IO.Put_Integer (Report_File, Temp_Store_Int, 4, 10);
                  SPARK_IO.Put_String (Report_File, "  ", 0);
               end if;
               E_Strings.Get_Line (File  => The_Temp_File,
                                   E_Str => Temp_Store_String);
               if Has_Numbers or E_Strings.Get_Length (Temp_Store_String) > 0 then
                  if not Has_Numbers then
                     SPARK_IO.Put_String (Report_File, "    ", 0);
                  end if;
                  E_Strings.Put_String (File  => Report_File,
                                        E_Str => Temp_Store_String);
                  SPARK_IO.New_Line (Report_File, 1);
               end if;
               --# end accept;
            end loop;
            SPARK_IO.New_Line (Report_File, 1);
         end if;
         --# accept F, 33, Temp_Store_Bool, "Temp_Store_Bool is not needed." &
         --#        F, 33, Temp_Status, "Temp_Status is not needed.";
      end Regurgitate_Temp_File;

   begin
      SPARK_IO.Put_Line (Report_File, Banner.MajorSeparatorLine, 0);
      SPARK_IO.Put_Line (Report_File, "Summary:", 0);
      SPARK_IO.New_Line (Report_File, 1);

      --  We want to print the file summaries in roughly two blocks:
      --  Warnings/Notes and actual errors. First, the warnings and
      --  non-critical errors:

      -- print out any used user-defined rule files
      Regurgitate_Temp_File
        (The_Temp_File => Temp_Rlu_Used_File,
         The_String_1  => "The following user-defined rule files have been used:",
         The_String_2  => "",
         Has_Numbers   => False);

      -- print out the file names and numbers of any VC proved by a user-defined proof rule
      Regurgitate_Temp_File
        (The_Temp_File => Temp_User_File,
         The_String_1  => "The following subprograms have VCs proved using a user-defined proof rule:",
         The_String_2  => "",
         Has_Numbers   => True);

      -- print out the file names and numbers of any VC proved by contradiction
      Regurgitate_Temp_File
        (The_Temp_File => Temp_Contra_File,
         The_String_1  => "The following subprograms have VCs proved by contradiction:",
         The_String_2  => "",
         Has_Numbers   => True);

      -- print out the file names and numbers of any VC proved by ViCToR
      Regurgitate_Temp_File
        (The_Temp_File => Temp_Victor_File,
         The_String_1  => "The following subprograms have VCs proved by Victor:",
         The_String_2  => "",
         Has_Numbers   => True);

      -- print out the file names and numbers of any VC proved by Riposte
      Regurgitate_Temp_File
        (The_Temp_File => Temp_Riposte_File,
         The_String_1  => "The following subprograms have VCs proved by Riposte:",
         The_String_2  => "",
         Has_Numbers   => True);

      -- print out the names of any missing SDP files
      Regurgitate_Temp_File
        (The_Temp_File => Temp_SDP_Error_File,
         The_String_1  => "***WARNING: The following DPC files have not been ZombieScoped:",
         The_String_2  => "",
         Has_Numbers   => False);

      -- print out the names of any missing DPC files
      Regurgitate_Temp_File
        (The_Temp_File => Temp_DPC_Error_File,
         The_String_1  => "***WARNING: The following DPC files are missing:",
         The_String_2  => "",
         Has_Numbers   => False);

      --  Secondly, we print the actual errors (those indicating that
      --  your code is definitely wrong):

      -- print out the names of files containing warnings or errors
      Regurgitate_Temp_File
        (The_Temp_File => Temp_Warn_Error_File,
         The_String_1  => "***WARNING: The following files, or their absence, raised warnings or errors:",
         The_String_2  => "",
         Has_Numbers   => True);

      -- print out the names of any user rule files containing syntax errors
      Regurgitate_Temp_File
        (The_Temp_File => Temp_Rlu_Error_File,
         The_String_1  => "***WARNING: The following user defined rule files contain syntax errors:",
         The_String_2  => "",
         Has_Numbers   => False);

      -- print out the file names and numbers of any false VC
      Regurgitate_Temp_File
        (The_Temp_File => Temp_False_File,
         The_String_1  => "The following subprograms have VCs proved false:",
         The_String_2  => "",
         Has_Numbers   => True);

      -- print out the file names and numbers of any undischarged VC (excluding those proved false)
      Regurgitate_Temp_File
        (The_Temp_File => Temp_File,
         The_String_1  => "The following subprograms have undischarged VCs (excluding those proved false):",
         The_String_2  => "",
         Has_Numbers   => True);

      -- print out the file names and numbers of any files with review errors
      Regurgitate_Temp_File
        (The_Temp_File => Temp_PR_Verr_File,
         The_String_1  => "***WARNING: The PRV file(s) associated with the following subprograms may be out of date",
         The_String_2  => "The following subprograms have review files containing VCs already proved elsewhere:",
         Has_Numbers   => True);

      -- print out all victor errors
      Regurgitate_Temp_File
        (The_Temp_File => Temp_Victor_Error_File,
         The_String_1  => "***WARNING: Please note the following warnings and/or errors surrounding victor files:",
         The_String_2  => "",
         Has_Numbers   => False);

      -- print out all Riposte errors
      Regurgitate_Temp_File
        (The_Temp_File => Temp_Riposte_Error_File,
         The_String_1  => "***WARNING: Please note the following warnings and/or errors surrounding Riposte files:",
         The_String_2  => "",
         Has_Numbers   => False);

      --# assert True;

      -- Print a summary of the number of subprograms conatining at
      -- least one instance of the following:
      SPARK_IO.Put_Line (Report_File, "Proof strategies used by subprograms", 0);
      SPARK_IO.Put_Line (Report_File, "-------------------------------------------------------------------------", 0);
      SPARK_IO.Put_String (Report_File, "Total subprograms with at least one VC proved by examiner:           ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_ALO_Examiner_VC, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with at least one VC proved by simplifier:         ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_ALO_Simplifier_VC, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with at least one VC proved by contradiction:      ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_ALO_Contradiction_VC, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with at least one VC proved with user proof rule:  ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_ALO_User_Rule_VC, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with at least one VC proved by Victor:             ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_ALO_Victor_VC, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with at least one VC proved by Riposte:            ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_ALO_Riposte_VC, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with at least one VC proved using checker:         ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_ALO_Checker_VC, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with at least one VC discharged by review:         ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_ALO_Review_VC, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      --# assert True;

      -- Print out hierarchy of proof strategy use (see declaration of Total_Type)
      --  Examiner -> Simplifier -> User Rules -> ViCToR -> Checker -> Review
      SPARK_IO.New_Line (Report_File, 1);
      SPARK_IO.Put_Line (Report_File, "Maximum extent of strategies used for fully proved subprograms:", 0);
      SPARK_IO.Put_Line (Report_File, "-------------------------------------------------------------------------", 0);
      SPARK_IO.Put_String (Report_File, "Total subprograms with proof completed by examiner:                  ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Proved_By_Examiner, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with proof completed by simplifier:                ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Proved_By_Simplifier, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with proof completed with user defined rules:      ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Proved_With_User_Proof_Rule, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with proof completed by Victor:                    ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Proved_By_Victor, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with proof completed by Riposte:                   ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Proved_By_Riposte, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with proof completed by checker:                   ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Proved_By_Checker, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with VCs discharged by review:                     ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Proved_By_Review, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      -- BUG: This could, in theory, overflow.
      Total_Subprograms_Proved :=
        ((((((The_Totals.Subprograms_Proved_By_Examiner + The_Totals.Subprograms_Proved_By_Simplifier) +
               The_Totals.Subprograms_Proved_With_User_Proof_Rule) +
              The_Totals.Subprograms_Proved_By_Checker) +
             The_Totals.Subprograms_Proved_By_Review) +
            The_Totals.Subprograms_Proved_By_Victor) +
           The_Totals.Subprograms_Proved_By_Riposte);

      --# assert Total_Subprograms_Proved =
      --#   The_Totals.Subprograms_Proved_By_Examiner +
      --#   The_Totals.Subprograms_Proved_By_Simplifier +
      --#   The_Totals.Subprograms_Proved_With_User_Proof_Rule +
      --#   The_Totals.Subprograms_Proved_By_Checker +
      --#   The_Totals.Subprograms_Proved_By_Review +
      --#   The_Totals.Subprograms_Proved_By_Victor +
      --#   The_Totals.Subprograms_Proved_By_Riposte;

      SPARK_IO.New_Line (Report_File, 1);
      SPARK_IO.Put_Line (Report_File, "Overall subprogram summary:", 0);
      SPARK_IO.Put_Line (Report_File, "-------------------------------------------------------------------------", 0);
      SPARK_IO.Put_String (Report_File, "Total subprograms fully proved:                                      ", 0);
      SPARK_IO.Put_Integer (Report_File, Total_Subprograms_Proved, 4, 10);
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with at least one undischarged VC:                 ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_ALO_Undischarged_VC, 4, 10);

      if The_Totals.Subprograms_With_ALO_Undischarged_VC > 0 then
         SPARK_IO.Put_String (Report_File, "  <<<", 0);
      end if;
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "Total subprograms with at least one false VC:                        ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_ALO_False_VC, 4, 10);

      if The_Totals.Subprograms_With_ALO_False_VC > 0 then
         SPARK_IO.Put_String (Report_File, "  <<<", 0);
      end if;
      SPARK_IO.New_Line (Report_File, 1);

      SPARK_IO.Put_String (Report_File, "                                                                    -----", 0);

      SPARK_IO.New_Line (Report_File, 1);
      SPARK_IO.Put_String (Report_File, "Total subprograms for which VCs have been generated:                 ", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_VCs, 4, 10);
      SPARK_IO.New_Line (Report_File, 2);

      --# assert Total_Subprograms_Proved =
      --#   The_Totals.Subprograms_Proved_By_Examiner +
      --#   The_Totals.Subprograms_Proved_By_Simplifier +
      --#   The_Totals.Subprograms_Proved_With_User_Proof_Rule +
      --#   The_Totals.Subprograms_Proved_By_Checker +
      --#   The_Totals.Subprograms_Proved_By_Review +
      --#   The_Totals.Subprograms_Proved_By_Victor +
      --#   The_Totals.Subprograms_Proved_By_Riposte;

      -- Only report errors if there are some.
      if The_Totals.Subprograms_Where_VC_Analysis_Abandoned > 0
        or else The_Totals.Subprograms_Where_DPC_Analysis_Abandoned > 0
        or else The_Totals.Subprograms_Where_Error (VCDetails.Missing_SLG_File) > 0
        or else The_Totals.Subprograms_Where_Error (VCDetails.Missing_VLG_File) > 0 then
         SPARK_IO.Put_Line (Report_File, "WARNING: Overall error summary:", 0);
         SPARK_IO.Put_Line (Report_File, "-------------------------------------------------------------------------", 0);
         SPARK_IO.Put_String (Report_File, "Total simplified subprograms with missing slg file:               ", 0);
         SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Where_Error (VCDetails.Missing_SLG_File), 7, 10);
         SPARK_IO.New_Line (Report_File, 1);
         SPARK_IO.Put_String (Report_File, "Total victored subprograms with missing vlg file:                 ", 0);
         SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Where_Error (VCDetails.Missing_VLG_File), 7, 10);
         SPARK_IO.New_Line (Report_File, 1);
         SPARK_IO.Put_String (Report_File, "Total subprograms where VC analysis was abandoned due to errors:     ", 0);
         SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Where_VC_Analysis_Abandoned, 4, 10);
         SPARK_IO.New_Line (Report_File, 1);
         SPARK_IO.Put_String (Report_File, "Total subprograms where DPC analysis was abandoned due to errors:     ", 0);
         SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Where_DPC_Analysis_Abandoned, 3, 10);
         SPARK_IO.New_Line (Report_File, 2);

         Overall_Errors := True;
      else
         -- One blank line between each table in this group, but double blank line
         -- after the last table.
         SPARK_IO.New_Line (Report_File, 1);
      end if;

      --  The sum of the subprograms fully proved,
      --  the subprograms with at least undischarged VC and
      --  the subprograms with at least 1 false VC must equal
      --  the number of subprograms for which VCs have been generated.

      SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);

      --# assert Total_Subprograms_Proved =
      --#   The_Totals.Subprograms_Proved_By_Examiner +
      --#   The_Totals.Subprograms_Proved_By_Simplifier +
      --#   The_Totals.Subprograms_Proved_With_User_Proof_Rule +
      --#   The_Totals.Subprograms_Proved_By_Checker +
      --#   The_Totals.Subprograms_Proved_By_Review +
      --#   The_Totals.Subprograms_Proved_By_Victor +
      --#   The_Totals.Subprograms_Proved_By_Riposte;

      -- Check the totals are balanced.
      if not Totals_Are_Balanced then
         Fatal_Error (Error => FatalErrors.Subprogram_Totals_Inconsistent);
      end if;

      --# assert True;

      SPARK_IO.Put_Line (Report_File, "ZombieScope Summary:", 0);
      SPARK_IO.Put_Line (Report_File, "-------------------------------------------------------------------------", 0);
      SPARK_IO.Put_String (Report_File, "Total subprograms for which DPCs have been generated:", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_DPCs, 20, 10);
      SPARK_IO.New_Line (Report_File, 1);
      SPARK_IO.Put_String (Report_File, "Total number subprograms with dead paths found:", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_With_Dead_Paths, 26, 10);
      SPARK_IO.New_Line (Report_File, 1);
      SPARK_IO.Put_String (Report_File, "Total number of dead paths found:", 0);
      SPARK_IO.Put_Integer (Report_File, The_Totals.Number_Of_Dead_Paths, 40, 10);
      SPARK_IO.New_Line (Report_File, 3);

      -- Issue warning message if some DPC files have not been analysed.

      --# assert True;

      SPARK_IO.Put_Line (Report_File, "VC summary:", 0);
      SPARK_IO.Put_Line (Report_File, "-------------------------------------------------------------------------", 0);
      SPARK_IO.Put_Line (Report_File, "Note: (User) denotes where the Simplifier has proved VCs using one or", 0);
      SPARK_IO.Put_Line (Report_File, "      more user-defined proof rules.", 0);

      SPARK_IO.New_Line (Report_File, 1);

      Table_Column_Enabled :=
        Table_Column_Enabled_T'
        (1  => True,
         2  => Sum (The_Totals.VCs_Proved_By_Examiner) > 0,
         3  => Sum (The_Totals.VCs_Proved_By_Simplifier) > 0,
         4  => Sum (The_Totals.VCs_Proved_With_User_Proof_Rule) > 0,
         5  => Sum (The_Totals.VCs_Proved_By_Victor) > 0,
         6  => Sum (The_Totals.VCs_Proved_By_Riposte) > 0,
         7  => Sum (The_Totals.VCs_Proved_By_Checker) > 0,
         8  => Sum (The_Totals.VCs_Proved_By_Review) > 0,
         9  => Sum (The_Totals.VCs_Proved_False) > 0,
         10 => Sum (The_Totals.VCs_Undischarged) > 0);

      SPARK_IO.Put_Line (Report_File, "Total VCs by type:", 0);
      SPARK_IO.Put_Line (Report_File, "------------------", 0);

      Print_Table_Head;

      for R in VCDetails.Terminal_Point_Type loop
         if not Table_Row_Format (R).Nonzero_Only or The_Totals.VCs_Total (R) > 0 then
            Print_Table_Row
              (Title         => Table_Row_Format (R).Name,
               The_Total     => The_Totals.VCs_Total (R),
               Examiner      => The_Totals.VCs_Proved_By_Examiner (R),
               Simplifier    => The_Totals.VCs_Proved_By_Simplifier (R),
               User_Rules    => The_Totals.VCs_Proved_With_User_Proof_Rule (R),
               Victor        => The_Totals.VCs_Proved_By_Victor (R),
               Riposte       => The_Totals.VCs_Proved_By_Riposte (R),
               Checker       => The_Totals.VCs_Proved_By_Checker (R),
               Review        => The_Totals.VCs_Proved_By_Review (R),
               False_VCs     => The_Totals.VCs_Proved_False (R),
               Undischarged  => The_Totals.VCs_Undischarged (R),
               Show_Warn_Tag => False);
         end if;
      end loop;

      Print_Table_Separator;

      Print_Table_Row
        (Title         => "Totals:",
         The_Total     => Sum (The_Totals.VCs_Total),
         Examiner      => Sum (The_Totals.VCs_Proved_By_Examiner),
         Simplifier    => Sum (The_Totals.VCs_Proved_By_Simplifier),
         User_Rules    => Sum (The_Totals.VCs_Proved_With_User_Proof_Rule),
         Victor        => Sum (The_Totals.VCs_Proved_By_Victor),
         Riposte       => Sum (The_Totals.VCs_Proved_By_Riposte),
         Checker       => Sum (The_Totals.VCs_Proved_By_Checker),
         Review        => Sum (The_Totals.VCs_Proved_By_Review),
         False_VCs     => Sum (The_Totals.VCs_Proved_False),
         Undischarged  => Sum (The_Totals.VCs_Undischarged),
         Show_Warn_Tag => True);

      --# assert True;

      if CommandLine.Data.OutputPercentUndischarged and then Sum (The_Totals.VCs_Total) /= 0 then

         Calculate_Percentages
           (The_Totals                     => The_Totals,
            Percent_Undischarged_Str       => Percent_Undischarged_Str,
            Percent_Proved_By_Examiner_Str => Percent_Proved_By_Examiner_Str,
            Percent_Proved_By_Victor_Str   => Percent_Proved_By_Victor_Str,
            Percent_Proved_By_Riposte_Str  => Percent_Proved_By_Riposte_Str,
            Percent_Proved_By_Checker_Str  => Percent_Proved_By_Checker_Str,
            Percent_Proved_By_Review_Str   => Percent_Proved_By_Review_Str,
            Percent_Simplified_Str         => Percent_Simplified_Str,
            Percent_With_User_Rule_Str     => Percent_With_User_Rule_Str,
            Percent_Proved_False_Str       => Percent_Proved_False_Str);

         if Sum (The_Totals.VCs_Proved_With_User_Proof_Rule) = 0 then
            Percent_With_User_Rule_Str := E_Strings.Empty_String;
         end if;

         Print_Table_String_Row
           (Title        => "%Totals:",
            The_Total    => E_Strings.Empty_String,
            Examiner     => Percent_Proved_By_Examiner_Str,
            Simplifier   => Percent_Simplified_Str,
            User_Rules   => Percent_With_User_Rule_Str,
            Victor       => Percent_Proved_By_Victor_Str,
            Riposte      => Percent_Proved_By_Riposte_Str,
            Checker      => Percent_Proved_By_Checker_Str,
            Review       => Percent_Proved_By_Review_Str,
            False_VCs    => Percent_Proved_False_Str,
            Undischarged => Percent_Undischarged_Str);
      end if;

      --# assert True;

      -- If we used or tried to use Victor or Riposte, we print a warning

      if The_Totals.Subprograms_With_ALO_Victor_VC > 0
        or else The_Totals.Subprograms_Where_Error (VCDetails.Missing_VLG_File) > 0
        or else The_Totals.Subprograms_Where_Error (VCDetails.Corrupt_VCT_File) > 0
        or else The_Totals.Subprograms_Where_Error (VCDetails.Corrupt_VLG_File) > 0 then
         Overall_Warnings := True;
         SPARK_IO.Put_Line (Report_File, "!!! WARNING: Experimental feature used: Proof by Victor", 0);
      end if;
      if The_Totals.Subprograms_Where_Error (VCDetails.Missing_VLG_File) > 0
        or else The_Totals.Subprograms_Where_Error (VCDetails.Corrupt_VCT_File) > 0
        or else The_Totals.Subprograms_Where_Error (VCDetails.Corrupt_VLG_File) > 0 then
         Overall_Errors := True;
      end if;

      if The_Totals.Subprograms_With_ALO_Riposte_VC > 0
        or else The_Totals.Subprograms_Where_Error (VCDetails.Corrupt_RSM_File) > 0 then
         Overall_Warnings := True;
         SPARK_IO.Put_Line (Report_File, "!!! WARNING: Experimental feature used: Proof with Riposte", 0);
      end if;
      if The_Totals.Subprograms_Where_Error (VCDetails.Corrupt_RSM_File) > 0 then
         Overall_Errors := True;
      end if;

      --# assert True;

      -- Only report errors if there are some.
      if The_Totals.Subprograms_Where_VC_Analysis_Abandoned > 0 then
         Overall_Errors := True;
         SPARK_IO.Put_Line (Report_File, "!!! ERRORS IN FILES RELATED TO ANALYSIS OF VCs; as below:", 0);
         for X in VCDetails.Error_Type_Missing_VC_Files loop
            if The_Totals.Subprograms_Where_Error (X) > 0 then
               case X is
                  when VCDetails.Missing_SLG_File =>
                     SPARK_IO.Put_String (Report_File, "!!!   Number of missing SLG (simplifier log) files:                  ", 0);
                  when VCDetails.Missing_VLG_File =>
                     SPARK_IO.Put_String (Report_File, "!!!   Number of missing VLG (ViCToR log) files:                      ", 0);
               end case;
               SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Where_Error (X), 8, 10);
               SPARK_IO.New_Line (Report_File, 1);
            end if;
         end loop;
         for X in VCDetails.Error_Type_Corrupt_VC_Files loop
            if The_Totals.Subprograms_Where_Error (X) > 0 then
               case X is
                  when VCDetails.Corrupt_VCG_File =>
                     SPARK_IO.Put_String (Report_File, "!!!   Number of erroneous VCG files:                                 ", 0);
                  when VCDetails.Corrupt_SIV_File =>
                     SPARK_IO.Put_String (Report_File, "!!!   Number of erroneous SIV (simplified) files:                    ", 0);
                  when VCDetails.Corrupt_SLG_File =>
                     SPARK_IO.Put_String (Report_File, "!!!   Number of erroneous SLG (simplifier log) files:                ", 0);
                  when VCDetails.Corrupt_VCT_File =>
                     SPARK_IO.Put_String (Report_File, "!!!   Number of erroneous VCT (Victor) files:                        ", 0);
                  when VCDetails.Corrupt_VLG_File =>
                     SPARK_IO.Put_String (Report_File, "!!!   Number of erroneous VLG (Victor log) files:                    ", 0);
                  when VCDetails.Corrupt_RSM_File =>
                     SPARK_IO.Put_String
                       (Report_File,
                        "!!!   Number of erroneous RSM (Riposte summary) files:                        ",
                        0);
                  when VCDetails.Corrupt_PLG_File =>
                     SPARK_IO.Put_String (Report_File, "!!!   Number of erroneous PLG (checker proof log) files:             ", 0);
                  when VCDetails.Corrupt_PRV_File =>
                     SPARK_IO.Put_String (Report_File, "!!!   Number of erroneous PRV (manual proof review) files:           ", 0);
               end case;
               SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Where_Error (X), 8, 10);
               SPARK_IO.New_Line (Report_File, 1);
            end if;
         end loop;
      end if;

      --# assert True;

      if The_Totals.Subprograms_Where_DPC_Analysis_Abandoned > 0 then
         Overall_Errors := True;
         SPARK_IO.Put_String (Report_File, "!!! ERRORS IN DPC FILES:                                          !!!", 0);
         SPARK_IO.Put_Integer (Report_File, The_Totals.Subprograms_Where_DPC_Analysis_Abandoned, 8, 10);
         SPARK_IO.New_Line (Report_File, 1);
      end if;

      SPARK_IO.New_Line (Report_File, 1);

      --# assert True;

      Print_Final_Summary;

   end Output;

begin
   The_Totals :=
     Total_Type'
     (Subprograms_With_VCs                     => 0,
      Subprograms_Where_Error                  => Error_Type_Counter'(others => 0),
      Subprograms_Where_VC_Analysis_Abandoned  => 0,
      Subprograms_Where_DPC_Analysis_Abandoned => 0,
      Subprograms_With_ALO_Undischarged_VC     => 0,
      Subprograms_With_ALO_Examiner_VC         => 0,
      Subprograms_With_ALO_Simplifier_VC       => 0,
      Subprograms_With_ALO_Contradiction_VC    => 0,
      Subprograms_With_ALO_User_Rule_VC        => 0,
      Subprograms_With_ALO_Victor_VC           => 0,
      Subprograms_With_ALO_Riposte_VC          => 0,
      Subprograms_With_ALO_Checker_VC          => 0,
      Subprograms_With_ALO_Review_VC           => 0,
      Subprograms_With_ALO_False_VC            => 0,
      Subprograms_Proved_By_Examiner           => 0,
      Subprograms_Proved_By_Simplifier         => 0,
      Subprograms_Proved_By_Victor             => 0,
      Subprograms_Proved_By_Riposte            => 0,
      Subprograms_Proved_By_Checker            => 0,
      Subprograms_Proved_With_User_Proof_Rule  => 0,
      Subprograms_Proved_By_Review             => 0,
      VCs_Total                                => Null_VC_Counter,
      VCs_Proved_By_Examiner                   => Null_VC_Counter,
      VCs_Proved_By_Simplifier                 => Null_VC_Counter,
      VCs_Proved_By_Victor                     => Null_VC_Counter,
      VCs_Proved_By_Riposte                    => Null_VC_Counter,
      VCs_Proved_By_Checker                    => Null_VC_Counter,
      VCs_Proved_With_User_Proof_Rule          => Null_VC_Counter,
      VCs_Proved_By_Review                     => Null_VC_Counter,
      VCs_Proved_False                         => Null_VC_Counter,
      VCs_Undischarged                         => Null_VC_Counter,
      Subprograms_With_DPCs                    => 0,
      Subprograms_With_Dead_Paths              => 0,
      Number_Of_Dead_Paths                     => 0);
end Total;