-------------------------------------------------------------------------------
-- (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.
--
--=============================================================================

with CommandLineData;
with E_Strings;
with LexTokenManager;
with SystemErrors;
with XMLReport;

use type CommandLineData.Flow_Analysis_Options;

separate (ErrorHandler)
package body Justifications is

   -- The Data Table, stored in Error_Context_Rec, has to serve two separate purposes:
   -- (1) a list of justifications in lexical order for listing at end of rep and lst files
   -- (2) a list structured by unit within the file that identifies which justifications are
   --     "in scope" at any particular time and which deal with nested units.

   -- For the first role, we just use the array of records in order.  Index 1 is the first justification
   -- and Current_Slot the last one.  We can find all entries bt looping over 1 .. Current_Slot.

   -- For the second role we use a stack and a linkages in the table.  Each table entry has a previous pointer
   -- that points to the next lexically earlier entry of that unit.  The constant End_Of_List means there
   -- are no more entries.  For any particular unit, the starting point for the search will be the TOS of the
   -- unit stack.

   -- When we start processing a unit we push End_Of_List to start with but always keep TOS pointing at the most recent
   -- table entry that has been added.

   -- When we finish processing the errors for a unit, the stack is popped thus removing all
   -- justifications for that unit from consideration but leaving them unchanged in the table for the first
   -- purpose described earlier.

   -- Last_Line-------------------------------------------------------------------
   -- The default scope of a justification is from the start justify to the end of the unit
   -- in which it appears.  An end justify can restrict this scope.  We don't actually need
   -- to know the last line number as we can use the following constant to represent it.
   -- In effect End_Of_Line_Unit has the value "infinity".
   End_Line_Of_Unit_Marker : constant LexTokenManager.Line_Numbers := 0;

   -- constant of private type declared in package spec
   Null_Unmatched_Justification_Iterator : constant Unmatched_Justification_Iterator :=
     Unmatched_Justification_Iterator'
     (Current_Table_Entry => ErrorHandler.End_Of_List,
      Current_Position    => LexTokenManager.Token_Position'(Start_Line_No => 0,
                                                             Start_Pos     => 0));

   No_Match_Message : constant String := "!!! No match found.";

   -- local stack operations -------------------------------
   function Current_Unit_List_Head (Unit_Stack : ErrorHandler.Unit_Stacks) return ErrorHandler.Data_Table_Ptr is
   begin
      SystemErrors.RT_Assert
        (C       => Unit_Stack.Ptr > 0,
         Sys_Err => SystemErrors.Precondition_Failure,
         Msg     => "Stack underflow in error justification handler");
      return Unit_Stack.Vector (Unit_Stack.Ptr).List_Items;
   end Current_Unit_List_Head;

   function Stack_Is_Empty (Unit_Stack : ErrorHandler.Unit_Stacks) return Boolean is
   begin
      return Unit_Stack.Ptr = 0;
   end Stack_Is_Empty;

   -- exported operations -------------------------------------------------------

   procedure Start_Unit (Which_Table : in out ErrorHandler.Justifications_Data_Tables) is

      procedure Stack_New_Unit (Unit_Stack : in out ErrorHandler.Unit_Stacks)
      --# derives Unit_Stack from *;
      is
      begin
         SystemErrors.RT_Assert
           (C       => Unit_Stack.Ptr < ErrorHandler.Max_Stack_Size,
            Sys_Err => SystemErrors.Precondition_Failure,
            Msg     => "Stack overflow in error justification handler");
         Unit_Stack.Ptr                     := Unit_Stack.Ptr + 1;
         Unit_Stack.Vector (Unit_Stack.Ptr) :=
           ErrorHandler.Stack_Record'(List_Items             => ErrorHandler.End_Of_List,
                                      Semantic_Error_In_Unit => False);
      end Stack_New_Unit;

   begin
      Stack_New_Unit (Unit_Stack => Which_Table.Unit_Stack);
   end Start_Unit;

   procedure Set_Current_Unit_Has_Semantic_Errors (Which_Table : in out ErrorHandler.Justifications_Data_Tables) is
   begin
      -- If a semantic error occurs before we get into the declarative part, or statements
      -- of a unit then the stack will be empty; however, there are no justifiable warnings
      -- for these regions so we can simply ignore the call
      if not Stack_Is_Empty (Unit_Stack => Which_Table.Unit_Stack) then
         Which_Table.Unit_Stack.Vector (Which_Table.Unit_Stack.Ptr).Semantic_Error_In_Unit := True;
      end if;
   end Set_Current_Unit_Has_Semantic_Errors;

   -- Operations concerned with reaching the end of a subprogram or other unit.  We provide an
   -- iterator for finding all the unmatched justifications so that Errorhandler.End_Unit can report
   -- them and also a stack Pop operation to clear the now completed unit from scope.

   -- local functions shared by First_Unmatched_Justification and Next_Unmatched_Justification
   -- Don't report unmatched flow  messages if a semantic error has occurred
   function Ignore_Flow_When_Semantic_Errors
     (Which_Table  : ErrorHandler.Justifications_Data_Tables;
      Current_Item : ErrorHandler.Data_Table_Ptr)
     return         Boolean
   is
      function Current_Unit_Has_Semantic_Errors (Unit_Stack : ErrorHandler.Unit_Stacks) return Boolean is
      begin
         SystemErrors.RT_Assert
           (C       => Unit_Stack.Ptr > 0,
            Sys_Err => SystemErrors.Precondition_Failure,
            Msg     => "Stack underflow in error justification handler");
         return Unit_Stack.Vector (Unit_Stack.Ptr).Semantic_Error_In_Unit;
      end Current_Unit_Has_Semantic_Errors;

   begin
      return Current_Unit_Has_Semantic_Errors (Unit_Stack => Which_Table.Unit_Stack)
        and then Which_Table.Data_Table (Current_Item).Kind = ErrorHandler.Flow_Message;
   end Ignore_Flow_When_Semantic_Errors;

   -- Don't report unmatched information-flow messages in data-flow mode. It may be that lower
   -- levels of the calling hierarchy have full derives annotations, but higher levels are
   -- analysed in data-flow mode. The information-flow relations are not calculated in data-
   -- flow mode so the justifications cannot be checked, and are therefore ignored.
   -- If flow=auto and derives are present then the justification can be checked.
   -- If flow=auto and derives not present then the justification should not be there.
   function Ignore_Information_Flow_Errors
     (Which_Table  : ErrorHandler.Justifications_Data_Tables;
      Current_Item : ErrorHandler.Data_Table_Ptr)
     return         Boolean
   --# global in CommandLineData.Content;
   is
      function Is_IFA (Num : Natural) return Boolean is
      begin
         return Num = 50 or else Num = 57 or else Num = 601 or else Num = 602;
      end Is_IFA;

   begin -- Ignore_Information_Flow_Errors
      return CommandLineData.Content.Flow_Option = CommandLineData.Data_Flow
        and then Which_Table.Data_Table (Current_Item).Kind = ErrorHandler.Flow_Message
        and then Is_IFA (Num => Which_Table.Data_Table (Current_Item).Err_Num);
   end Ignore_Information_Flow_Errors;

   procedure First_Unmatched_Justification
     (It          :    out Unmatched_Justification_Iterator;
      Which_Table : in     ErrorHandler.Justifications_Data_Tables)
   is
      Current_Item : ErrorHandler.Data_Table_Ptr;
   begin
      -- establish default answer
      It := Null_Unmatched_Justification_Iterator;
      -- seek unmatched items
      Current_Item := Current_Unit_List_Head (Unit_Stack => Which_Table.Unit_Stack);
      while Current_Item /= ErrorHandler.End_Of_List loop
         -- Only justifications with specific identifiers are checked for matches.
         -- A justification which applies to all does not have to have a match
         if not Which_Table.Data_Table (Current_Item).Applies_To_All
           and then Which_Table.Data_Table (Current_Item).Match_Count = 0
           and then
           -- Unmatched item found,
           -- but we ignore it if it is a flow error justification and the flow analyser hasn't run
           (not Ignore_Flow_When_Semantic_Errors (Which_Table  => Which_Table,
                                                  Current_Item => Current_Item))
           and then (not Ignore_Information_Flow_Errors (Which_Table  => Which_Table,
                                                         Current_Item => Current_Item)) then
            It :=
              Unmatched_Justification_Iterator'
              (Current_Table_Entry => Which_Table.Data_Table (Current_Item).Previous,
               Current_Position    => Which_Table.Data_Table (Current_Item).Position);

            exit;
         end if;
         Current_Item := Which_Table.Data_Table (Current_Item).Previous;
      end loop;
   end First_Unmatched_Justification;

   procedure Next_Unmatched_Justification
     (It          : in out Unmatched_Justification_Iterator;
      Which_Table : in     ErrorHandler.Justifications_Data_Tables)
   is
      Current_Item : ErrorHandler.Data_Table_Ptr;
   begin
      Current_Item := It.Current_Table_Entry;
      -- establish default answer
      It := Null_Unmatched_Justification_Iterator;
      -- seek unmatched items
      while Current_Item /= ErrorHandler.End_Of_List loop
         -- Only justifications with specific identifiers are checked for matches.
         -- A justification which applies to all does not have to have a match
         if not Which_Table.Data_Table (Current_Item).Applies_To_All
           and then Which_Table.Data_Table (Current_Item).Match_Count = 0
           and then
           -- Unmatched item found,
           -- but we ignore it if it is a flow error justification and the flow analyser hasn't run
           (not Ignore_Flow_When_Semantic_Errors (Which_Table  => Which_Table,
                                                  Current_Item => Current_Item))
           and then (not Ignore_Information_Flow_Errors (Which_Table  => Which_Table,
                                                         Current_Item => Current_Item)) then
            It :=
              Unmatched_Justification_Iterator'
              (Current_Table_Entry => Which_Table.Data_Table (Current_Item).Previous,
               Current_Position    => Which_Table.Data_Table (Current_Item).Position);

            exit;
         end if;
         Current_Item := Which_Table.Data_Table (Current_Item).Previous;
      end loop;
   end Next_Unmatched_Justification;

   function Error_Position (It : Unmatched_Justification_Iterator) return LexTokenManager.Token_Position is
   begin
      return It.Current_Position;
   end Error_Position;

   function Is_Null_Iterator (It : Unmatched_Justification_Iterator) return Boolean is
   begin
      return It = Null_Unmatched_Justification_Iterator;
   end Is_Null_Iterator;

   procedure End_Unit (Which_Table : in out ErrorHandler.Justifications_Data_Tables) is

      procedure Stack_Pop_Unit (Unit_Stack : in out ErrorHandler.Unit_Stacks)
      --# derives Unit_Stack from *;
      is
      begin
         SystemErrors.RT_Assert
           (C       => Unit_Stack.Ptr > 0,
            Sys_Err => SystemErrors.Precondition_Failure,
            Msg     => "Stack underflow in error justification handler");
         Unit_Stack.Ptr := Unit_Stack.Ptr - 1;
      end Stack_Pop_Unit;

   begin
      -- Discard all justifications belonging to this now finished unit
      Stack_Pop_Unit (Unit_Stack => Which_Table.Unit_Stack);
   end End_Unit;

   -- end of operations associated with reaching the end of a unit

   procedure Start_Justification
     (Which_Table                    : in out ErrorHandler.Justifications_Data_Tables;
      Position                       : in     LexTokenManager.Token_Position;
      Line                           : in     LexTokenManager.Line_Numbers;
      Kind                           : in     ErrorHandler.Justification_Kinds;
      Err_Num                        : in     Natural;
      Identifiers                    : in     ErrorHandler.Justification_Identifiers;
      Applies_To_All                 : in     Boolean;
      Explanation                    : in     E_Strings.T;
      Maximum_Justifications_Reached :    out Boolean)
   is

      New_Entry : ErrorHandler.Data_Table_Entry;

      procedure Update_Current_Unit_List_Head (Which_Table : in out ErrorHandler.Justifications_Data_Tables)
      --# derives Which_Table from *;
      is
      begin
         SystemErrors.RT_Assert
           (C       => Which_Table.Unit_Stack.Ptr > 0,
            Sys_Err => SystemErrors.Precondition_Failure,
            Msg     => "Stack underflow in error justification handler");
         -- Set top of the stack that is associated with Which_Table to most recently added table entry index
         Which_Table.Unit_Stack.Vector (Which_Table.Unit_Stack.Ptr).List_Items := Which_Table.Current_Slot;
      end Update_Current_Unit_List_Head;

   begin
      -- The return parameter below is only ever set True once, when the table first fills up.  If the
      -- table is already full then we return False because we only want to generate one warning
      -- at the point of call where the table first fills, not at every call thereafter.
      Maximum_Justifications_Reached := False;

      if Which_Table.Accepting_More_Entries then
         Which_Table.Current_Slot := Which_Table.Current_Slot + 1;
         if Which_Table.Current_Slot = ErrorHandler.Max_Table_Entries then
            Maximum_Justifications_Reached     := True;       -- signal to caller that table has just become full
            Which_Table.Accepting_More_Entries := False;   -- remember that table is full for future calls
         end if;

         New_Entry :=
           ErrorHandler.Data_Table_Entry'
           (Kind           => Kind,
            Err_Num        => Err_Num,
            Identifiers    => Identifiers,
            Applies_To_All => Applies_To_All,
            Explanation    => Explanation,
            Position       => Position,
            Start_Line     => Line,
            End_Line       => End_Line_Of_Unit_Marker,
            End_Found      => False,
            Match_Count    => 0,
            Match_Line     => Which_Table.Data_Table (Which_Table.Current_Slot).Match_Line,
            Previous       => Current_Unit_List_Head (Unit_Stack => Which_Table.Unit_Stack));

         Which_Table.Data_Table (Which_Table.Current_Slot) := New_Entry;
         Update_Current_Unit_List_Head (Which_Table => Which_Table);
      end if;
   end Start_Justification;

   procedure End_Justification
     (Which_Table   : in out ErrorHandler.Justifications_Data_Tables;
      Line          : in     LexTokenManager.Line_Numbers;
      Unmatched_End :    out Boolean)
   is
      Entry_To_Check : ErrorHandler.Data_Table_Ptr;
      Match_Found    : Boolean := False;
      Starting_Line  : LexTokenManager.Line_Numbers;
   begin
      SystemErrors.RT_Assert
        (C       => not Stack_Is_Empty (Unit_Stack => Which_Table.Unit_Stack),
         Sys_Err => SystemErrors.Precondition_Failure,
         Msg     => "Stack underflow in End_Justification");

      Entry_To_Check := Current_Unit_List_Head (Unit_Stack => Which_Table.Unit_Stack);
      while Entry_To_Check /= ErrorHandler.End_Of_List loop
         if not Which_Table.Data_Table (Entry_To_Check).End_Found then
            -- a start justify with no matching end has been found
            Match_Found                                       := True;
            Which_Table.Data_Table (Entry_To_Check).End_Found := True;
            Which_Table.Data_Table (Entry_To_Check).End_Line  := Line; -- end justify restricts line range over which it is valid

            -- At this point we have matched one begin with one end; however, there is one further check to do to
            -- deal with the form of justify statement that has several clauses separated by '&'.  In this case we will
            -- have several entries all with the same start line.  We want to set all of these to be closed by the
            -- end we have just found.
            Starting_Line  := Which_Table.Data_Table (Entry_To_Check).Start_Line;
            Entry_To_Check := Which_Table.Data_Table (Entry_To_Check).Previous;
            while Entry_To_Check /= ErrorHandler.End_Of_List
            --# assert Match_Found;
            loop
               -- we process further linked table entries until we find one that has a different start line number
               -- and therefore is not part of the same multiple entry clause
               exit when Which_Table.Data_Table (Entry_To_Check).Start_Line /= Starting_Line;

               -- if we get to here, the line number is the same and it is part of the same clause
               Which_Table.Data_Table (Entry_To_Check).End_Found := True;
               Which_Table.Data_Table (Entry_To_Check).End_Line  := Line; -- restricts line range over which justify valid

               Entry_To_Check := Which_Table.Data_Table (Entry_To_Check).Previous;
            end loop;
         end if;
         exit when Match_Found; -- each end justify should only match one start
         Entry_To_Check := Which_Table.Data_Table (Entry_To_Check).Previous;
      end loop;
      -- Tell caller that end didn't match a start so that warning can be raised; however, don't return True
      -- if the table has filled up otherwise we will get lots of unmatched end warnings for the justifications
      -- that never got added because the table was full
      Unmatched_End := not Match_Found and Which_Table.Accepting_More_Entries;
   end End_Justification;

   procedure Check_Whether_Justified
     (Which_Table : in out ErrorHandler.Justifications_Data_Tables;
      Line        : in     LexTokenManager.Token_Position;
      Kind        : in     ErrorHandler.Justification_Kinds;
      Err_Num     : in     Natural;
      Identifiers : in     ErrorHandler.Justification_Identifiers;
      Match_Found :    out Boolean)
   is

      type Search_Sort is (Search_Identifiers, Search_Applies_To_All);

      Current_Stack_Ptr : ErrorHandler.Stack_Index;

      function Matching_Entry_Found
        (The_Table_Entry : ErrorHandler.Data_Table_Entry;
         Line            : LexTokenManager.Line_Numbers;
         Kind            : ErrorHandler.Justification_Kinds;
         Err_Num         : Natural;
         Identifiers     : ErrorHandler.Justification_Identifiers;
         Search_For      : Search_Sort)
        return            Boolean
      --# global in LexTokenManager.State;
      is
         function Below_End_Line (Line, End_Line : LexTokenManager.Line_Numbers) return Boolean is
            Result : Boolean;
         begin
            if End_Line = End_Line_Of_Unit_Marker then
               Result := True;
            else
               Result := Line <= End_Line;
            end if;
            return Result;
         end Below_End_Line;

         function Identifiers_Match
           (The_Table_Entry : ErrorHandler.Data_Table_Entry;
            Identifiers     : ErrorHandler.Justification_Identifiers)
           return            Boolean
         --# global in LexTokenManager.State;
         is
            Result : Boolean := True;

            function Identifier_Matches (From_The_Table, From_The_Call : ErrorHandler.Justification_Identifier) return Boolean
            --# global in LexTokenManager.State;
            is
               Result : Boolean;
            begin
               -- Tricky comparison.  From_The_Call will contain: a null string and a valid symbol;
               -- or a valid string and a null symbol; or both will be null.
               -- From_The_Table will contain either both null or both valid.
               -- We need to match as follows:
               if From_The_Call = ErrorHandler.Null_Justification_Identifier then
                  -- both null, so we require From_The_Table to be exactly the same
                  Result := From_The_Table = ErrorHandler.Null_Justification_Identifier;

               elsif LexTokenManager.Lex_String_Case_Insensitive_Compare
                 (Lex_Str1 => From_The_Call.String_Form,
                  Lex_Str2 => LexTokenManager.Null_String) =
                 LexTokenManager.Str_Eq then
                  Result := From_The_Call.Symbol_Form = From_The_Table.Symbol_Form;

               else -- Strings aren't null so compare them
                  Result :=
                    LexTokenManager.Lex_String_Case_Insensitive_Compare
                    (Lex_Str1 => From_The_Call.String_Form,
                     Lex_Str2 => From_The_Table.String_Form) =
                    LexTokenManager.Str_Eq;
               end if;

               return Result;
            end Identifier_Matches;

         begin -- Identifiers_Match
            for I in Integer range 1 .. ErrorHandler.Max_Justification_Identifier_Length loop
               if not Identifier_Matches
                 (From_The_Table => The_Table_Entry.Identifiers (I),
                  From_The_Call  => Identifiers (I)) then
                  Result := False;
                  exit;
               end if;
            end loop;
            return Result;
         end Identifiers_Match;

      begin -- Matching_Entry_Found
         return Line >= The_Table_Entry.Start_Line
           and then Below_End_Line (Line     => Line,
                                    End_Line => The_Table_Entry.End_Line)
           and then Err_Num = The_Table_Entry.Err_Num
           and then Kind = The_Table_Entry.Kind
           -- Last because it is much the most expensive test
           and then ((Search_For = Search_Identifiers
                        and then Identifiers_Match (The_Table_Entry => The_Table_Entry,
                                                    Identifiers     => Identifiers))
                     or else (Search_For = Search_Applies_To_All and then The_Table_Entry.Applies_To_All));
      end Matching_Entry_Found;

      procedure Check_Justified_In_Unit
        (Search_For  : in     Search_Sort;
         Which_Table : in out ErrorHandler.Justifications_Data_Tables;
         Line        : in     LexTokenManager.Token_Position;
         Kind        : in     ErrorHandler.Justification_Kinds;
         Err_Num     : in     Natural;
         Identifiers : in     ErrorHandler.Justification_Identifiers;
         Match_Found :    out Boolean)
      --# global in LexTokenManager.State;
      --# derives Match_Found,
      --#         Which_Table from Err_Num,
      --#                          Identifiers,
      --#                          Kind,
      --#                          LexTokenManager.State,
      --#                          Line,
      --#                          Search_For,
      --#                          Which_Table;
      is
         Entry_To_Check : ErrorHandler.Data_Table_Ptr;
      begin
         Match_Found := False;
         if not Stack_Is_Empty (Unit_Stack => Which_Table.Unit_Stack) then -- can't have a match if nothing is even in stack yet
            Entry_To_Check := Current_Unit_List_Head (Unit_Stack => Which_Table.Unit_Stack);
            while Entry_To_Check /= ErrorHandler.End_Of_List loop
               if Matching_Entry_Found
                 (The_Table_Entry => Which_Table.Data_Table (Entry_To_Check),
                  Line            => Line.Start_Line_No,
                  Kind            => Kind,
                  Err_Num         => Err_Num,
                  Identifiers     => Identifiers,
                  Search_For      => Search_For) then
                  -- note how many times we got a match
                  Which_Table.Data_Table (Entry_To_Check).Match_Count := Which_Table.Data_Table (Entry_To_Check).Match_Count + 1;
                  -- and retain the most recent line number where it happened
                  Which_Table.Data_Table (Entry_To_Check).Match_Line := Line.Start_Line_No;

                  -- finally, return result to caller
                  Match_Found := True;
                  exit;
               end if;
               Entry_To_Check := Which_Table.Data_Table (Entry_To_Check).Previous;
            end loop;
         end if;
      end Check_Justified_In_Unit;

   begin -- Check_Whether_Justified
      if CommandLineData.Content.Justification_Option = CommandLineData.Ignore then
         Match_Found := False;
      else
         -- First check against justification statements with specific identifiers.
         -- These miust be in the current unit.
         Check_Justified_In_Unit
           (Search_For  => Search_Identifiers,
            Which_Table => Which_Table,
            Line        => Line,
            Kind        => Kind,
            Err_Num     => Err_Num,
            Identifiers => Identifiers,
            Match_Found => Match_Found);

         -- If a a specific identifier match has not been found and we are
         -- analysing auto-generated code, look for a match with an Applies_To_All
         -- justification defined in successively enclosing units starting with
         -- the current unit.
         if not Match_Found
           and then CommandLineData.Content.Language_Profile in CommandLineData.Auto_Code_Generators
           and then not Stack_Is_Empty (Which_Table.Unit_Stack) then
            Current_Stack_Ptr := Which_Table.Unit_Stack.Ptr;
            for Previous_Unit in reverse ErrorHandler.Stack_Index range ErrorHandler.Stack_Index'First .. Current_Stack_Ptr loop
               Which_Table.Unit_Stack.Ptr := Previous_Unit;
               Check_Justified_In_Unit
                 (Search_For  => Search_Applies_To_All,
                  Which_Table => Which_Table,
                  Line        => Line,
                  Kind        => Kind,
                  Err_Num     => Err_Num,
                  Identifiers => Identifiers,
                  Match_Found => Match_Found);
               exit when Match_Found;
            end loop;
            Which_Table.Unit_Stack.Ptr := Current_Stack_Ptr;
         end if;
      end if;
   end Check_Whether_Justified;

   function Table_Contains_Entries (Which_Table : in ErrorHandler.Justifications_Data_Tables) return Boolean is
   begin
      return Which_Table.Current_Slot > 0;
   end Table_Contains_Entries;

   procedure Print_Justifications (Which_Table : in ErrorHandler.Justifications_Data_Tables;
                                   File        : in SPARK_IO.File_Type) is

      procedure Print_Common_Header
      --# global in     File;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                File;
      is
      begin
         -- This string is common to both "Full" and "Brief" justifications modes,
         -- so that the justifications summary table (in either mode) can be
         -- recognized by the HTML report file generator.  If this string changes,
         -- then Process_Report_Line in sparkhtml.adb will also need to be updated.
         SPARK_IO.Put_Line (File, "Expected messages marked with the accept annotation", 0);
      end Print_Common_Header;

      procedure Print_Full_Listing
      --# global in     CommandLineData.Content;
      --#        in     File;
      --#        in     Which_Table;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                CommandLineData.Content,
      --#                                File,
      --#                                Which_Table;
      is

         procedure Print_Headers
         --# global in     File;
         --#        in out SPARK_IO.File_Sys;
         --# derives SPARK_IO.File_Sys from *,
         --#                                File;
         is
         begin
            Print_Common_Header;
            SPARK_IO.Put_Line (File, "Type Msg    Lines              Reason                    Match", 0);
            SPARK_IO.Put_Line (File, "     No.  From    To                                    No.  Line", 0);
         end Print_Headers;

         procedure Print_Kind (The_Type : in ErrorHandler.Justification_Kinds)
         --# global in     File;
         --#        in out SPARK_IO.File_Sys;
         --# derives SPARK_IO.File_Sys from *,
         --#                                File,
         --#                                The_Type;
         is
         begin
            case The_Type is
               when ErrorHandler.Flow_Message =>
                  SPARK_IO.Put_String (File, "Flow ", 0);
               when ErrorHandler.Warning_Message =>
                  SPARK_IO.Put_String (File, "Warn ", 0);
            end case;
         end Print_Kind;

         procedure Print_Line_No (The_Line : in LexTokenManager.Line_Numbers)
         --# global in     CommandLineData.Content;
         --#        in     File;
         --#        in out SPARK_IO.File_Sys;
         --# derives SPARK_IO.File_Sys from *,
         --#                                CommandLineData.Content,
         --#                                File,
         --#                                The_Line;
         is
         begin
            if The_Line = 0 then
               SPARK_IO.Put_String (File, "   end", 0);
            elsif CommandLineData.Content.Plain_Output then
               SPARK_IO.Put_String (File, "      ", 0);
            else
               SPARK_IO.Put_Integer (File, Integer (The_Line), 6, 10);
            end if;
         end Print_Line_No;

         procedure Print_Explanation (Ex_Explanation : in E_Strings.T)
         --# global in     File;
         --#        in out SPARK_IO.File_Sys;
         --# derives SPARK_IO.File_Sys from *,
         --#                                Ex_Explanation,
         --#                                File;
         is
            Ch_Idx, Printed_Chars : Natural;
            Ch                    : Character;
            Field_Width           : constant := 32;
         begin
            SPARK_IO.Put_String (File, "  ", 0);
            Ch_Idx        := 1;
            Printed_Chars := 0;
            loop
               exit when Ch_Idx > E_Strings.Get_Length (E_Str => Ex_Explanation);
               exit when Printed_Chars >= Field_Width;

               Ch := E_Strings.Get_Element (E_Str => Ex_Explanation,
                                            Pos   => Ch_Idx);
               if Ch /= '"' then -- strip quotes
                  SPARK_IO.Put_Char (File, E_Strings.Get_Element (E_Str => Ex_Explanation,
                                                                  Pos   => Ch_Idx));
                  Printed_Chars := Printed_Chars + 1;
               end if;
               Ch_Idx := Ch_Idx + 1;
            end loop;
            -- if we haven't reached Field_Width then pad out with spaces
            for I in Natural range Printed_Chars .. Field_Width loop
               SPARK_IO.Put_Char (File, ' ');
            end loop;
         end Print_Explanation;

      begin -- Print_Full_Listing
         Print_Headers;
         for I in ErrorHandler.Data_Table_Index range 1 .. Which_Table.Current_Slot loop
            Print_Kind (The_Type => Which_Table.Data_Table (I).Kind);

            SPARK_IO.Put_Integer (File, Which_Table.Data_Table (I).Err_Num, 3, 10);

            Print_Line_No (The_Line => Which_Table.Data_Table (I).Start_Line);
            Print_Line_No (The_Line => Which_Table.Data_Table (I).End_Line);

            Print_Explanation (Which_Table.Data_Table (I).Explanation);
            SPARK_IO.Put_Integer (File, Which_Table.Data_Table (I).Match_Count, 4, 10);

            if Which_Table.Data_Table (I).Match_Count = 0 then
               SPARK_IO.Put_String (File, "  " & No_Match_Message, 0);
            else
               Print_Line_No (The_Line => Which_Table.Data_Table (I).Match_Line);
            end if;
            SPARK_IO.New_Line (File, 1);
         end loop;
         SPARK_IO.New_Line (File, 2);
      end Print_Full_Listing;

      procedure Print_Brief_Listing
      --# global in     File;
      --#        in     Which_Table;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                File,
      --#                                Which_Table;
      is
         Failed_Matches : Natural := 0;
      begin
         Print_Common_Header;
         for I in ErrorHandler.Data_Table_Index range 1 .. Which_Table.Current_Slot loop
            if Which_Table.Data_Table (I).Match_Count = 0 then
               Failed_Matches := Failed_Matches + 1;
            end if;
         end loop;
         SPARK_IO.Put_Integer (File, Integer (Which_Table.Current_Slot), 0, 10);
         SPARK_IO.Put_String (File, " message(s) marked as expected", 0);
         if Failed_Matches > 0 then
            SPARK_IO.Put_String (File, ", !!! Warning, ", 0);
            SPARK_IO.Put_Integer (File, Failed_Matches, 0, 10);
            SPARK_IO.Put_String (File, " message(s) did not occur", 0);

         end if;
         SPARK_IO.Put_Char (File, '.');
         SPARK_IO.New_Line (File, 2);
      end Print_Brief_Listing;

   begin -- Print_Justifications
      if Table_Contains_Entries (Which_Table => Which_Table) then
         SPARK_IO.New_Line (File, 1);
         case CommandLineData.Content.Justification_Option is
            when CommandLineData.Full =>
               Print_Full_Listing;
            when CommandLineData.Brief =>
               Print_Brief_Listing;
            when CommandLineData.Ignore =>
               null;
         end case;
      end if;
   end Print_Justifications;

   -- Precondition: Must be called on a report file, at the correct location in the schema
   procedure Print_Justifications_XML (Which_Table : in ErrorHandler.Justifications_Data_Tables;
                                       File        : in SPARK_IO.File_Type) is

      procedure Print_Full_Listing
      --# global in     File;
      --#        in     Which_Table;
      --#        in out SPARK_IO.File_Sys;
      --#        in out XMLReport.State;
      --# derives SPARK_IO.File_Sys from *,
      --#                                File,
      --#                                Which_Table,
      --#                                XMLReport.State &
      --#         XMLReport.State   from *,
      --#                                Which_Table;
      is

         No_Match_Explanation : E_Strings.T;

         function Print_Kind_To_String (The_Type : in ErrorHandler.Justification_Kinds) return E_Strings.T is
            Kind_String : E_Strings.T;
         begin
            case The_Type is
               when ErrorHandler.Flow_Message =>
                  Kind_String := E_Strings.Copy_String (Str => "Flow");
               when ErrorHandler.Warning_Message =>
                  Kind_String := E_Strings.Copy_String (Str => "Warning");
            end case;
            return Kind_String;
         end Print_Kind_To_String;

         function Print_Line_No_To_String (The_Line : in LexTokenManager.Line_Numbers) return E_Strings.T is
            Line_No_Str : E_Strings.T;
         begin
            if The_Line = 0 then
               Line_No_Str := E_Strings.Copy_String (Str => "end");
            else
               E_Strings.Put_Int_To_String (Dest     => Line_No_Str,
                                            Item     => Integer (The_Line),
                                            Start_Pt => 1,
                                            Base     => 10);
            end if;
            return Line_No_Str;
         end Print_Line_No_To_String;

      begin -- Print_Full_Listing
         No_Match_Explanation := E_Strings.Copy_String (Str => No_Match_Message);
         XMLReport.Start_Section (Section => XMLReport.S_Full_Justifications,
                                  Report  => File);

         for I in ErrorHandler.Data_Table_Index range 1 .. Which_Table.Current_Slot loop

            XMLReport.Start_Full_Justification
              (Print_Kind_To_String (The_Type => Which_Table.Data_Table (I).Kind),
               Which_Table.Data_Table (I).Err_Num,
               Integer (Which_Table.Data_Table (I).Start_Line),
               Print_Line_No_To_String (The_Line => Which_Table.Data_Table (I).End_Line),
               Which_Table.Data_Table (I).Match_Count,
               Integer (Which_Table.Data_Table (I).Match_Line),
               File);

            if Which_Table.Data_Table (I).Match_Count = 0 then
               E_Strings.Put_String (File  => File,
                                     E_Str => No_Match_Explanation);
            else
               E_Strings.Put_String (File  => File,
                                     E_Str => SPARK_XML.Filter_String (Which_Table.Data_Table (I).Explanation));
            end if;

            XMLReport.End_Full_Justification (File);
         end loop;
         XMLReport.End_Section (Section => XMLReport.S_Full_Justifications,
                                Report  => File);
      end Print_Full_Listing;

      procedure Print_Brief_Listing
      --# global in     File;
      --#        in     Which_Table;
      --#        in out SPARK_IO.File_Sys;
      --#        in out XMLReport.State;
      --# derives SPARK_IO.File_Sys from *,
      --#                                File,
      --#                                Which_Table,
      --#                                XMLReport.State &
      --#         XMLReport.State   from *,
      --#                                Which_Table;
      is
         Failed_Matches : Natural := 0;
      begin
         for I in ErrorHandler.Data_Table_Index range 1 .. Which_Table.Current_Slot loop
            if Which_Table.Data_Table (I).Match_Count = 0 then
               Failed_Matches := Failed_Matches + 1;
            end if;
         end loop;
         XMLReport.Brief_Justifications (Natural (Which_Table.Current_Slot), Failed_Matches, File);
      end Print_Brief_Listing;

   begin -- Print_Justifications_XML
      if Table_Contains_Entries (Which_Table => Which_Table) then
         XMLReport.Start_Section (Section => XMLReport.S_Justifications,
                                  Report  => File);
         case CommandLineData.Content.Justification_Option is
            when CommandLineData.Full =>
               Print_Full_Listing;
            when CommandLineData.Brief =>
               Print_Brief_Listing;
            when CommandLineData.Ignore =>
               null;
         end case;
         XMLReport.End_Section (Section => XMLReport.S_Justifications,
                                Report  => File);
      end if;
   end Print_Justifications_XML;

end Justifications;