-------------------------------------------------------------------------------
-- (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 to perform processing of VC files                                   --
--                                                                            --
--The method of collecting information from the VC files is described in the  --
--specification. Below is given the algorithm for writing the information to  --
--the report file.                                                            --
--                                                                            --
--In order to print the status of all VCs as a table, information about the   --
--VCs is now collected in the VCHeap.                                         --
--                                                                            --
--A record is put on the heap for each VC identified in the VCG file          --
--indicating its name (used for indexing the records) and status              --
--(undischarged at this point).                                               --
--                                                                            --
--The status is subsequently updated for VCs identified when parsing the      --
--SIV and PLG files (if the VC has been recognised as fully simplified        --
--or fully proved).                                                           --
--                                                                            --
--When this parsing phase is complete, the content of the VCHeap is printed   --
--to the report file.                                                         --
--                                                                            --
--------------------------------------------------------------------------------

with Ada.Characters.Handling;
with CommandLine;
with FatalErrors;
with Heap;
with OSFiling;
with PathFormatter;
with SPARK_Calendar;
with Total;
with VCDetails;
with VCHeap;

use type SPARK_Calendar.Error_Code;
use type VCDetails.VC_State_T;

package body VCS is

   -- All non-refinement and non-inheritance VCs have line numbers associated
   -- with their start and finish points.
   -- Sentinel values are used as follows:
   --    -1 is used for refinement and inheritance VCs, which do not have any
   --       line number associated with them.
   --     0 is used to mean the start of a subprogram (e.g. the precondition)
   -- 'Last is used to mean the end of a subprogram (e.g. the postcondition)

   subtype VC_Line_Type is Integer range -1 .. Integer'Last;
   Refinement_Or_Inheritance_VC : constant VC_Line_Type := -1;
   VC_Line_Start                : constant VC_Line_Type := 0;
   VC_Line_End                  : constant VC_Line_Type := VC_Line_Type'Last;

   -- Added to describe different forms of corrupt files.
   -- (This is known not to be a complete solution. The file parsing routines in
   -- pogs are quite basic, making it difficult to offer extensive well-formed
   -- file checks. Neverthless, the checks that are considered, are the most common,
   -- and are tracable to genuine user concerns.)
   type File_Status_T is (Not_Corrupt, Corrupt_Empty_File, Corrupt_Unknown_Subprogram);

   type File_Types is (Simplified_VC_File_Type, Standard_VC_File_Type);

   type Parsing_State_Type is (Initial, First_Range, First_VC_Name, New_Range, New_VC_Name);

   type VC_Info_Type is record
      Start_Line          : VC_Line_Type;
      End_Line            : VC_Line_Type;
      End_Line_Point_Type : VCDetails.Terminal_Point_Type;
      Number_Of_VCs       : Natural;
      Valid               : Boolean;   -- used so that invalid data (at start of
                                       -- processing) is not printed
      File_Type           : File_Types; -- SIV / VCG / PLG

      -- used to print the 'UndischargedVCs' message
      -- used to decide whether to print the start line for the given range
      Any_VCs_Printed : Boolean;
      This_Start_Line_Printed : Boolean;
   end record;

   subtype Errors_Index is Integer range 1 .. 1000;
   type Errors_List is array (Errors_Index) of E_Strings.T;

   type Review_Errors is record
      Errors       : Boolean;     -- Have we recorded any errors?
      Error_List   : Errors_List;  -- The list of errors
      Last_Error   : Errors_Index; -- The last error
      Excess_Count : Natural;     -- How many errors are unreported.
   end record;

   Report_Wrap_Column : constant Positive := 70;

   -- Note that all the columns below refer to the line AFTER it has been
   -- trimmed of white space
   VCG_File_Date_Time_Start_Column : constant E_Strings.Positions := 8;

   -- note, setting this to 20 ensures that the resolution is only down to
   -- the nearest second, for compatibility with the same information as
   -- extracted from the SIV file
   VCG_File_Date_Time_Length : constant E_Strings.Lengths := 20;

   SIV_File_VC_Generation_Date_Start_Column  : constant E_Strings.Positions := 9;
   SIV_File_VC_Generation_Date_Length        : constant E_Strings.Lengths   := 11;
   SIV_File_VC_Generation_Time_Start_Column  : constant E_Strings.Positions := 22;
   SIV_File_VC_Generation_Time_Length        : constant E_Strings.Lengths   := 8;
   SIV_File_Simplification_Date_Start_Column : constant E_Strings.Positions := 43;
   SIV_File_Simplification_Date_Length       : constant E_Strings.Lengths   := 11;
   SIV_File_Simplification_Time_Start_Column : constant E_Strings.Positions := 56;
   SIV_File_Simplification_Time_Length       : constant E_Strings.Lengths   := 8;

   -- Constants for processing DPC and SDP files.
   -- These constants are identical to the processing of VCG and
   -- SIV files as their format, at this time, are the same.

   DPC_File_Date_Time_Start_Column : constant E_Strings.Positions := 8;
   DPC_File_Date_Time_Length       : constant E_Strings.Lengths   := 20;

   SDP_File_VC_Generation_Date_Start_Column  : constant E_Strings.Positions := 9;
   SDP_File_VC_Generation_Date_Length        : constant E_Strings.Lengths   := 11;
   SDP_File_VC_Generation_Time_Start_Column  : constant E_Strings.Positions := 22;
   SDP_File_VC_Generation_Time_Length        : constant E_Strings.Lengths   := 8;
   SDP_File_Simplification_Date_Start_Column : constant E_Strings.Positions := 44;
   SDP_File_Simplification_Date_Length       : constant E_Strings.Lengths   := 11;
   SDP_File_Simplification_Time_Start_Column : constant E_Strings.Positions := 56;
   SDP_File_Simplification_Time_Length       : constant E_Strings.Lengths   := 8;

   -- Constants to extract Proof Log File date
   PLG_File_VC_Proof_Date_Start_Column : constant E_Strings.Positions := 8;
   PLG_File_VC_Proof_Date_Length       : constant E_Strings.Lengths   := 11;
   PLG_File_VC_Proof_Time_Start_Column : constant E_Strings.Positions := 28;
   PLG_File_VC_Proof_Time_Length       : constant E_Strings.Lengths   := 8;

   Unknown_SIV_Date : constant String := "Unknown SIV file date";
   Unknown_VCG_Date : constant String := "Unknown VCG file date";
   Unknown_SDP_Date : constant String := "Unknown SDP file date";
   Unknown_DPC_Date : constant String := "Unknown DPC file date";
   Unknown_VCT_Date : constant String := "Unknown VCT file date";

   ----------------------------------------------------------------------------
   -- NB this trims the string given, then appends a space and a trimmed version
   -- of the next line from the input file
   procedure Append_Next_Line_From_File (Line : in out E_Strings.T;
                                         File : in     SPARK_IO.File_Type)
   --# global in out SPARK_IO.File_Sys;
   --# derives Line,
   --#         SPARK_IO.File_Sys from *,
   --#                                File,
   --#                                SPARK_IO.File_Sys;
   is
      Next_Line    : E_Strings.T;
      Trimmed_Line : E_Strings.T;
   begin
      Trimmed_Line := E_Strings.Trim (Line);
      Line         := Trimmed_Line;
      E_Strings.Append_String (E_Str => Line,
                               Str   => " ");
      E_Strings.Get_Line (File  => File,
                          E_Str => Next_Line);
      Trimmed_Line := E_Strings.Trim (Next_Line);
      E_Strings.Append_Examiner_String (E_Str1 => Line,
                                        E_Str2 => Trimmed_Line);
   end Append_Next_Line_From_File;

   ---------------------------------------------------------------------------

   function Extract_Line_Number_At_Position (Line      : E_Strings.T;
                                             Start_Pos : E_Strings.Positions) return VC_Line_Type is
      Result   : VC_Line_Type := 0;
      Pos      : E_Strings.Positions;
      Finished : Boolean      := False;
   begin
      Pos := Start_Pos;

      while not Finished loop
         if E_Strings.Get_Element (E_Str => Line,
                                   Pos   => Pos) >= '0'
           and then E_Strings.Get_Element (E_Str => Line,
                                           Pos   => Pos) <= '9' then
            Result := (10 * Result) +
              (Character'Pos (E_Strings.Get_Element (E_Str => Line,
                                                     Pos   => Pos)) - Character'Pos ('0'));
            if Pos < E_Strings.Get_Length (E_Str => Line) then
               Pos := Pos + 1;
            else
               Finished := True;
            end if;
         else
            Finished := True;
         end if;
      end loop;

      return Result;
   end Extract_Line_Number_At_Position;

   ---------------------------------------------------------------------------

   function Is_VC_Proof_Success_Line (Line : E_Strings.T) return Boolean is
   begin
      return E_Strings.Eq1_String (E_Str => E_Strings.Section (Line, 1, 14),
                                   Str   => "*** PROVED VC ");
   end Is_VC_Proof_Success_Line;

   ---------------------------------------------------------------------------

   function Is_New_Range_Line (Line : E_Strings.T) return Boolean is
   begin
      return E_Strings.Eq1_String
        (E_Str => E_Strings.Section (E_Str     => Line,
                                     Start_Pos => 1,
                                     Length    => 17),
         Str   => "For path(s) from ")
        or else E_Strings.Eq1_String
        (E_Str => E_Strings.Section (E_Str     => Line,
                                     Start_Pos => 1,
                                     Length    => 14),
         Str   => "For checks of ");
   end Is_New_Range_Line;

   ---------------------------------------------------------------------------

   function Is_New_VC_Line (Line : E_Strings.T) return Boolean is
      Ret_Val : Boolean;
   begin
      --  The shortest possible New VC Line is for a function that has
      --  a single letter identifier, followed by a full-stop e.g.
      --  function_g.  which is 11 characters.
      if E_Strings.Get_Length (E_Str => Line) >= 11 then
         Ret_Val := E_Strings.Eq1_String (E_Str => E_Strings.Section (Line, 1, 10),
                                          Str   => "procedure_")
           or else E_Strings.Eq1_String (E_Str => E_Strings.Section (Line, 1, 9),
                                         Str   => "function_")
           or else E_Strings.Eq1_String (E_Str => E_Strings.Section (Line, 1, 10),
                                         Str   => "task_type_");
         if Ret_Val then
            for I in E_Strings.Lengths range 9 .. E_Strings.Get_Length (E_Str => Line) - 1 loop
               if not (Ada.Characters.Handling.Is_Alphanumeric (E_Strings.Get_Element (E_Str => Line,
                                                                                       Pos   => I))
                         or else E_Strings.Get_Element (E_Str => Line,
                                                        Pos   => I) = '_') then

                  Ret_Val := False;
                  exit;
               end if;
               --# assert I in 9 .. E_Strings.Get_Length (Line) - 1 and
               --#   Line = Line% and
               --#   E_Strings.Get_Length (Line) >= 11;
            end loop;

            if E_Strings.Get_Element (E_Str => Line,
                                      Pos   => E_Strings.Get_Length (E_Str => Line)) /= '.' then
               Ret_Val := False;
            end if;
         end if;
      else
         Ret_Val := False;
      end if;
      return Ret_Val;
   end Is_New_VC_Line;

   ---------------------------------------------------------------------------

   function Is_Trivially_True_VC (Line : E_Strings.T) return Boolean is
   begin
      return E_Strings.Eq1_String (E_Str => E_Strings.Section (Line, 1, 10),
                                   Str   => "*** true .");
   end Is_Trivially_True_VC;

   ---------------------------------------------------------------------------

   function Is_Trivially_False_VC (Line : E_Strings.T) return Boolean is
      VC_Proved_False : Boolean;
      Unused_Pos      : E_Strings.Positions;
   begin
      if E_Strings.Get_Length (E_Str => Line) >= 14 then
         --# accept F, 10, Unused_Pos, "Unused_Pos unused here";
         E_Strings.Find_Sub_String
           (E_Str         => Line,
            Search_String => "   false .",
            String_Found  => VC_Proved_False,
            String_Start  => Unused_Pos);
         --# end accept;
         -- It must be a conclusion, not a hypothesis!
         VC_Proved_False := VC_Proved_False and then (E_Strings.Get_Element (E_Str => Line,
                                                                             Pos   => 1) = 'C');
      else
         VC_Proved_False := False;
      end if;
      --# accept F, 33, Unused_Pos, "Unused_Pos unused here";
      return VC_Proved_False;
   end Is_Trivially_False_VC;

   ---------------------------------------------------------------------------

   function Is_VC_Error_Message (Line : E_Strings.T) return Boolean is
   begin
      return E_Strings.Get_Length (E_Str => Line) > 0 and then E_Strings.Get_Element (E_Str => Line,
                                                                                      Pos   => 1) = '!';
   end Is_VC_Error_Message;

   ---------------------------------------------------------------------------

   -- see file header
   procedure WriteVCInfo
     (Report_File                : in     SPARK_IO.File_Type;
      VC_Info                    : in     VC_Info_Type;
      Anything_Printed_This_Time :    out Boolean)
   --# global in out SPARK_IO.File_Sys;
   --# derives Anything_Printed_This_Time from VC_Info &
   --#         SPARK_IO.File_Sys          from *,
   --#                                         Report_File,
   --#                                         VC_Info;
      is separate;
   pragma Unreferenced (WriteVCInfo);

   ---------------------------------------------------------------------------

   procedure PrintVCReport
     (VC_Filename          : in E_Strings.T;
      SIV_Filename         : in E_Strings.T;
      VCTR_Filename        : in E_Strings.T;
      RSM_Filename         : in E_Strings.T;
      PLG_Filename         : in E_Strings.T;
      SLG_Filename         : in E_Strings.T;
      VC_Error             : in Boolean;
      SIV_Error            : in Boolean;
      VCTR_Error           : in Boolean;
      RSM_Error            : in Boolean;
      PLG_Error            : in Boolean;
      SLG_Error            : in Boolean;
      SLG_File_Missing     : in Boolean;
      REV_Errors           : in Review_Errors;
      Report_File          : in SPARK_IO.File_Type;
      Temp_File            : in SPARK_IO.File_Type;
      Temp_False_File      : in SPARK_IO.File_Type;
      Temp_Contra_File     : in SPARK_IO.File_Type;
      Temp_Victor_File     : in SPARK_IO.File_Type;
      Temp_Riposte_File    : in SPARK_IO.File_Type;
      Temp_User_File       : in SPARK_IO.File_Type;
      Temp_PR_Verr_File    : in SPARK_IO.File_Type;
      Temp_Warn_Error_File : in SPARK_IO.File_Type)
   --# global in     CommandLine.Data;
   --#        in     VCHeap.I_State;
   --#        in     VCHeap.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLine.Data,
   --#                                PLG_Error,
   --#                                PLG_Filename,
   --#                                Report_File,
   --#                                REV_Errors,
   --#                                RSM_Error,
   --#                                RSM_Filename,
   --#                                SIV_Error,
   --#                                SIV_Filename,
   --#                                SLG_Error,
   --#                                SLG_Filename,
   --#                                SLG_File_Missing,
   --#                                Temp_Contra_File,
   --#                                Temp_False_File,
   --#                                Temp_File,
   --#                                Temp_PR_Verr_File,
   --#                                Temp_Riposte_File,
   --#                                Temp_User_File,
   --#                                Temp_Victor_File,
   --#                                Temp_Warn_Error_File,
   --#                                VCHeap.I_State,
   --#                                VCHeap.State,
   --#                                VCTR_Error,
   --#                                VCTR_Filename,
   --#                                VC_Error,
   --#                                VC_Filename;
      is separate;

   ---------------------------------------------------------------------------

   -- Process a line of type (1). Note that this can actually spread over two
   -- file lines, so the first action of this procedure is to read the next
   -- line from the file and append it onto the previous one. This has no
   -- unwanted side effects, as there is always a blank line between this and
   -- the start of the VC
   procedure ProcessNewRangeLine (Line    : in     E_Strings.T;
                                  VC_Info : in out VC_Info_Type)
   --# derives VC_Info from *,
   --#                      Line;
      is separate;

   ---------------------------------------------------------------------------

   procedure Read_Next_Non_Blank_Line (File      : in     SPARK_IO.File_Type;
                                       Success   :    out Boolean;
                                       File_Line :    out E_Strings.T)
   --# global in out SPARK_IO.File_Sys;
   --# derives File_Line,
   --#         SPARK_IO.File_Sys,
   --#         Success           from File,
   --#                                SPARK_IO.File_Sys;
   is
      Finished     : Boolean     := False;
      Status       : Boolean     := False;
      Line_Read    : E_Strings.T;
      Trimmed_Line : E_Strings.T := E_Strings.Empty_String;
   begin
      while not Finished loop
         E_Strings.Get_Line (File  => File,
                             E_Str => Line_Read);
         Trimmed_Line := E_Strings.Trim (Line_Read);

         if E_Strings.Get_Length (E_Str => Trimmed_Line) > 0 then
            Status   := True;
            Finished := True;
         else
            if SPARK_IO.End_Of_File (File) then
               Status   := False;
               Finished := True;
            end if;
         end if;
      end loop;
      Success   := Status;
      File_Line := Trimmed_Line;
   end Read_Next_Non_Blank_Line;

   ---------------------------------------------------------------------------

   --  This will return true if the given E_Str indicates a
   --  subprogram. (This is line 10 in .vcg files.) Currently, we are
   --  a valid subprogram if we start with either procedure, function
   --  or task_type and then either follow with a space or a newline.
   function Is_Valid_Subprogram (E_Str : E_Strings.T) return Boolean is
      function VC_Or_Newline (Prefix : String) return Boolean
      --# global in E_Str;
      is
         Result : Boolean;
      begin
         if E_Strings.Starts_With (E_Str, Prefix) then
            --  We now know E_Str starts with the given prefix, now the
            --  next character must either not exist at all or be a
            --  space.
            --  Note that due to the implementation of E_Strings it
            --  would be sufficient to just call Get_Element; if we
            --  ask for a position outside the string E_Strings will
            --  return a space. However, the below is safe for future
            --  changes.
            if E_Strings.Get_Length (E_Str => E_Str) = Prefix'Length then
               Result := True;
            elsif E_Strings.Get_Element (E_Str => E_Str,
                                         Pos   => Prefix'Length + 1) = ' ' then
               Result := True;
            else
               Result := False;
            end if;
         else
            Result := False;
         end if;
         return Result;
      end VC_Or_Newline;

   begin
      return VC_Or_Newline ("procedure") or else VC_Or_Newline ("function") or else VC_Or_Newline ("task_type");
   end Is_Valid_Subprogram;

   ---------------------------------------------------------------------------

   procedure AnalyseVCFile
     (Report_File    : in     SPARK_IO.File_Type;
      Filename       : in     E_Strings.T;
      Error_In_File  :    out Boolean;
      File_Date_Time :    out E_Strings.T)
   --# global in     CommandLine.Data;
   --#        in out FatalErrors.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out VCHeap.I_State;
   --#        in out VCHeap.State;
   --# derives Error_In_File,
   --#         SPARK_IO.File_Sys from CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys &
   --#         FatalErrors.State,
   --#         VCHeap.State      from *,
   --#                                CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys,
   --#                                VCHeap.State &
   --#         File_Date_Time    from Filename,
   --#                                SPARK_IO.File_Sys &
   --#         VCHeap.I_State    from *,
   --#                                CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys;
   -- precondition to entering this procedure is that the VCG file exists
      is separate;

   ---------------------------------------------------------------------------

   procedure AnalyseSimplifiedVCFile
     (Report_File        : in     SPARK_IO.File_Type;
      Filename           : in     E_Strings.T;
      VC_File_Date_Time  : in     E_Strings.T;
      SIV_File_Date_Time :    out E_Strings.T;
      Error_In_SIV_File  :    out Boolean)
   --# global in     CommandLine.Data;
   --#        in out FatalErrors.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out VCHeap.State;
   --# derives Error_In_SIV_File,
   --#         SPARK_IO.File_Sys  from CommandLine.Data,
   --#                                 Filename,
   --#                                 Report_File,
   --#                                 SPARK_IO.File_Sys,
   --#                                 VC_File_Date_Time &
   --#         FatalErrors.State,
   --#         VCHeap.State       from *,
   --#                                 CommandLine.Data,
   --#                                 Filename,
   --#                                 Report_File,
   --#                                 SPARK_IO.File_Sys,
   --#                                 VCHeap.State,
   --#                                 VC_File_Date_Time &
   --#         SIV_File_Date_Time from Filename,
   --#                                 SPARK_IO.File_Sys;
   -- precondition to entering this procedure is that the SIV file exists
      is separate;

   ---------------------------------------------------------------------------

   procedure AnalyseVictoredVCFile
     (Report_File            : in     SPARK_IO.File_Type;
      Filename               : in     E_Strings.T;
      Error_In_VCTR_File     :    out Boolean;
      File_Error             :    out E_Strings.T;
      Temp_Victor_Error_File : in     SPARK_IO.File_Type)
   --# global in     CommandLine.Data;
   --#        in out FatalErrors.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out VCHeap.State;
   --# derives Error_In_VCTR_File,
   --#         File_Error,
   --#         SPARK_IO.File_Sys  from CommandLine.Data,
   --#                                 Filename,
   --#                                 Report_File,
   --#                                 SPARK_IO.File_Sys,
   --#                                 Temp_Victor_Error_File &
   --#         FatalErrors.State,
   --#         VCHeap.State       from *,
   --#                                 CommandLine.Data,
   --#                                 Filename,
   --#                                 Report_File,
   --#                                 SPARK_IO.File_Sys,
   --#                                 VCHeap.State;
   -- precondition to entering this procedure is that the VCT file exists
      is separate;

   ---------------------------------------------------------------------------

   procedure AnalyseVictorLogFile
     (Filename           : in     E_Strings.T;
      VC_File_Date_Time  : in     E_Strings.T;
      SIV_File_Date_Time : in     E_Strings.T;
      VLG_File_Date_Time :    out E_Strings.T;
      Error_In_VLG_File  :    out Boolean;
      File_Error         :    out E_Strings.T)
   --# global in out FatalErrors.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_In_VLG_File,
   --#         File_Error         from Filename,
   --#                                 SIV_File_Date_Time,
   --#                                 SPARK_IO.File_Sys,
   --#                                 VC_File_Date_Time &
   --#         FatalErrors.State,
   --#         SPARK_IO.File_Sys  from *,
   --#                                 Filename,
   --#                                 SPARK_IO.File_Sys &
   --#         VLG_File_Date_Time from Filename,
   --#                                 SPARK_IO.File_Sys;
   -- precondition to entering this procedure is that the VLG file exists
      is separate;

   ---------------------------------------------------------------------------

   procedure Analyse_Riposte_Summary_File
     (Report_File             : in     SPARK_IO.File_Type;
      Filename                : in     E_Strings.T;
      Error_In_RSM_File       :    out Boolean;
      File_Error              :    out E_Strings.T;
      Temp_Riposte_Error_File : in     SPARK_IO.File_Type)
   --# global in     CommandLine.Data;
   --#        in out FatalErrors.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out VCHeap.State;
   --# derives Error_In_RSM_File,
   --#         File_Error,
   --#         SPARK_IO.File_Sys from CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys,
   --#                                Temp_Riposte_Error_File &
   --#         FatalErrors.State,
   --#         VCHeap.State      from *,
   --#                                CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys,
   --#                                VCHeap.State;
   -- precondition to entering this procedure is that the RSM file exists
      is separate;

   ---------------------------------------------------------------------------

   procedure Analyse_DPC_File
     (Report_File    : in     SPARK_IO.File_Type;
      Filename       : in     E_Strings.T;
      Error_In_File  :    out Boolean;
      File_Date_Time :    out E_Strings.T)
   --# global in     CommandLine.Data;
   --#        in out FatalErrors.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out VCHeap.I_State;
   --#        in out VCHeap.State;
   --# derives Error_In_File,
   --#         SPARK_IO.File_Sys from CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys &
   --#         FatalErrors.State,
   --#         VCHeap.I_State,
   --#         VCHeap.State      from *,
   --#                                CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys,
   --#                                VCHeap.State &
   --#         File_Date_Time    from Filename,
   --#                                SPARK_IO.File_Sys;
   -- precondition to entering this procedure is that the DPC file exists
      is separate;

   ---------------------------------------------------------------------------

   procedure Analyse_Summary_DP_File
     (Report_File        : in     SPARK_IO.File_Type;
      Filename           : in     E_Strings.T;
      DPC_File_Date_Time : in     E_Strings.T;
      Error_In_SDP_File  :    out Boolean)
   --# global in     CommandLine.Data;
   --#        in out FatalErrors.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out VCHeap.State;
   --# derives Error_In_SDP_File,
   --#         SPARK_IO.File_Sys from CommandLine.Data,
   --#                                DPC_File_Date_Time,
   --#                                Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys &
   --#         FatalErrors.State,
   --#         VCHeap.State      from *,
   --#                                CommandLine.Data,
   --#                                DPC_File_Date_Time,
   --#                                Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys,
   --#                                VCHeap.State;
   -- precondition to entering this procedure is that the SIV file exists
      is separate;

   ---------------------------------------------------------------------------

   procedure AnalyseReviewFile
     (Report_File : in     SPARK_IO.File_Type;
      Filename    : in     E_Strings.T;
      Errors      :    out Review_Errors)
   --# global in     VCHeap.I_State;
   --#        in out FatalErrors.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out VCHeap.State;
   --# derives Errors,
   --#         SPARK_IO.File_Sys,
   --#         VCHeap.State      from Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys,
   --#                                VCHeap.I_State,
   --#                                VCHeap.State &
   --#         FatalErrors.State from *,
   --#                                Filename,
   --#                                Report_File,
   --#                                SPARK_IO.File_Sys,
   --#                                VCHeap.I_State,
   --#                                VCHeap.State;
   -- precondition to entering this procedure is that the PRV file exists
      is separate;

   ---------------------------------------------------------------------------

   procedure AnalyseProofLogFile
     (Report_File        : in     SPARK_IO.File_Type;
      Filename           : in     E_Strings.T;
      SIV_File_Date_Time : in     E_Strings.T;
      Error_In_File      :    out Boolean)
   --# global in     CommandLine.Data;
   --#        in out FatalErrors.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out VCHeap.State;
   --# derives Error_In_File,
   --#         SPARK_IO.File_Sys from CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                SIV_File_Date_Time,
   --#                                SPARK_IO.File_Sys &
   --#         FatalErrors.State,
   --#         VCHeap.State      from *,
   --#                                CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                SIV_File_Date_Time,
   --#                                SPARK_IO.File_Sys,
   --#                                VCHeap.State;
   -- precondition to entering this procedure is that the SIV file exists
      is separate;

   procedure AnalyseSimpLogFile
     (Report_File       : in     SPARK_IO.File_Type;
      Filename          : in     E_Strings.T;
      Rule_Files_Errors : in out SPARK_IO.File_Type;
      Rule_Files_Used   : in out SPARK_IO.File_Type;
      SLG_Error_In_File :    out Boolean)
   --# global in     CommandLine.Data;
   --#        in out FatalErrors.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives FatalErrors.State,
   --#         SPARK_IO.File_Sys from *,
   --#                                CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                Rule_Files_Errors,
   --#                                Rule_Files_Used,
   --#                                SPARK_IO.File_Sys &
   --#         Rule_Files_Errors,
   --#         Rule_Files_Used   from *,
   --#                                CommandLine.Data,
   --#                                Filename,
   --#                                SPARK_IO.File_Sys &
   --#         SLG_Error_In_File from CommandLine.Data,
   --#                                Filename,
   --#                                Report_File,
   --#                                Rule_Files_Errors,
   --#                                Rule_Files_Used,
   --#                                SPARK_IO.File_Sys;
   -- precondition to entering this procedure is that the SLG file exists
   -- and that the SIV file date time was valid
      is separate;

   ---------------------------------------------------------------------------

   procedure Analyse
     (Report_File             : in     SPARK_IO.File_Type;
      Filename                : in     E_Strings.T;
      Analyse_Proof_Log       : in     Boolean;
      Temp_File               : in     SPARK_IO.File_Type;
      Temp_False_File         : in     SPARK_IO.File_Type;
      Temp_Contra_File        : in     SPARK_IO.File_Type;
      Temp_Victor_File        : in     SPARK_IO.File_Type;
      Temp_Riposte_File       : in     SPARK_IO.File_Type;
      Temp_User_File          : in     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     SPARK_IO.File_Type;
      Temp_Warn_Error_File    : in     SPARK_IO.File_Type;
      Temp_SDP_Error_File     : in     SPARK_IO.File_Type;
      Temp_DPC_Error_File     : in     SPARK_IO.File_Type;
      Temp_Victor_Error_File  : in     SPARK_IO.File_Type;
      Temp_Riposte_Error_File : in     SPARK_IO.File_Type)
   is

      VC_Filename             : E_Strings.T;
      VC_File_Date_Time       : E_Strings.T;
      VC_File_Contained_Error : Boolean;

      SIV_File_Date_Time       : E_Strings.T;
      Simplified_VC_Filename   : E_Strings.T;
      SIV_File_Contained_Error : Boolean;

      Victored_VC_Filename      : E_Strings.T;
      VCTR_File_Contained_Error : Boolean;
      VCTR_File_Error           : E_Strings.T;

      Victor_Log_Filename             : E_Strings.T;
      Victor_File_Date_Time           : E_Strings.T;
      Victor_Log_File_Contained_Error : Boolean;
      Victor_Log_File_Error           : E_Strings.T;

      Riposte_Summary_Filename : E_Strings.T;
      RSM_File_Contained_Error : Boolean;
      RSM_File_Error           : E_Strings.T;

      Simplifier_Log_Filename  : E_Strings.T;
      SLG_File_Contained_Error : Boolean;
      SLG_File_Is_Missing      : Boolean;

      Proof_Log_Filename       : E_Strings.T;
      PLG_File_Contained_Error : Boolean;

      PRV_Filename    : E_Strings.T;
      PRV_File_Errors : Review_Errors;

      DPC_Filename             : E_Strings.T;
      DPC_File_Date_Time       : E_Strings.T;
      DPC_File_Contained_Error : Boolean;

      Summary_DP_Filename : E_Strings.T;

      SDP_File_Contained_Error : Boolean;

      Processed_VCG_File : Boolean;
      Processed_DPC_File : Boolean;

      procedure Say_Filename_Being_Processed (Filename : in E_Strings.T)
      --# global in     CommandLine.Data;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                CommandLine.Data,
      --#                                Filename;
      is
      begin
         SPARK_IO.Put_String (SPARK_IO.Standard_Output, "Processing file ", 0);
         E_Strings.Put_Line (File  => SPARK_IO.Standard_Output,
                             E_Str => PathFormatter.Format (Filename));
         SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
      end Say_Filename_Being_Processed;

   begin -- Analyse

      Processed_VCG_File := False;
      Processed_DPC_File := False;

      VC_File_Contained_Error  := False;
      SLG_File_Contained_Error := False;
      SLG_File_Is_Missing      := False;

      SIV_File_Date_Time := E_Strings.Empty_String;

      Simplified_VC_Filename  := E_Strings.Empty_String;
      Simplifier_Log_Filename := E_Strings.Empty_String;
      Proof_Log_Filename      := E_Strings.Empty_String;

      Victored_VC_Filename     := E_Strings.Empty_String;
      Riposte_Summary_Filename := E_Strings.Empty_String;

      PRV_File_Errors :=
        Review_Errors'
        (Errors       => False,
         Error_List   => Errors_List'(others => E_Strings.Empty_String),
         Last_Error   => Errors_Index'First,
         Excess_Count => 0);

      -- Initialise for VCG
      VC_Filename := Filename;
      E_Strings.Append_Examiner_String (E_Str1 => VC_Filename,
                                        E_Str2 => OSFiling.VC_File_Extension);
      -- Initialise for DPC
      DPC_Filename := Filename;
      E_Strings.Append_Examiner_String (E_Str1 => DPC_Filename,
                                        E_Str2 => OSFiling.DPC_File_Extension);
      -- Initialise for SDP
      Summary_DP_Filename := Filename;
      E_Strings.Append_Examiner_String (E_Str1 => Summary_DP_Filename,
                                        E_Str2 => OSFiling.Summary_DP_File_Extension);

      SIV_File_Contained_Error  := False;
      RSM_File_Contained_Error  := False;
      VCTR_File_Contained_Error := False;
      PLG_File_Contained_Error  := False;

      if OSFiling.Is_File (Name => VC_Filename) then
         -- Record that VCG file is present.
         Processed_VCG_File := True;
         -- Initilise the other files that may be seen.
         --
         -- The logic here is quite confusing.
         --
         -- These files are initialised to their full names if the vcg
         -- file exists. This initialisation is independent to the
         -- existence of these files, or their own dependencies.  The
         -- absence of this initialisation (null string, from default
         -- initialisations above) is detected and sometimes used. This
         -- null string test (hopefully) is only ever used to infer
         -- whether or not the vcg file exists. It might be a lot neater
         -- to just test to see if the vcg file exists.
         --
         -- Unfortunately, these empty strings may be processed in an
         -- unsafe manner. However, it seems that the potentially unsafe
         -- routines are only called when the vcg file is present, so
         -- these initialisations below must take place, and the
         -- potential errors are avoided.
         --
         -- Oh, note also that these are all local variables. But, this
         -- 'Analyse' procedure also contains a call to 'PrintVCReport'
         -- (it does analysis and printing), so the local variables have
         -- a wider impact than might be expected.

         -- Initialise for SIV
         Simplified_VC_Filename := Filename;
         E_Strings.Append_Examiner_String (E_Str1 => Simplified_VC_Filename,
                                           E_Str2 => OSFiling.Simplified_VC_File_Extension);

         -- Initialise for SLG
         Simplifier_Log_Filename := Filename;
         E_Strings.Append_Examiner_String (E_Str1 => Simplifier_Log_Filename,
                                           E_Str2 => OSFiling.Simplifier_Log_File_Extension);
         SLG_File_Contained_Error := False;

         -- Initialise for Victor
         Victored_VC_Filename := Filename;
         E_Strings.Append_Examiner_String (E_Str1 => Victored_VC_Filename,
                                           E_Str2 => OSFiling.Victored_VC_File_Extension);

         -- Initialise for Victor Log
         Victor_Log_Filename := Filename;
         E_Strings.Append_Examiner_String (E_Str1 => Victor_Log_Filename,
                                           E_Str2 => OSFiling.Victor_Log_File_Extension);

         -- Initialise for Riposte
         Riposte_Summary_Filename := Filename;
         E_Strings.Append_Examiner_String (E_Str1 => Riposte_Summary_Filename,
                                           E_Str2 => OSFiling.Riposte_Summary_File_Extension);

         -- Initialise for PLG
         Proof_Log_Filename := Filename;
         E_Strings.Append_Examiner_String (E_Str1 => Proof_Log_Filename,
                                           E_Str2 => OSFiling.Proof_Log_File_Extension);
         PLG_File_Contained_Error := False;

         -- Initialise for PRV ("Proof Review")
         PRV_Filename := Filename;
         E_Strings.Append_Examiner_String (E_Str1 => PRV_Filename,
                                           E_Str2 => OSFiling.Review_File_Extension);

         -- Processing VCG file
         -- ###################
         -- If the VCG file exists: analyse it

         Say_Filename_Being_Processed (Filename => VC_Filename);
         AnalyseVCFile (Report_File, VC_Filename, VC_File_Contained_Error,
                        -- for comparison with entry in SIV file
                        VC_File_Date_Time);

         if VC_File_Contained_Error then
            SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "*** Warning: VCG file error: subprogram processing abandoned ***", 0);
            SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
            VCHeap.Raise_Error (Error_Kind => VCDetails.Corrupt_VCG_File);
         end if;

         --# assert True;

         -- Processing SIV file
         -- ###################
         -- If VCG analysis is not in error then:
         -- If the SIV file exists: analyse it
         if not VC_File_Contained_Error then
            if OSFiling.Is_File (Name => Simplified_VC_Filename) then
               Say_Filename_Being_Processed (Filename => Simplified_VC_Filename);
               AnalyseSimplifiedVCFile
                 (Report_File        => Report_File,
                  Filename           => Simplified_VC_Filename,
                  VC_File_Date_Time  => VC_File_Date_Time,
                  SIV_File_Date_Time => SIV_File_Date_Time,
                  Error_In_SIV_File  => SIV_File_Contained_Error);

               if SIV_File_Contained_Error then
                  SPARK_IO.Put_Line
                    (SPARK_IO.Standard_Output,
                     "*** Warning: SIV file error: subprogram processing abandoned ***",
                     0);
                  SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
                  VCHeap.Raise_Error (Error_Kind => VCDetails.Corrupt_SIV_File);
               else

                  -- Processing SLG file
                  -- ###################
                  -- If VCG analysis is not in error then:
                  -- If the SIV analysis is not in error then:
                  -- if the SLG file exists: analyse it
                  -- DEBUG If you're looking to fix SEPR: 2263, then this is a good place to start..
                  if OSFiling.Is_File (Name => Simplifier_Log_Filename) then
                     Say_Filename_Being_Processed (Filename => Simplifier_Log_Filename);
                     AnalyseSimpLogFile
                       (Report_File,
                        Simplifier_Log_Filename,
                        Temp_Rlu_Error_File,
                        Temp_Rlu_Used_File,
                        SLG_File_Contained_Error);

                     if SLG_File_Contained_Error then
                        SPARK_IO.Put_Line
                          (SPARK_IO.Standard_Output,
                           "*** Warning: SLG file error: subprogram processing abandoned ***",
                           0);
                        SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
                        VCHeap.Raise_Error (Error_Kind => VCDetails.Corrupt_SLG_File);
                     end if;

                  else
                     SPARK_IO.Put_String (SPARK_IO.Standard_Output, "Simplifier log file not found: ", 0);
                     E_Strings.Put_Line
                       (File  => SPARK_IO.Standard_Output,
                        E_Str => PathFormatter.Format (Simplifier_Log_Filename));
                     SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);

                     -- The absence of an SLG file is not treated as an error.
                     -- Some organisations may deliberately delete SLG files, to
                     -- save space. To support the use of POGS on such data sets,
                     -- missing SLG files can not be regarded as errors, as this
                     -- would lead to the analysis of these subprograms being
                     -- abandoned.

                     -- It is still necessary to report missing SLG files. To maintain
                     -- the distinction between missing SLG and error, an additional
                     -- variable is used.
                     SLG_File_Is_Missing := True;
                     VCHeap.Raise_Error (Error_Kind => VCDetails.Missing_SLG_File);

                     -- See: EmptyStringHere?
                     -- Simplifier_Log_Filename := ELStrings.EmptyString;
                  end if;

                  -- TODO: J525-022: Do we want to look at the ViCToR equivalent here?

               end if;
            else
               -- DEBUG If you're looking to fix SEPR: 2264, then this is a good place to start..

               -- otherwise say that VCs not simplified
               SPARK_IO.New_Line (Report_File, 1);
               SPARK_IO.Put_Line (Report_File, "VCs not simplified", 0);

               -- See: EmptyStringHere?
               --Simplified_VC_Filename := ELStrings.EmptyString;
            end if;
         end if;

         --# assert True;

         -- Processing VCT and VLG files
         -- ############################
         -- If VCG analysis is not in error and
         -- If SIV analysis is not in error (or never happened, in which case it is not in error) then:
         -- Check that the vct file exists
         -- Check that the vlg file exists and obtain its timestamp
         -- Compare timestamps of the vlg to the ones recorded in vcg
         --    and siv files (which will be raised as an error if they
         --    are not in the expected sequence)
         -- Analyse the vct file if the above resulted in no errors
         if not VC_File_Contained_Error and not SIV_File_Contained_Error then
            if OSFiling.Is_File (Name => Victored_VC_Filename) then
               if OSFiling.Is_File (Name => Victor_Log_Filename) then
                  --  First we analyse the VLG file
                  Say_Filename_Being_Processed (Filename => Victor_Log_Filename);
                  --# accept F, 10, Victor_File_Date_Time, "We don't use this yet, but may in the future.";
                  AnalyseVictorLogFile
                    (Filename           => Victor_Log_Filename,
                     VC_File_Date_Time  => VC_File_Date_Time,
                     SIV_File_Date_Time => SIV_File_Date_Time,
                     VLG_File_Date_Time => Victor_File_Date_Time,
                     Error_In_VLG_File  => Victor_Log_File_Contained_Error,
                     File_Error         => Victor_Log_File_Error);
                  --# end accept;

                  --  We still flag this up as an error.
                  --  Victor_Log_File_Contained_Error will not get passed on later,
                  --  but VCTR_File_Contained_Error will be.
                  if Victor_Log_File_Contained_Error then
                     VCTR_File_Contained_Error := True;
                  end if;

                  --  Then we analyse the VCT file if the above resulted in no errors
                  if not Victor_Log_File_Contained_Error then
                     Say_Filename_Being_Processed (Filename => Victored_VC_Filename);
                     AnalyseVictoredVCFile
                       (Report_File,
                        Victored_VC_Filename,
                        VCTR_File_Contained_Error,
                        VCTR_File_Error,
                        Temp_Victor_Error_File);

                     if VCTR_File_Contained_Error then
                        SPARK_IO.Put_String (SPARK_IO.Standard_Output, "*** Warning: VCT file error: ", 0);
                        E_Strings.Put_Line (File  => SPARK_IO.Standard_Output,
                                            E_Str => VCTR_File_Error);
                        SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
                        VCHeap.Raise_Error (Error_Kind => VCDetails.Corrupt_VCT_File);

                        --  We also mention the error in the victor error file.
                        E_Strings.Put_String
                          (File  => Temp_Victor_Error_File,
                           E_Str => PathFormatter.Format (Victored_VC_Filename));
                        SPARK_IO.Put_Char (Temp_Victor_Error_File, ' ');
                        SPARK_IO.Put_Char (Temp_Victor_Error_File, '(');
                        E_Strings.Put_String (File  => Temp_Victor_Error_File,
                                              E_Str => VCTR_File_Error);
                        SPARK_IO.Put_Line (Temp_Victor_Error_File, ")", 0);
                     end if;
                  else
                     SPARK_IO.Put_String (SPARK_IO.Standard_Output, "*** Warning: VLG file error: ", 0);
                     E_Strings.Put_Line (File  => SPARK_IO.Standard_Output,
                                         E_Str => Victor_Log_File_Error);
                     SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
                     VCHeap.Raise_Error (Error_Kind => VCDetails.Corrupt_VLG_File);

                     --  We also mention the error in the victor error file.
                     E_Strings.Put_String (File  => Temp_Victor_Error_File,
                                           E_Str => PathFormatter.Format (Victor_Log_Filename));
                     SPARK_IO.Put_Char (Temp_Victor_Error_File, ' ');
                     SPARK_IO.Put_Char (Temp_Victor_Error_File, '(');
                     E_Strings.Put_String (File  => Temp_Victor_Error_File,
                                           E_Str => Victor_Log_File_Error);
                     SPARK_IO.Put_Line (Temp_Victor_Error_File, ")", 0);
                  end if;
               else
                  SPARK_IO.Put_Line
                    (SPARK_IO.Standard_Output,
                     "*** Warning: VLG file missing: subprogram processing abandoned ***",
                     0);
                  SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
                  VCHeap.Raise_Error (Error_Kind => VCDetails.Missing_VLG_File);
               end if;
            end if;
            --  We don't mention it if no victor output can be found,
            --  as it is an optional feature.
         end if;

         --# assert True;

         -- Processing RSM file
         -- ###################
         -- If VCG analysis is not in error and
         -- If SIV analysis is not in error (or never happened, in which case it is not in error) then:
         -- Check that the rsm file exists
         -- Analyse the rsm file if the above resulted in no errors
         if not VC_File_Contained_Error and not SIV_File_Contained_Error then
            if OSFiling.Is_File (Name => Riposte_Summary_Filename) then
               Say_Filename_Being_Processed (Filename => Riposte_Summary_Filename);
               Analyse_Riposte_Summary_File
                 (Report_File,
                  Riposte_Summary_Filename,
                  RSM_File_Contained_Error,
                  RSM_File_Error,
                  Temp_Riposte_Error_File);

               if RSM_File_Contained_Error then
                  SPARK_IO.Put_String (SPARK_IO.Standard_Output, "*** Warning: RSM file error: ", 0);
                  E_Strings.Put_Line (File  => SPARK_IO.Standard_Output,
                                      E_Str => RSM_File_Error);
                  SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
                  VCHeap.Raise_Error (Error_Kind => VCDetails.Corrupt_RSM_File);

                  --  We also mention the error in the Riposte error file.
                  E_Strings.Put_String (File  => Temp_Riposte_Error_File,
                                        E_Str => PathFormatter.Format (Riposte_Summary_Filename));
                  SPARK_IO.Put_Char (Temp_Riposte_Error_File, ' ');
                  SPARK_IO.Put_Char (Temp_Riposte_Error_File, '(');
                  E_Strings.Put_String (File  => Temp_Riposte_Error_File,
                                        E_Str => RSM_File_Error);
                  SPARK_IO.Put_Line (Temp_Riposte_Error_File, ")", 0);
               end if;
            end if;
            --  We don't mention it if no Riposte output can be found,
            --  as it is an optional feature.
         end if;

         --# assert True;

         -- Processing PLG file
         -- ###################
         -- Unsimplified VCs might have been proven using the checker alone.
         -- If VCG analysis is not in error then:
         -- If any SIV analysis is not in error then:
         -- If any SLG analysis is not in error then:
         -- If any victor analysis is not in error (or never happened):
         -- If the 'Analyse_Proof_Log ' is set:
         -- If the PLG file exists then: analyse it
         -- Analyse the PLG file
         if not VC_File_Contained_Error and
           not SIV_File_Contained_Error and
           not SLG_File_Contained_Error and
           not VCTR_File_Contained_Error and
           Analyse_Proof_Log then
            if OSFiling.Is_File (Name => Proof_Log_Filename) then
               Say_Filename_Being_Processed (Filename => Proof_Log_Filename);
               AnalyseProofLogFile (Report_File, Proof_Log_Filename, SIV_File_Date_Time, PLG_File_Contained_Error);

               if PLG_File_Contained_Error then
                  SPARK_IO.Put_Line
                    (SPARK_IO.Standard_Output,
                     "*** Warning: PLG file error: subprogram processing abandoned ***",
                     0);
                  SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
                  VCHeap.Raise_Error (Error_Kind => VCDetails.Corrupt_PLG_File);
               end if;
            else
               null;
               -- See: EmptyStringHere?
               --Proof_Log_Filename := ELStrings.EmptyString;
            end if;
         end if;

         --# assert True;

         -- Processing PRV file
         -- ###################

         -- PRV files may be present regardless of simplification or application of the checker.
         -- If VCG analysis is not in error then:
         -- If any SIV analysis is not in error then:
         -- If any SLG analysis is not in error then:
         -- If any victor analysis is not in error (or never happened):
         -- If any PLG analysis is not in error then:
         -- If the PRV file exists then: analyse it

         if not VC_File_Contained_Error and
           not SIV_File_Contained_Error and
           not SLG_File_Contained_Error and
           not VCTR_File_Contained_Error and
           not PLG_File_Contained_Error and
           OSFiling.Is_File (Name => PRV_Filename) then
            Say_Filename_Being_Processed (Filename => PRV_Filename);
            AnalyseReviewFile (Report_File, PRV_Filename, PRV_File_Errors);

            if PRV_File_Errors.Errors then
               SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "*** Warning: PRV file error: subprogram processing abandoned ***", 0);
               SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
               VCHeap.Raise_Error (Error_Kind => VCDetails.Corrupt_PRV_File);
            end if;
         end if;

      end if;

      --# assert True;

      if OSFiling.Is_File (Name => DPC_Filename) then
         Processed_DPC_File := True;
         -- Processing DPC file
         -- ###################
         -- If the DPC file exists: analyse it.
         Say_Filename_Being_Processed (Filename => DPC_Filename);
         Analyse_DPC_File (Report_File, DPC_Filename, DPC_File_Contained_Error,
                           -- for comparison with entry in SDP file
                           DPC_File_Date_Time);

         if DPC_File_Contained_Error then
            SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "*** Warning: DPC file error: subprogram processing abandoned ***", 0);
            SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
            VCHeap.Raise_Error (Error_Kind => VCDetails.Corrupt_DPC_File);
         end if;

         --# assert True;

         -- Processing SDP File.
         -- ###################
         -- If the SDP file exists: analyse it
         if OSFiling.Is_File (Name => Summary_DP_Filename) then
            Say_Filename_Being_Processed (Filename => Summary_DP_Filename);
            Analyse_Summary_DP_File (Report_File, Summary_DP_Filename, DPC_File_Date_Time, SDP_File_Contained_Error);

            if SDP_File_Contained_Error then
               SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "*** Warning: SDP file error: subprogram processing abandoned ***", 0);
               SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
               VCHeap.Raise_Error (Error_Kind => VCDetails.Corrupt_SDP_File);
            end if;
         elsif OSFiling.Is_File (Name => DPC_Filename) and not OSFiling.Is_File (Name => Summary_DP_Filename) then
            SPARK_IO.New_Line (Report_File, 1);
            SPARK_IO.Put_Line (Report_File, "DPCs not ZombieScoped", 0);
            E_Strings.Put_Line (File  => Temp_SDP_Error_File,
                                E_Str => PathFormatter.Format (Summary_DP_Filename));
         elsif not OSFiling.Is_File (Name => DPC_Filename) and OSFiling.Is_File (Name => Summary_DP_Filename) then
            -- An error has occurred as an SDP file exists without the
            -- corresponding DPC file.
            SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "*** Warning: Missing DPC file error. ***", 0);
            SPARK_IO.Put_Line (Report_File, "*** Warning: Missing DPC files error. ***", 0);
            E_Strings.Put_Line (File  => Temp_DPC_Error_File,
                                E_Str => PathFormatter.Format (DPC_Filename));
         end if;
      end if;
      --# assert True;

      if Processed_VCG_File or Processed_DPC_File then
         Total.Update_Totals (VCG => Processed_VCG_File,
                              DPC => Processed_DPC_File);
         PrintVCReport
           (VC_Filename          => VC_Filename,
            SIV_Filename         => Simplified_VC_Filename,
            VCTR_Filename        => Victored_VC_Filename,
            RSM_Filename         => Riposte_Summary_Filename,
            PLG_Filename         => Proof_Log_Filename,
            SLG_Filename         => Simplifier_Log_Filename,
            VC_Error             => VC_File_Contained_Error,
            SIV_Error            => SIV_File_Contained_Error,
            VCTR_Error           => VCTR_File_Contained_Error,
            RSM_Error            => RSM_File_Contained_Error,
            PLG_Error            => PLG_File_Contained_Error,
            SLG_Error            => SLG_File_Contained_Error,
            SLG_File_Missing     => SLG_File_Is_Missing,
            REV_Errors           => PRV_File_Errors,
            Report_File          => Report_File,
            Temp_File            => Temp_File,
            Temp_False_File      => Temp_False_File,
            Temp_Contra_File     => Temp_Contra_File,
            Temp_Victor_File     => Temp_Victor_File,
            Temp_Riposte_File    => Temp_Riposte_File,
            Temp_User_File       => Temp_User_File,
            Temp_PR_Verr_File    => Temp_PR_Verr_File,
            Temp_Warn_Error_File => Temp_Warn_Error_File);

         SPARK_IO.New_Line (Report_File, 1);
      end if;

      --# assert True;

      --# accept Flow, 601, VCHeap.State, Temp_Rlu_Error_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, VCHeap.State, Temp_Rlu_Used_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, VCHeap.State, Temp_Victor_Error_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, VCHeap.State, Temp_Riposte_Error_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, VCHeap.I_State, Temp_Victor_Error_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, VCHeap.I_State, Temp_Riposte_Error_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, Total.State, Temp_Rlu_Error_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, Total.State, Temp_Rlu_Used_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, Total.State, Temp_Victor_Error_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, Total.State, Temp_Riposte_Error_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, Temp_Rlu_Error_File, CommandLine.Data, "False coupling through SPARK_IO" &
      --#        Flow, 601, Temp_Rlu_Used_File, CommandLine.Data, "False coupling through SPARK_IO" &
      --#        Flow, 601, Temp_Rlu_Error_File, Report_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, Temp_Rlu_Used_File, Report_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, FatalErrors.State, Temp_Victor_Error_File, "False coupling through SPARK_IO" &
      --#        Flow, 601, FatalErrors.State, Temp_Riposte_Error_File, "False coupling through SPARK_IO" &
      --#        Flow, 33, Victor_File_Date_Time, "We don't export this yet - we might in the future.";
   end Analyse;

end VCS;