File: errorhandler.adb

package info (click to toggle)
spark 2012.0.deb-9
links: PTS, VCS
area: main
in suites: jessie, jessie-kfreebsd
size: 29,260 kB
ctags: 3,098
sloc: ada: 186,243; cpp: 13,497; makefile: 685; yacc: 440; lex: 176; ansic: 119; sh: 16
file content (5499 lines) | stat: -rw-r--r-- 249,673 bytes
parent folder | download | duplicates (2)
-------------------------------------------------------------------------------
-- (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 Ada.Characters.Latin_1;
with CommandLineData;
with Debug;
with FileSystem;
with ScreenEcho;
with SPARK_XML;
with SP_Relations;
with SystemErrors;
with XMLReport;

use type CommandLineData.Justification_Options;

package body ErrorHandler
--# own Error_Context is Conversions.State,
--#                      Echo_Accumulator,
--#                      ErrorBuffer.Buffer,
--#                      Error_Context_Rec,
--#                      File_Open_Error,
--#                      Potential_Invalid_Value,
--#                      Stop_SLI,
--#                      Total_Error_Count,
--#                      WarningStatus.SuppressionList;
is

   ----------------------------------------------------------------------
   -- Centralized location for wrapper strings used when appending error explanations
   -- to error message strings.  These are used by Conversions and in calls to ErrorAccumulator.Start_Msg

   Explanation_Prefix  : constant String := " [Explanatory note: ";
   Explanation_Postfix : constant String := "]";

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

   --# inherit CommandLineData,
   --#         Dictionary,
   --#         ErrorHandler,
   --#         Error_IO,
   --#         Error_Types,
   --#         ExaminerConstants,
   --#         E_Strings,
   --#         LexTokenManager,
   --#         SPARK_IO,
   --#         SP_Symbols,
   --#         SystemErrors;
   package Conversions
   --# own State;
   --# initializes State;
   is

      procedure ToString
        (Err_Num : in     Error_Types.NumericError;
         Purpose : in     Error_Types.ConversionRequestSource;
         Err_Str :    out Error_Types.StringError);
      --# global in     CommandLineData.Content;
      --#        in     Dictionary.Dict;
      --#        in     LexTokenManager.State;
      --#        in out State;
      --# derives Err_Str from CommandLineData.Content,
      --#                      Dictionary.Dict,
      --#                      Err_Num,
      --#                      LexTokenManager.State,
      --#                      Purpose,
      --#                      State &
      --#         State   from *,
      --#                      CommandLineData.Content,
      --#                      Err_Num,
      --#                      Purpose;

      procedure Output_Reference_List (To_File : in SPARK_IO.File_Type);
      --# global in     CommandLineData.Content;
      --#        in     State;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                CommandLineData.Content,
      --#                                State,
      --#                                To_File;

   end Conversions;

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

   --# inherit CommandLineData,
   --#         Conversions,
   --#         Dictionary,
   --#         ErrorHandler,
   --#         Error_IO,
   --#         Error_Types,
   --#         ExaminerConstants,
   --#         E_Strings,
   --#         LexTokenManager,
   --#         SPARK_IO,
   --#         SP_Symbols,
   --#         SystemErrors;
   package ErrorBuffer
   --# own Buffer;
   --# initializes Buffer;
   is

      -- this is a generic add routines called by more closely focussed procedure
      procedure Add
        (Err_File            : in out Error_IO.File_Type;
         Err_Type            : in     Error_Types.Error_Class;
         Pos                 : in     LexTokenManager.Token_Position;
         Scope               : in     Dictionary.Scopes;
         Error_Number        : in     Natural;
         Reference           : in     Natural;
         Name1, Name2, Name3 : in     Error_Types.Names;
         Echo_Str            :    out Error_Types.StringError);
      --# global in     CommandLineData.Content;
      --#        in     Dictionary.Dict;
      --#        in     LexTokenManager.State;
      --#        in out Buffer;
      --#        in out Conversions.State;
      --#        in out SPARK_IO.File_Sys;
      --# derives Buffer            from *,
      --#                                CommandLineData.Content,
      --#                                Dictionary.Dict,
      --#                                Error_Number,
      --#                                Err_Type,
      --#                                Name1,
      --#                                Name2,
      --#                                Name3,
      --#                                Pos,
      --#                                Reference,
      --#                                Scope &
      --#         Conversions.State from *,
      --#                                Buffer,
      --#                                CommandLineData.Content,
      --#                                Error_Number,
      --#                                Err_Type,
      --#                                Name1,
      --#                                Name2,
      --#                                Name3,
      --#                                Pos,
      --#                                Reference,
      --#                                Scope &
      --#         Echo_Str          from Buffer,
      --#                                CommandLineData.Content,
      --#                                Conversions.State,
      --#                                Dictionary.Dict,
      --#                                Error_Number,
      --#                                Err_Type,
      --#                                LexTokenManager.State,
      --#                                Name1,
      --#                                Name2,
      --#                                Name3,
      --#                                Pos,
      --#                                Reference,
      --#                                Scope &
      --#         Err_File          from *,
      --#                                Buffer,
      --#                                CommandLineData.Content,
      --#                                Error_Number,
      --#                                Err_Type,
      --#                                Name1,
      --#                                Name2,
      --#                                Name3,
      --#                                Pos,
      --#                                Reference,
      --#                                Scope,
      --#                                SPARK_IO.File_Sys &
      --#         SPARK_IO.File_Sys from *,
      --#                                Buffer,
      --#                                CommandLineData.Content,
      --#                                Dictionary.Dict,
      --#                                Error_Number,
      --#                                Err_File,
      --#                                Err_Type,
      --#                                Name1,
      --#                                Name2,
      --#                                Name3,
      --#                                Pos,
      --#                                Reference,
      --#                                Scope;

      procedure Flush (Err_File : in out Error_IO.File_Type);
      --# global in     Dictionary.Dict;
      --#        in out Buffer;
      --#        in out SPARK_IO.File_Sys;
      --# derives Buffer            from * &
      --#         Err_File          from *,
      --#                                Buffer,
      --#                                SPARK_IO.File_Sys &
      --#         SPARK_IO.File_Sys from *,
      --#                                Buffer,
      --#                                Dictionary.Dict,
      --#                                Err_File;

   end ErrorBuffer;

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

   -- This package provides a list of justification (accept) annotations found in the
   -- code.  When errors are added, the list can be consulted to see whether the error
   -- should be displayed or not.  The table is populated for the file currently being examined,
   -- when the error context changes, the table contents are saved to a temorary file (or memory-based
   -- simulation of such a file) so that we can list all the justifications in the report and listing files.

   --# inherit CommandLineData,
   --#         Dictionary,
   --#         ErrorHandler,
   --#         E_Strings,
   --#         LexTokenManager,
   --#         SPARK_IO,
   --#         SPARK_XML,
   --#         SystemErrors,
   --#         XMLReport;
   package Justifications is
      type Unmatched_Justification_Iterator is private;

      procedure Start_Unit (Which_Table : in out ErrorHandler.Justifications_Data_Tables);
      --# derives Which_Table from *;

      procedure Set_Current_Unit_Has_Semantic_Errors (Which_Table : in out ErrorHandler.Justifications_Data_Tables);
      --# derives Which_Table from *;

      procedure First_Unmatched_Justification
        (It          :    out Unmatched_Justification_Iterator;
         Which_Table : in     ErrorHandler.Justifications_Data_Tables);
      --# global in CommandLineData.Content;
      --# derives It from CommandLineData.Content,
      --#                 Which_Table;

      procedure Next_Unmatched_Justification
        (It          : in out Unmatched_Justification_Iterator;
         Which_Table : in     ErrorHandler.Justifications_Data_Tables);
      --# global in CommandLineData.Content;
      --# derives It from *,
      --#                 CommandLineData.Content,
      --#                 Which_Table;

      function Error_Position (It : Unmatched_Justification_Iterator) return LexTokenManager.Token_Position;

      function Is_Null_Iterator (It : Unmatched_Justification_Iterator) return Boolean;

      procedure End_Unit (Which_Table : in out ErrorHandler.Justifications_Data_Tables);
      --# derives Which_Table from *;

      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);
      --# derives Maximum_Justifications_Reached from Which_Table &
      --#         Which_Table                    from *,
      --#                                             Applies_To_All,
      --#                                             Err_Num,
      --#                                             Explanation,
      --#                                             Identifiers,
      --#                                             Kind,
      --#                                             Line,
      --#                                             Position;

      procedure End_Justification
        (Which_Table   : in out ErrorHandler.Justifications_Data_Tables;
         Line          : in     LexTokenManager.Line_Numbers;
         Unmatched_End :    out Boolean);
      --# derives Unmatched_End,
      --#         Which_Table   from Line,
      --#                            Which_Table;

      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);
      --# global in CommandLineData.Content;
      --#        in LexTokenManager.State;
      --# derives Match_Found,
      --#         Which_Table from CommandLineData.Content,
      --#                          Err_Num,
      --#                          Identifiers,
      --#                          Kind,
      --#                          LexTokenManager.State,
      --#                          Line,
      --#                          Which_Table;

      procedure Print_Justifications (Which_Table : in ErrorHandler.Justifications_Data_Tables;
                                      File        : in SPARK_IO.File_Type);
      --# global in     CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                CommandLineData.Content,
      --#                                File,
      --#                                Which_Table;

      procedure Print_Justifications_XML
        (Which_Table : in ErrorHandler.Justifications_Data_Tables;
         File        : in SPARK_IO.File_Type);
      --# global in     CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --#        in out XMLReport.State;
      --# derives SPARK_IO.File_Sys from *,
      --#                                CommandLineData.Content,
      --#                                File,
      --#                                Which_Table,
      --#                                XMLReport.State &
      --#         XMLReport.State   from *,
      --#                                CommandLineData.Content,
      --#                                Which_Table;
   private
      type Unmatched_Justification_Iterator is record
         Current_Table_Entry : ErrorHandler.Data_Table_Ptr;
         Current_Position    : LexTokenManager.Token_Position;
      end record;
   end Justifications;

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

   --# inherit Ada.Characters.Handling,
   --#         Ada.Characters.Latin_1,
   --#         CommandLineData,
   --#         CommandLineHandler,
   --#         ErrorHandler,
   --#         ExaminerConstants,
   --#         E_Strings,
   --#         FileSystem,
   --#         LexTokenManager,
   --#         ScreenEcho,
   --#         SPARK_IO,
   --#         SystemErrors,
   --#         XMLReport;
   package WarningStatus
   --# own SuppressionList;
   --# initializes SuppressionList;
   is
      procedure ReadWarningFile;
      --# global in     CommandLineData.Content;
      --#        in out ErrorHandler.File_Open_Error;
      --#        in out LexTokenManager.State;
      --#        in out SPARK_IO.File_Sys;
      --#        in out SuppressionList;
      --# derives ErrorHandler.File_Open_Error from *,
      --#                                           CommandLineData.Content,
      --#                                           SPARK_IO.File_Sys &
      --#         LexTokenManager.State,
      --#         SPARK_IO.File_Sys,
      --#         SuppressionList              from CommandLineData.Content,
      --#                                           LexTokenManager.State,
      --#                                           SPARK_IO.File_Sys,
      --#                                           SuppressionList;

      function Is_Suppressed (The_Element : ErrorHandler.Warning_Elements) return Boolean;
      --# global in SuppressionList;
      function Pragma_Is_Suppressed (Pragma_Name : LexTokenManager.Lex_String) return Boolean;
      --# global in LexTokenManager.State;
      --#        in SuppressionList;

      procedure Output_Warning_List (To_File : in SPARK_IO.File_Type);
      --# global in     CommandLineData.Content;
      --#        in     LexTokenManager.State;
      --#        in     SuppressionList;
      --#        in out SPARK_IO.File_Sys;
      --#        in out XMLReport.State;
      --# derives SPARK_IO.File_Sys from *,
      --#                                CommandLineData.Content,
      --#                                LexTokenManager.State,
      --#                                SuppressionList,
      --#                                To_File,
      --#                                XMLReport.State &
      --#         XMLReport.State   from *,
      --#                                CommandLineData.Content,
      --#                                SuppressionList;

      procedure Report_Suppressed_Warnings (To_File : in SPARK_IO.File_Type;
                                            Counter : in ErrorHandler.Counters);
      --# global in     SuppressionList;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Counter,
      --#                                SuppressionList,
      --#                                To_File;

   end WarningStatus;

   ----------------------------------------------------------------------
   Stmt_Width            : constant Positive := 4;
   Source_Line_Indent    : constant Positive := 6;
   Error_Line_Length     : constant Positive := 80;
   XML_Error_Line_Length : constant Positive := 256;

   subtype Error_Set_Lengths is Natural range 0 .. ExaminerConstants.MaxErrorSetSize;
   subtype Error_Set_Positions is Natural range 1 .. ExaminerConstants.MaxErrorSetSize;
   type Error_Struct is record
      Err_Num : Natural;
      Error   : Error_Types.StringError;
   end record;
   type Error_Array is array (Error_Set_Positions) of Error_Struct;
   type Error_Sets is record
      Length  : Error_Set_Lengths;
      Content : Error_Array;
   end record;

   Empty_Error_Struct : constant Error_Struct := Error_Struct'(0, Error_Types.Empty_StringError);
   Empty_Error_Array  : constant Error_Array  := Error_Array'(Error_Set_Positions => Empty_Error_Struct);
   Empty_Error_Set    : constant Error_Sets   := Error_Sets'(0, Empty_Error_Array);
   ----------------------------------------------------------------------

   --# inherit CommandLineData,
   --#         ErrorHandler,
   --#         Error_Types,
   --#         ExaminerConstants,
   --#         E_Strings,
   --#         SPARK_IO,
   --#         SystemErrors,
   --#         XMLReport;
   package ErrorAccumulator is

      type T is private;

      Clear : constant T;

      function Is_Error_Continuation (The_Error : Error_Types.StringError) return Boolean;

      function Is_Error_Start (The_Error : Error_Types.StringError) return Boolean;

      function Is_Active (This : T) return Boolean;

      procedure Start_Msg
        (This         :    out T;
         Start_Error  : in     ErrorHandler.Error_Struct;
         Start_Indent : in     Natural;
         Explanation  : in     E_Strings.T;
         Line_Length  : in     Natural;
         Indent       : in     Natural);
      --# derives This from Explanation,
      --#                   Indent,
      --#                   Line_Length,
      --#                   Start_Error,
      --#                   Start_Indent;

      procedure Flush (This    : in out T;
                       Listing : in     SPARK_IO.File_Type);
      --# global in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Listing,
      --#                                This &
      --#         This              from *;

      procedure Add
        (This            : in out T;
         Error           : in     ErrorHandler.Error_Struct;
         End_Pos, Indent : in     Natural;
         Listing         : in     SPARK_IO.File_Type);
      --# global in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                End_Pos,
      --#                                Error,
      --#                                Indent,
      --#                                Listing,
      --#                                This &
      --#         This              from *,
      --#                                End_Pos,
      --#                                Error,
      --#                                Indent;
      --#

   private

      type T is record
         Active       : Boolean;
         Start_Error  : ErrorHandler.Error_Struct;
         Start_Indent : Natural;
         -- following fields only concerned with appending explanation to message after Flush operation
         Explanation : E_Strings.T;
         Line_Length : Natural;
         Indent      : Natural;
      end record;

      Clear : constant T :=
        T'
        (Active       => False,
         Start_Error  => ErrorHandler.Empty_Error_Struct,
         Start_Indent => 0,
         Explanation  => E_Strings.Empty_String,
         Line_Length  => 0,
         Indent       => 0);

   end ErrorAccumulator;

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

   Error_Context_Rec       : Error_Contexts;
   Echo_Accumulator        : ErrorAccumulator.T;
   Total_Error_Count       : Total_Error_Counts;
   File_Open_Error         : Boolean := False;
   Stop_SLI                : Boolean := False;
   Potential_Invalid_Value : Boolean := False;
   ----------------------------------------------------------------------

   function Dependency_Err_Number (Err_Type : Full_Depend_Err_Type) return Natural is
      Result : Natural;
   begin
      case Err_Type is
         -- Unconditional dependency errors
         when Not_Used | Not_Used_New | Not_Used_Continue | Ineff_Init | Ineff_Local_Init | Policy_Violation =>
            Result := Dependency_Err_Type'Pos (Err_Type) + Error_Types.UncondDependencyErrorOffset;
            -- Conditional dependency errors
         when May_Be_Used                |
           May_Be_Used_New            |
           May_Be_Used_Continue       |
           Uninitialised              |
           Integrity_Violation        |
           May_Be_Integrity_Violation =>
            Result := Dependency_Err_Type'Pos (Err_Type) + Error_Types.CondDependencyErrorOffset;
      end case;
      return Result;
   end Dependency_Err_Number;

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

   package body Conversions is separate;

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

   package body ErrorBuffer is separate;

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

   package body WarningStatus is separate;

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

   package body Justifications is separate;

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

   function Symbol_To_Justification_Identifier (Sym : Dictionary.Symbol) return Justification_Identifier is
   begin
      return Justification_Identifier'(String_Form => LexTokenManager.Null_String,
                                       Symbol_Form => Sym);
   end Symbol_To_Justification_Identifier;

   function Lex_Str_To_Justification_Identifier (Str : LexTokenManager.Lex_String) return Justification_Identifier is
   begin
      return Justification_Identifier'(String_Form => Str,
                                       Symbol_Form => Dictionary.NullSymbol);
   end Lex_Str_To_Justification_Identifier;

   procedure Read_Warning_File
   --# global in     CommandLineData.Content;
   --#        in out File_Open_Error;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out WarningStatus.SuppressionList;
   --# derives File_Open_Error               from *,
   --#                                            CommandLineData.Content,
   --#                                            SPARK_IO.File_Sys &
   --#         LexTokenManager.State,
   --#         SPARK_IO.File_Sys,
   --#         WarningStatus.SuppressionList from CommandLineData.Content,
   --#                                            LexTokenManager.State,
   --#                                            SPARK_IO.File_Sys,
   --#                                            WarningStatus.SuppressionList;
   is
   begin
      WarningStatus.ReadWarningFile;
   end Read_Warning_File;

   procedure Output_Warning_List (To_File : in SPARK_IO.File_Type)
   --# global in     CommandLineData.Content;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out SPARK_IO.File_Sys;
   --#        in out XMLReport.State;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                LexTokenManager.State,
   --#                                To_File,
   --#                                WarningStatus.SuppressionList,
   --#                                XMLReport.State &
   --#         XMLReport.State   from *,
   --#                                CommandLineData.Content,
   --#                                WarningStatus.SuppressionList;
   is
   begin
      WarningStatus.Output_Warning_List (To_File => To_File);
   end Output_Warning_List;

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

   procedure Output_Reference_List (To_File : in SPARK_IO.File_Type)
   --# global in     CommandLineData.Content;
   --#        in     Conversions.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Conversions.State,
   --#                                To_File;
   is
   begin
      Conversions.Output_Reference_List (To_File => To_File);
   end Output_Reference_List;

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

   function Lex_String_To_Name (Str : LexTokenManager.Lex_String) return Error_Types.Names
   --# global in LexTokenManager.State;
   is
      Result : Error_Types.Names;
   begin
      if LexTokenManager.Lex_String_Case_Insensitive_Compare (Lex_Str1 => Str,
                                                              Lex_Str2 => LexTokenManager.Null_String) =
        LexTokenManager.Str_Eq then
         Result := Error_Types.NoName;
      elsif LexTokenManager.Lex_String_Case_Insensitive_Compare (Lex_Str1 => Str,
                                                                 Lex_Str2 => LexTokenManager.Main_Program_Token) =
        LexTokenManager.Str_Eq then
         Result := Error_Types.ThePartitionName;
      else
         Result :=
           Error_Types.Names'(Name_Sort => Error_Types.LexString,
                              Name_Sym  => Dictionary.NullSymbol,
                              Name_Str  => Str,
                              Pos       => 0);
      end if;
      return Result;
   end Lex_String_To_Name;

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

   function Symbol_To_Name (Sym : Dictionary.Symbol) return Error_Types.Names is
      Result : Error_Types.Names;
   begin
      if Dictionary.Is_Null_Symbol (Sym) then
         Result := Error_Types.NoName;
      else
         Result :=
           Error_Types.Names'(Name_Sort => Error_Types.Symbol,
                              Name_Sym  => Sym,
                              Name_Str  => LexTokenManager.Null_String,
                              Pos       => 0);
      end if;
      return Result;
   end Symbol_To_Name;

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

   function SP_Symbol_To_Name (Sym : SP_Symbols.SP_Symbol) return Error_Types.Names is
   begin
      return Error_Types.Names'
        (Name_Sort => Error_Types.ParserSymbol,
         Name_Sym  => Dictionary.NullSymbol,
         Name_Str  => LexTokenManager.Null_String,
         Pos       => SP_Symbols.SP_Symbol'Pos (Sym));
   end SP_Symbol_To_Name;

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

   procedure Append_String (E_Str : in out Error_Types.StringError;
                            Str   : in     String)
   --# derives E_Str from *,
   --#                    Str;
   is
      pragma Inline (Append_String);
   begin
      E_Strings.Append_String (E_Str => E_Str.Message,
                               Str   => Str);
   end Append_String;

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

   procedure AppendSym (Error : in out Error_Types.StringError;
                        Sym   : in     SP_Symbols.SP_Symbol)
   --# derives Error from *,
   --#                    Sym;
      is separate;

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

   procedure Append_Lex_String (E_Str : in out Error_Types.StringError;
                                L_Str : in     LexTokenManager.Lex_String)
   --# global in LexTokenManager.State;
   --# derives E_Str from *,
   --#                    LexTokenManager.State,
   --#                    L_Str;
   is
      pragma Inline (Append_Lex_String);
   begin
      E_Strings.Append_Examiner_String
        (E_Str1 => E_Str.Message,
         E_Str2 => LexTokenManager.Lex_String_To_String (Lex_Str => L_Str));
   end Append_Lex_String;
   pragma Unreferenced (Append_Lex_String); -- unused at present

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

   procedure Set_Col (File : in SPARK_IO.File_Type;
                      Posn : in Positive)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                File,
   --#                                Posn;
   is
      pragma Inline (Set_Col);
   begin
      if File = SPARK_IO.Standard_Output then
         ScreenEcho.Set_Col (Posn);
      else
         SPARK_IO.Set_Col (File, Posn);
      end if;
   end Set_Col;

   procedure Put_Char (File : in SPARK_IO.File_Type;
                       Item : in Character)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                File,
   --#                                Item;
   is
      pragma Inline (Put_Char);
   begin
      if File = SPARK_IO.Standard_Output then
         ScreenEcho.Put_Char (Item);
      else
         SPARK_IO.Put_Char (File => File,
                            Item => Item);
      end if;
   end Put_Char;

   procedure Put_Integer
     (File  : in SPARK_IO.File_Type;
      Item  : in Integer;
      Width : in Natural;
      Base  : in SPARK_IO.Number_Base)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Base,
   --#                                File,
   --#                                Item,
   --#                                Width;
   is
      pragma Inline (Put_Integer);
   begin
      if File = SPARK_IO.Standard_Output then
         ScreenEcho.Put_Integer (Item, Width, Base);
      else
         SPARK_IO.Put_Integer (File  => File,
                               Item  => Item,
                               Width => Width,
                               Base  => Base);
      end if;
   end Put_Integer;

   procedure New_Line (File    : in SPARK_IO.File_Type;
                       Spacing : in Positive)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                File,
   --#                                Spacing;
   is
      pragma Inline (New_Line);
   begin
      if File = SPARK_IO.Standard_Output then
         ScreenEcho.New_Line (Spacing);
      else
         SPARK_IO.New_Line (File    => File,
                            Spacing => Spacing);
      end if;
   end New_Line;

   procedure Put_Line (File : in SPARK_IO.File_Type;
                       Item : in String;
                       Stop : in Natural)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                File,
   --#                                Item,
   --#                                Stop;
   is
      pragma Inline (Put_Line);
   begin
      if File = SPARK_IO.Standard_Output then
         ScreenEcho.Put_Line (Item);
      else
         SPARK_IO.Put_Line (File => File,
                            Item => Item,
                            Stop => Stop);
      end if;
   end Put_Line;

   procedure Put_E_String (File  : in SPARK_IO.File_Type;
                           E_Str : in E_Strings.T)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                E_Str,
   --#                                File;
   is
      pragma Inline (Put_E_String);
   begin
      if File = SPARK_IO.Standard_Output then
         ScreenEcho.Put_ExaminerString (E_Str);
      else
         E_Strings.Put_String (File  => File,
                               E_Str => E_Str);
      end if;
   end Put_E_String;
   pragma Unreferenced (Put_E_String); -- unused at present

   procedure Put_E_Line (File  : in SPARK_IO.File_Type;
                         E_Str : in E_Strings.T)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                E_Str,
   --#                                File;
   is
      pragma Inline (Put_E_Line);
   begin
      if File = SPARK_IO.Standard_Output then
         ScreenEcho.Put_ExaminerLine (E_Str);
      else
         E_Strings.Put_Line (File  => File,
                             E_Str => E_Str);
      end if;
   end Put_E_Line;

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

   procedure Put_Spaces (File : in SPARK_IO.File_Type;
                         N    : in Natural)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                File,
   --#                                N;
   is
   begin
      for I in Natural range 1 .. N loop
         Put_Char (File => File,
                   Item => ' ');
      end loop;
   end Put_Spaces;

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

   procedure PrintLine
     (Listing                    : in     SPARK_IO.File_Type;
      Start_Pos, End_Pos, Indent : in     Natural;
      Line                       : in     E_Strings.T;
      Add_New_Line               : in     Boolean;
      New_Start                  :    out Natural)
   --# global in out SPARK_IO.File_Sys;
   --# derives New_Start         from End_Pos,
   --#                                Indent,
   --#                                Line,
   --#                                Start_Pos &
   --#         SPARK_IO.File_Sys from *,
   --#                                Add_New_Line,
   --#                                End_Pos,
   --#                                Indent,
   --#                                Line,
   --#                                Listing,
   --#                                Start_Pos;
      is separate;

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

   package body ErrorAccumulator is separate;

   -----------------------------------------------------------------------------
   -- String utility used in calls to ErrorAccumulator.Start_Msg to remove explanations from
   -- strings being stored in the accumulator so that they can be kept and
   -- printed when the accumulator is flushed

   -- e.g. if "rage, rage against the dying of the light [Explanatory note: by Dylan Thomas]" is passed
   -- in in Estr and ErrorHandlerError.Prefix is set to " [Explanatory note: " then after the call,
   -- Estr has "rage, rage against the dying of the light" and
   -- Explanation has " [Explanatory note: by Dylan Thomas]"

   -- If there is no match for ErrorHandlerError.Prefix then E_Str is unchanged and Explanation
   -- is the EmptyString;

   procedure Split_String_At_Explanation (E_Str       : in out E_Strings.T;
                                          Explanation :    out E_Strings.T)
   --# derives Explanation,
   --#         E_Str       from E_Str;
   is
      Start_Point : Natural;
      Found_It    : Boolean;
   begin
      E_Strings.Find_Sub_String
        (E_Str         => E_Str,
         Search_String => Explanation_Prefix,
         String_Found  => Found_It,
         String_Start  => Start_Point);
      if Found_It then
         Explanation :=
           E_Strings.Section
           (E_Str     => E_Str,
            Start_Pos => Start_Point,
            Length    => (E_Strings.Get_Length (E_Str => E_Str) - Start_Point) + 1);
         -- truncate E_Str to remove Explanation
         E_Str := E_Strings.Section (E_Str     => E_Str,
                                     Start_Pos => 1,
                                     Length    => Start_Point - 1);
      else
         Explanation := E_Strings.Empty_String;
      end if;
   end Split_String_At_Explanation; -- one DF error reported on Explanation.Content

   -----------------------------------------------------------------------------
   procedure Flush_Buffer
   --# global in     Dictionary.Dict;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --# derives ErrorBuffer.Buffer from * &
   --#         Error_Context_Rec  from *,
   --#                                 ErrorBuffer.Buffer,
   --#                                 SPARK_IO.File_Sys &
   --#         SPARK_IO.File_Sys  from *,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec;
   is
      Err_File : Error_IO.File_Type;
   begin
      Err_File := Error_Context_Rec.Errs;
      ErrorBuffer.Flush (Err_File => Err_File);
      Error_Context_Rec.Errs := Err_File;
   end Flush_Buffer;

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

   procedure Inc_Total_Justified_Warnings
   --# global in out Total_Error_Count;
   --# derives Total_Error_Count from *;
   is
   begin
      if Total_Error_Count.Justified_Warnings = Count'Last then
         SystemErrors.Fatal_Error (Sys_Err => SystemErrors.Too_Many_Errors,
                                   Msg     => "");
      end if;
      Total_Error_Count.Justified_Warnings := Total_Error_Count.Justified_Warnings + 1;
   end Inc_Total_Justified_Warnings;

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

   procedure Echo_Total_Error_Count
   --# global in     CommandLineData.Content;
   --#        in     Total_Error_Count;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Total_Error_Count;
   is
      procedure Indent
      --# global in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *;
      is
      begin
         ScreenEcho.Put_String ("     ");
      end Indent;

      procedure End_Line (Is_Plural : in Boolean)
      --# global in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Is_Plural;
      is
      begin
         if Is_Plural then
            ScreenEcho.Put_Line ("s");
         else
            ScreenEcho.New_Line (1);
         end if;
      end End_Line;

   begin -- Echo_Total_Error_Count
      if CommandLineData.Content.Echo and not CommandLineData.Content.Makefile_Mode then
         ScreenEcho.New_Line (1);

         -- Explicit and summarized warnings are handled separately
         -- First explicit counts
         if Total_Error_Count.Grand_Total = 0 then
            ScreenEcho.Put_Line ("   No errors or warnings");
         else
            ScreenEcho.Put_Integer (Integer (Total_Error_Count.Grand_Total), 5, 10);
            if Total_Error_Count.Grand_Total > 1 then
               ScreenEcho.Put_Line (" errors or warnings, comprising:");
            else
               ScreenEcho.Put_Line (" error or warning, comprising:");
            end if;
            -- List subtotals by category
            if Total_Error_Count.Explicit_Error_Count (Syntax_Or_Semantic) > 0 then
               Indent;
               ScreenEcho.Put_Integer (Integer (Total_Error_Count.Explicit_Error_Count (Syntax_Or_Semantic)), 5, 10);
               ScreenEcho.Put_String (" syntax or semantic error");
               End_Line (Is_Plural => Total_Error_Count.Explicit_Error_Count (Syntax_Or_Semantic) > 1);
            end if;
            if Total_Error_Count.Explicit_Error_Count (Flow) > 0 then
               Indent;
               ScreenEcho.Put_Integer (Integer (Total_Error_Count.Explicit_Error_Count (Flow)), 5, 10);
               ScreenEcho.Put_String (" flow error");
               End_Line (Is_Plural => Total_Error_Count.Explicit_Error_Count (Flow) > 1);
            end if;
            if Total_Error_Count.Explicit_Error_Count (Warning) > 0 then
               Indent;
               ScreenEcho.Put_Integer (Integer (Total_Error_Count.Explicit_Error_Count (Warning)), 5, 10);
               ScreenEcho.Put_String (" warning");
               End_Line (Is_Plural => Total_Error_Count.Explicit_Error_Count (Warning) > 1);
            end if;
         end if;

         -- Then append summary of suppressed warnings (say nothing at all if total is 0)
         if Total_Error_Count.Suppressed_Warnings > 0 then
            ScreenEcho.Put_Integer (Integer (Total_Error_Count.Suppressed_Warnings), 5, 10);
            ScreenEcho.Put_String (" summarized warning");
            End_Line (Is_Plural => Total_Error_Count.Suppressed_Warnings > 1);
         end if;

         -- Then append summary of justified warnings (say nothing at all if total is 0)
         if Total_Error_Count.Justified_Warnings > 0 then
            ScreenEcho.Put_Integer (Integer (Total_Error_Count.Justified_Warnings), 5, 10);
            ScreenEcho.Put_String (" expected (justified) warning");
            End_Line (Is_Plural => Total_Error_Count.Justified_Warnings > 1);
         end if;
      end if;
   end Echo_Total_Error_Count;

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

   procedure Inc_Message_Count (Err_Type : in Error_Types.Error_Class)
   --# global in out Error_Context_Rec;
   --#        in out Total_Error_Count;
   --# derives Error_Context_Rec,
   --#         Total_Error_Count from *,
   --#                                Err_Type;
   is

      procedure Inc_Total_Errors_Or_Warnings (Kind : in Counted_Error_Kinds)
      --# global in out Total_Error_Count;
      --# derives Total_Error_Count from *,
      --#                                Kind;
      is
      begin
         if Total_Error_Count.Grand_Total = Count'Last then
            SystemErrors.Fatal_Error (Sys_Err => SystemErrors.Too_Many_Errors,
                                      Msg     => "");
         end if;
         Total_Error_Count.Grand_Total := Total_Error_Count.Grand_Total + 1;
         -- We don't need to guard the following increment because a subtotal can't
         -- overflow without the grand total (tested above) overflowing first
         Total_Error_Count.Explicit_Error_Count (Kind) := Total_Error_Count.Explicit_Error_Count (Kind) + 1;
      end Inc_Total_Errors_Or_Warnings;

   begin
      if Error_Context_Rec.Num_Message = Count'Last then
         SystemErrors.Fatal_Error (Sys_Err => SystemErrors.Too_Many_Errors,
                                   Msg     => "");
      end if;
      Error_Context_Rec.Num_Message := Error_Context_Rec.Num_Message + 1;
      if Err_Type /= Error_Types.NoErr then
         if Error_Context_Rec.Num_Errs = Count'Last then
            SystemErrors.Fatal_Error (Sys_Err => SystemErrors.Too_Many_Errors,
                                      Msg     => "");
         end if;
         Error_Context_Rec.Num_Errs := Error_Context_Rec.Num_Errs + 1;
      end if;
      -- Above lines maintain counts of errors per unit in the current ErrorContext record.

      -- We also need to maintain grand totals (in various subcategories) thus:
      case Err_Type is
         when Error_Types.LexErr | Error_Types.SyntaxErr | Error_Types.SyntaxRec | Error_Types.SemanticErr =>
            Inc_Total_Errors_Or_Warnings (Kind => Syntax_Or_Semantic);
         when Error_Types.UncondFlowErr       |
           Error_Types.CondlFlowErr        |
           Error_Types.UncondDependencyErr |
           Error_Types.CondlDependencyErr  |
           Error_Types.DepSemanticErr      |  -- refinement inconsistency, treat as a flow error
           Error_Types.ControlFlowErr      |
           Error_Types.IneffectiveStat     |
           Error_Types.StabilityErr        |
           Error_Types.UsageErr            =>
            Inc_Total_Errors_Or_Warnings (Kind => Flow);
         when Error_Types.WarningWithPosition | Error_Types.WarningWithoutPosition | Error_Types.Note =>
            Inc_Total_Errors_Or_Warnings (Kind => Warning);
         when Error_Types.NoErr =>
            null;
      end case;
   end Inc_Message_Count;

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

   procedure Inc_Suppressed_Warning_Counter (Warning_Type : in Warning_Elements)
   --# global in out Error_Context_Rec;
   --#        in out Total_Error_Count;
   --# derives Error_Context_Rec from *,
   --#                                Warning_Type &
   --#         Total_Error_Count from *;
   is

      procedure Inc_Total_Suppressed_Warnings
      --# global in out Total_Error_Count;
      --# derives Total_Error_Count from *;
      is
      begin
         if Total_Error_Count.Suppressed_Warnings = Count'Last then
            SystemErrors.Fatal_Error (Sys_Err => SystemErrors.Too_Many_Errors,
                                      Msg     => "");
         end if;
         Total_Error_Count.Suppressed_Warnings := Total_Error_Count.Suppressed_Warnings + 1;
      end Inc_Total_Suppressed_Warnings;

   begin
      if Error_Context_Rec.Counter (Warning_Type) = Count'Last then
         SystemErrors.Fatal_Error (Sys_Err => SystemErrors.Too_Many_Suppressed_Warnings,
                                   Msg     => "");
      end if;
      Error_Context_Rec.Counter (Warning_Type) := Error_Context_Rec.Counter (Warning_Type) + 1;
      Inc_Total_Suppressed_Warnings; -- above is per file, per kind count; this one is grand total
   end Inc_Suppressed_Warning_Counter;

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

   procedure Move_To_Indent
     (Source_File : in SPARK_IO.File_Type;
      Line        : in E_Strings.T;
      Indent      : in Natural;
      Position    : in Integer)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Indent,
   --#                                Line,
   --#                                Position,
   --#                                Source_File;
   is
      Limit : Integer;
   begin
      Put_Spaces (File => Source_File,
                  N    => Indent);
      if Position > E_Strings.Get_Length (E_Str => Line) then
         Limit := E_Strings.Get_Length (E_Str => Line);
      else
         Limit := Position;
      end if;
      for I in Natural range 1 .. Limit loop
         if E_Strings.Get_Element (E_Str => Line,
                                   Pos   => I) = Ada.Characters.Latin_1.HT then
            Put_Char (File => Source_File,
                      Item => Ada.Characters.Latin_1.HT);
         else
            Put_Char (File => Source_File,
                      Item => ' ');
         end if;
      end loop;
      for i in Natural range 1 .. Position - Limit loop
         Put_Char (File => Source_File,
                   Item => ' ');
      end loop;
   end Move_To_Indent;

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

   procedure GetFileLine
   --# global in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context_Rec,
   --#         SPARK_IO.File_Sys from Error_Context_Rec,
   --#                                SPARK_IO.File_Sys;
      is separate;

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

   procedure Print_Source_Line (To_File : in SPARK_IO.File_Type)
   --# global in     CommandLineData.Content;
   --#        in     Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Error_Context_Rec,
   --#                                To_File;
   is
   begin
      if not CommandLineData.Content.Plain_Output then
         Put_Integer (File  => To_File,
                      Item  => Integer (Error_Context_Rec.Line_No),
                      Width => Stmt_Width,
                      Base  => 10);
      end if;

      Set_Col (File => To_File,
               Posn => Source_Line_Indent + 1);
      Put_E_Line (File  => To_File,
                  E_Str => Error_Context_Rec.Current_Line);
   end Print_Source_Line;

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

   function Error_Has_Position_Inline (Err_Type : in Error_Types.Error_Class) return Boolean is
   begin
      return not (Err_Type = Error_Types.UncondDependencyErr or
                    Err_Type = Error_Types.NoErr or
                    Err_Type = Error_Types.CondlDependencyErr or
                    Err_Type = Error_Types.DepSemanticErr or
                    Err_Type = Error_Types.UsageErr or
                    Err_Type = Error_Types.Note or
                    Err_Type = Error_Types.WarningWithoutPosition);
   end Error_Has_Position_Inline;

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

   function Convert_Message_Id (Message_Id : Natural;
                                Err_Type   : Error_Types.Error_Class) return Natural is
      Id : Natural;
   begin
      case Err_Type is
         when Error_Types.CondlDependencyErr =>
            if Message_Id = Dependency_Err_Number (May_Be_Used_New) then
               Id := Dependency_Err_Number (May_Be_Used);
            else
               Id := Message_Id;
            end if;
         when Error_Types.UncondDependencyErr =>
            if Message_Id = Dependency_Err_Number (Not_Used_New) then
               Id := Dependency_Err_Number (Not_Used);
            else
               Id := Message_Id;
            end if;
         when others =>
            Id := Message_Id;
      end case;
      return Id;
   end Convert_Message_Id;

   procedure Put_Message_Id (File       : in SPARK_IO.File_Type;
                             Message_Id : in Natural;
                             Err_Type   : in Error_Types.Error_Class)
   --# global in     CommandLineData.Content;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Err_Type,
   --#                                File,
   --#                                Message_Id;
   is
   begin
      if Message_Id = 0 then
         SPARK_IO.Put_Char (File => File,
                            Item => ' ');
      else
         SPARK_IO.Put_Integer
           (File  => File,
            Item  => Convert_Message_Id (Message_Id => Message_Id,
                                         Err_Type   => Err_Type),
            Width => 3,
            Base  => 10);
         if CommandLineData.Content.Brief then
            SPARK_IO.Put_String (File => File,
                                 Item => " - ",
                                 Stop => 0);
         else
            SPARK_IO.Put_String (File => File,
                                 Item => ": ",
                                 Stop => 0);
         end if;
      end if;
   end Put_Message_Id;

   function Get_Error_Class (Err_Class : in Error_Types.Error_Class) return E_Strings.T is
      Tmp_String : E_Strings.T;
   begin
      case Err_Class is
         when Error_Types.LexErr =>
            Tmp_String := E_Strings.Copy_String (Str => "Lexical Error");
         when Error_Types.SyntaxErr =>
            Tmp_String := E_Strings.Copy_String (Str => "Syntax Error");
         when Error_Types.SyntaxRec =>
            Tmp_String := E_Strings.Copy_String (Str => "Syntax Recovery");
         when Error_Types.SemanticErr =>
            Tmp_String := E_Strings.Copy_String (Str => "Semantic Error");
         when Error_Types.ControlFlowErr =>
            Tmp_String := E_Strings.Copy_String (Str => "Illegal Structure");
         when Error_Types.UncondFlowErr       |
           Error_Types.UncondDependencyErr |
           Error_Types.IneffectiveStat     |
           Error_Types.StabilityErr        |
           Error_Types.UsageErr            |
           Error_Types.DepSemanticErr      =>
            Tmp_String := E_Strings.Copy_String (Str => "Flow Error");
         when Error_Types.CondlFlowErr           |
           Error_Types.CondlDependencyErr     |
           Error_Types.WarningWithPosition    |
           Error_Types.WarningWithoutPosition =>
            Tmp_String := E_Strings.Copy_String (Str => "Warning");
         when Error_Types.Note =>
            Tmp_String := E_Strings.Copy_String (Str => "Note");
         when Error_Types.NoErr =>
            Tmp_String := E_Strings.Copy_String (Str => "No Error");
      end case;

      return Tmp_String;
   end Get_Error_Class;

   procedure Output_Error_Marker
     (File       : in SPARK_IO.File_Type;
      Err_Type   : in Error_Types.Error_Class;
      Message_Id : in Natural;
      Err_Count  : in Natural)
   --# global in     CommandLineData.Content;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Err_Count,
   --#                                Err_Type,
   --#                                File,
   --#                                Message_Id;
   is

      procedure Output_Full_Error_Name (File     : in SPARK_IO.File_Type;
                                        Err_Type : in Error_Types.Error_Class)
      --# global in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Err_Type,
      --#                                File;
      is
      begin
         case Err_Type is
            when Error_Types.LexErr =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Lexical Error     :",
                                    Stop => 0);
            when Error_Types.SyntaxErr =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Syntax Error      :",
                                    Stop => 0);
            when Error_Types.SyntaxRec =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Syntax Recovery   :",
                                    Stop => 0);
            when Error_Types.SemanticErr =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Semantic Error    :",
                                    Stop => 0);
            when Error_Types.ControlFlowErr =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Illegal Structure :",
                                    Stop => 0);
            when Error_Types.CondlFlowErr        |
              Error_Types.CondlDependencyErr  |
              Error_Types.UncondFlowErr       |
              Error_Types.UncondDependencyErr |
              Error_Types.IneffectiveStat     |
              Error_Types.StabilityErr        |
              Error_Types.UsageErr            |
              Error_Types.DepSemanticErr      =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Flow Error        :",
                                    Stop => 0);
            when Error_Types.WarningWithPosition | Error_Types.WarningWithoutPosition =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Warning           :",
                                    Stop => 0);
            when Error_Types.Note =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Note              :",
                                    Stop => 0);
            when Error_Types.NoErr =>
               null;
         end case;
      end Output_Full_Error_Name;

      procedure Output_Error_Flash (File     : in SPARK_IO.File_Type;
                                    Err_Type : in Error_Types.Error_Class)
      --# global in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Err_Type,
      --#                                File;
      is
      begin
         case Err_Type is

            when Error_Types.LexErr         |
              Error_Types.SyntaxErr      |
              Error_Types.SyntaxRec      |
              Error_Types.ControlFlowErr |
              Error_Types.SemanticErr    =>
               SPARK_IO.Put_String (File => File,
                                    Item => "***",
                                    Stop => 0);
            when Error_Types.UncondFlowErr       |
              Error_Types.UncondDependencyErr |
              Error_Types.IneffectiveStat     |
              Error_Types.StabilityErr        |
              Error_Types.UsageErr            |
              Error_Types.DepSemanticErr      =>
               SPARK_IO.Put_String (File => File,
                                    Item => "!!!",
                                    Stop => 0);
            when Error_Types.CondlFlowErr | Error_Types.CondlDependencyErr =>
               SPARK_IO.Put_String (File => File,
                                    Item => "???",
                                    Stop => 0);
            when Error_Types.NoErr =>
               SPARK_IO.Put_String (File => File,
                                    Item => "+++        ",
                                    Stop => 0);
            when Error_Types.WarningWithPosition | Error_Types.WarningWithoutPosition | Error_Types.Note =>
               SPARK_IO.Put_String (File => File,
                                    Item => "---",
                                    Stop => 0);
         end case;
      end Output_Error_Flash;

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

      procedure Output_Error_Count (File      : in SPARK_IO.File_Type;
                                    Err_Count : in Natural)
      --# global in     CommandLineData.Content;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                CommandLineData.Content,
      --#                                Err_Count,
      --#                                File;
      is
      begin
         if (Err_Count = 0) or CommandLineData.Content.Plain_Output then
            SPARK_IO.Put_String (File => File,
                                 Item => "        ",
                                 Stop => 0);
         else
            SPARK_IO.Put_String (File => File,
                                 Item => " (",
                                 Stop => 0);
            Put_Integer (File  => File,
                         Item  => Err_Count,
                         Width => 3,
                         Base  => 10);
            SPARK_IO.Put_String (File => File,
                                 Item => ")  ",
                                 Stop => 0);
         end if;
      end Output_Error_Count;

   begin --Output_Error_Marker
      Output_Error_Flash (File     => File,
                          Err_Type => Err_Type);
      if Err_Type /= Error_Types.NoErr then
         Output_Error_Count (File      => File,
                             Err_Count => Err_Count);
         Output_Full_Error_Name (File     => File,
                                 Err_Type => Err_Type);
         Put_Message_Id (File       => File,
                         Message_Id => Message_Id,
                         Err_Type   => Err_Type);
      else
         Output_Full_Error_Name (File     => File,
                                 Err_Type => Err_Type);
      end if;
   end Output_Error_Marker;

   procedure Output_Brief_Error_Marker
     (File       : in SPARK_IO.File_Type;
      Err_Type   : in Error_Types.Error_Class;
      Message_Id : in Natural)
   --# global in     CommandLineData.Content;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Err_Type,
   --#                                File,
   --#                                Message_Id;
   is

      procedure Output_Brief_Error_Name (File     : in SPARK_IO.File_Type;
                                         Err_Type : in Error_Types.Error_Class)
      --# global in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Err_Type,
      --#                                File;
      is
      begin
         case Err_Type is
            when Error_Types.LexErr =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Lexical Error ",
                                    Stop => 0);
            when Error_Types.SyntaxErr =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Syntax Error ",
                                    Stop => 0);
            when Error_Types.SyntaxRec =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Syntax Recovery ",
                                    Stop => 0);
            when Error_Types.SemanticErr =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Semantic Error ",
                                    Stop => 0);
            when Error_Types.ControlFlowErr =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Illegal Structure ",
                                    Stop => 0);
            when Error_Types.CondlFlowErr        |
              Error_Types.CondlDependencyErr  |
              Error_Types.UncondFlowErr       |
              Error_Types.UncondDependencyErr |
              Error_Types.IneffectiveStat     |
              Error_Types.StabilityErr        |
              Error_Types.UsageErr            |
              Error_Types.DepSemanticErr      =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Flow Error ",
                                    Stop => 0);
            when Error_Types.WarningWithPosition | Error_Types.WarningWithoutPosition =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Warning ",
                                    Stop => 0);
            when Error_Types.Note =>
               SPARK_IO.Put_String (File => File,
                                    Item => "Note ",
                                    Stop => 0);
            when Error_Types.NoErr =>
               null;
         end case;
      end Output_Brief_Error_Name;

   begin
      if Err_Type /= Error_Types.NoErr then
         Output_Brief_Error_Name (File     => File,
                                  Err_Type => Err_Type);
         Put_Message_Id (File       => File,
                         Message_Id => Message_Id,
                         Err_Type   => Err_Type);
      end if;
   end Output_Brief_Error_Marker;

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

   procedure EchoErrorEntry (Echo_File : in SPARK_IO.File_Type;
                             Error     : in Error_Types.StringError)
   --# global in     CommandLineData.Content;
   --#        in out Echo_Accumulator;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --# derives Echo_Accumulator  from *,
   --#                                CommandLineData.Content,
   --#                                Error,
   --#                                Error_Context_Rec &
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Echo_Accumulator,
   --#                                Echo_File,
   --#                                Error,
   --#                                Error_Context_Rec,
   --#                                SPARK_IO.File_Sys;
      is separate;

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

   procedure Flush_Echo_Messages
   --# global in out Echo_Accumulator;
   --#        in out SPARK_IO.File_Sys;
   --# derives Echo_Accumulator,
   --#         SPARK_IO.File_Sys from *,
   --#                                Echo_Accumulator;
   is
      Was_Active : Boolean;
   begin
      Was_Active := ErrorAccumulator.Is_Active (This => Echo_Accumulator);
      ErrorAccumulator.Flush (This    => Echo_Accumulator,
                              Listing => SPARK_IO.Standard_Output);
      if Was_Active then
         New_Line (File    => SPARK_IO.Standard_Output,
                   Spacing => 1);
      end if;

   end Flush_Echo_Messages;

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

   procedure Error_Init (Source_File_Name : in E_Strings.T;
                         Echo             : in Boolean)
   --# global in     Dictionary.Dict;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --# derives Echo_Accumulator,
   --#         ErrorBuffer.Buffer from * &
   --#         Error_Context_Rec  from *,
   --#                                 Dictionary.Dict,
   --#                                 Echo,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Source_File_Name,
   --#                                 SPARK_IO.File_Sys &
   --#         SPARK_IO.File_Sys  from *,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Source_File_Name;
   is
      Source_File  : SPARK_IO.File_Type := SPARK_IO.Null_File;
      Err_File     : Error_IO.File_Type := Error_IO.Null_File;
      Success      : SPARK_IO.File_Status;
      OK_Temp_File : Boolean;
      New_Context  : Error_Contexts;
   begin
      Error_IO.Create (Err_File, Success);
      OK_Temp_File := Success = SPARK_IO.Ok;
      if not OK_Temp_File then
         SystemErrors.Fatal_Error (Sys_Err => SystemErrors.Error_Handler_Temporary_Files,
                                   Msg     => "in Error_Init");
      end if;
      New_Context.Errs                      := Err_File;
      New_Context.Line_No                   := 0;
      New_Context.Source_File_Name          := Source_File_Name;
      New_Context.Num_Errs                  := 0;
      New_Context.Num_Message               := 0;
      New_Context.Severity                  := No_Error;
      New_Context.Recovery_Messages         := False;
      New_Context.Echo                      := Echo;
      New_Context.Current_Line              := E_Strings.Empty_String;
      New_Context.Counter                   := Counters'(others => 0);
      New_Context.Source                    := SPARK_IO.Null_File;
      New_Context.Justifications_Data_Table := Empty_Justifications_Data_Table;
      --# accept Flow, 10, Error_Context_Rec, "Flush changes buffer but we need to initialize it anyway";
      Flush_Buffer;
      --# end accept;
      Error_Context_Rec := New_Context;

      FileSystem.Open_Source_File (File   => Source_File,
                                   Name   => Source_File_Name,
                                   Status => Success);

      Error_Context_Rec.Source := Source_File;
      if not (Success = SPARK_IO.Ok) then
         SystemErrors.Fatal_Error (Sys_Err => SystemErrors.Error_Handler_Source,
                                   Msg     => "in Error_Init");
      end if;
      Flush_Echo_Messages;
   end Error_Init;

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

   procedure Spark_Make_Init
   --# global in     Dictionary.Dict;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --# derives Echo_Accumulator,
   --#         ErrorBuffer.Buffer from * &
   --#         Error_Context_Rec  from SPARK_IO.File_Sys &
   --#         SPARK_IO.File_Sys  from *,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec;
   is
      Err_File    : Error_IO.File_Type := Error_IO.Null_File;
      Unused      : SPARK_IO.File_Status;
      New_Context : Error_Contexts;
   begin
      --# accept Flow, 10, Unused, "Design decision not to check file status";
      Error_IO.Create (File   => Err_File,
                       Status => Unused);
      --# end accept;
      New_Context.Errs                      := Err_File;
      New_Context.Line_No                   := 0;
      New_Context.Num_Errs                  := 0;
      New_Context.Num_Message               := 0;
      New_Context.Severity                  := No_Error;
      New_Context.Source_File_Name          := E_Strings.Empty_String;
      New_Context.Recovery_Messages         := False;
      New_Context.Echo                      := False; --Echo;
      New_Context.Current_Line              := E_Strings.Empty_String;
      New_Context.Counter                   := Counters'(others => 0);
      New_Context.Source                    := SPARK_IO.Null_File;
      New_Context.Justifications_Data_Table := Empty_Justifications_Data_Table;

      --# accept Flow, 10, Error_Context_Rec, "Flush changes buffer but we need to initialize it anyway";
      Flush_Buffer;
      --# end accept;
      Error_Context_Rec := New_Context;
      Flush_Echo_Messages;
      --# accept Flow, 33, Unused, "Consequence of earlier deliberate non-use";
   end Spark_Make_Init;

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

   procedure Get_Error_Context (Context : out Error_Contexts)
   --# global in     Dictionary.Dict;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --# derives Context,
   --#         Error_Context_Rec  from ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 SPARK_IO.File_Sys &
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer from * &
   --#         SPARK_IO.File_Sys  from *,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec;
   is
      Source_File : SPARK_IO.File_Type;
      Success     : SPARK_IO.File_Status;
   begin
      Flush_Buffer;
      Source_File := Error_Context_Rec.Source;
      --# accept Flow, 10, Success, "Intentional non use of file return code";
      SPARK_IO.Close (Source_File, Success);
      --# end accept;
      Error_Context_Rec.Source := Source_File;
      Context                  := Error_Context_Rec;
      Flush_Echo_Messages;
      --# accept Flow, 33, Success, "Consequence of earlier non-use";
   end Get_Error_Context;

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

   procedure Set_Error_Context (Context : in Error_Contexts)
   --# global in     Dictionary.Dict;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --# derives Echo_Accumulator,
   --#         ErrorBuffer.Buffer from * &
   --#         Error_Context_Rec  from *,
   --#                                 Context,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 SPARK_IO.File_Sys &
   --#         SPARK_IO.File_Sys  from *,
   --#                                 Context,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec;
   is
      Success     : SPARK_IO.File_Status;
      Source_File : SPARK_IO.File_Type;
   begin
      --# accept Flow, 10, Error_Context_Rec, "Flush changes buffer but we need to initialize it anyway";
      Flush_Buffer;
      --# end accept;
      Error_Context_Rec := Context;
      Source_File       := Error_Context_Rec.Source;

      --# accept Flow, 10, Success, "Intentional non use of file return code";
      FileSystem.Open_Source_File (File   => Source_File,
                                   Name   => Error_Context_Rec.Source_File_Name,
                                   Status => Success);
      --# end accept;

      Error_Context_Rec.Source       := Source_File;
      Error_Context_Rec.Line_No      := 0;
      Error_Context_Rec.Current_Line := E_Strings.Empty_String;
      Flush_Echo_Messages;
      --# accept Flow, 33, Success, "Consequence of earlier non-use";
   end Set_Error_Context;

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

   procedure Error_Reset
   --# global in out Error_Context_Rec;
   --#           out Potential_Invalid_Value;
   --# derives Error_Context_Rec       from * &
   --#         Potential_Invalid_Value from ;
   is
   begin
      Error_Context_Rec.Severity := No_Error;
      Potential_Invalid_Value    := False;
   end Error_Reset;

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

   procedure Get_Error_Severity (Severity : out Error_Level)
   --# global in Error_Context_Rec;
   --# derives Severity from Error_Context_Rec;
   is
   begin
      Severity := Error_Context_Rec.Severity;
   end Get_Error_Severity;

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

   function Syntax_Or_Semantic_Error return Boolean
   --# global in Total_Error_Count;
   is
   begin
      return Total_Error_Count.Explicit_Error_Count (Syntax_Or_Semantic) /= 0;
   end Syntax_Or_Semantic_Error;

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

   function Possibly_Invalid_Values return Boolean
   --# global in Potential_Invalid_Value;
   is
   begin
      return Potential_Invalid_Value;
   end Possibly_Invalid_Values;

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

   function Generate_SLI return Boolean
   --# global in CommandLineData.Content;
   --#        in Stop_SLI;
   is
   begin
      return CommandLineData.Content.Generate_SLI and then not Stop_SLI;
   end Generate_SLI;

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

   procedure Report_Success
     (Position    : in LexTokenManager.Token_Position;
      Subprog_Str : in LexTokenManager.Lex_String;
      Err_Num     : in Error_Types.ErrNumRange)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Err_Num,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Subprog_Str &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Num,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 SPARK_IO.File_Sys,
   --#                                 Subprog_Str &
   --#         Total_Error_Count  from *;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      Inc_Message_Count (Err_Type => Error_Types.NoErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.NoErr,
         Pos          => Position,
         Scope        => Dictionary.GlobalScope,
         Error_Number => Err_Num,
         Reference    => No_Reference,
         Name1        => Lex_String_To_Name (Str => Subprog_Str),
         Name2        => Error_Types.NoName,
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;

      -- In "Brief" mode we don't echo success messages, since an
      -- IDE like GPS would interpret them as "errors", which they
      -- aren't!
      if not CommandLineData.Content.Brief then
         EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      end if;
   end Report_Success;

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

   procedure Hidden_Text
     (Position : in LexTokenManager.Token_Position;
      Unit_Str : in LexTokenManager.Lex_String;
      Unit_Typ : in SP_Symbols.SP_Symbol)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Unit_Str,
   --#                                 Unit_Typ,
   --#                                 WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 SPARK_IO.File_Sys,
   --#                                 Unit_Str,
   --#                                 Unit_Typ,
   --#                                 WarningStatus.SuppressionList &
   --#         Total_Error_Count  from *,
   --#                                 CommandLineData.Content,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 WarningStatus.SuppressionList;
   is
      Error              : Error_Types.StringError;
      File               : Error_IO.File_Type;
      Error_Is_Justified : Boolean;
   begin
      Justifications.Check_Whether_Justified
        (Which_Table => Error_Context_Rec.Justifications_Data_Table,
         Line        => Position,
         Kind        => Warning_Message,
         Err_Num     => 10,
         Identifiers => Null_Justification_Identifiers,
         Match_Found => Error_Is_Justified);
      if Error_Is_Justified then
         Inc_Total_Justified_Warnings;
      else
         if WarningStatus.Is_Suppressed (The_Element => Hidden_Parts) then
            Inc_Suppressed_Warning_Counter (Warning_Type => Hidden_Parts);
         else
            Inc_Message_Count (Err_Type => Error_Types.WarningWithoutPosition);
            File := Error_Context_Rec.Errs;

            ErrorBuffer.Add
              (Err_File     => File,
               Err_Type     => Error_Types.WarningWithoutPosition,
               Pos          => Position,
               Scope        => Dictionary.GlobalScope,
               Error_Number => 10,
               Reference    => No_Reference,
               Name1        => Lex_String_To_Name (Str => Unit_Str),
               Name2        => SP_Symbol_To_Name (Sym => Unit_Typ),
               Name3        => Error_Types.NoName,
               Echo_Str     => Error);
            Error_Context_Rec.Errs := File;
            EchoErrorEntry (SPARK_IO.Standard_Output, Error);
         end if;
      end if;
   end Hidden_Text;

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

   procedure Hidden_Handler
     (Position : in LexTokenManager.Token_Position;
      Unit_Str : in LexTokenManager.Lex_String;
      Unit_Typ : in SP_Symbols.SP_Symbol)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Unit_Str,
   --#                                 Unit_Typ,
   --#                                 WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 SPARK_IO.File_Sys,
   --#                                 Unit_Str,
   --#                                 Unit_Typ,
   --#                                 WarningStatus.SuppressionList &
   --#         Total_Error_Count  from *,
   --#                                 CommandLineData.Content,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 WarningStatus.SuppressionList;
   is
      Error              : Error_Types.StringError;
      File               : Error_IO.File_Type;
      Error_Is_Justified : Boolean;
   begin
      Justifications.Check_Whether_Justified
        (Which_Table => Error_Context_Rec.Justifications_Data_Table,
         Line        => Position,
         Kind        => Warning_Message,
         Err_Num     => 9,
         Identifiers => Null_Justification_Identifiers,
         Match_Found => Error_Is_Justified);
      if Error_Is_Justified then
         Inc_Total_Justified_Warnings;
      else
         if WarningStatus.Is_Suppressed (The_Element => Handler_Parts) then
            Inc_Suppressed_Warning_Counter (Warning_Type => Handler_Parts);
         else
            Inc_Message_Count (Err_Type => Error_Types.WarningWithoutPosition);
            File := Error_Context_Rec.Errs;

            ErrorBuffer.Add
              (Err_File     => File,
               Err_Type     => Error_Types.WarningWithoutPosition,
               Pos          => Position,
               Scope        => Dictionary.GlobalScope,
               Error_Number => 9,
               Reference    => No_Reference,
               Name1        => Lex_String_To_Name (Str => Unit_Str),
               Name2        => SP_Symbol_To_Name (Sym => Unit_Typ),
               Name3        => Error_Types.NoName,
               Echo_Str     => Error);
            Error_Context_Rec.Errs := File;
            EchoErrorEntry (SPARK_IO.Standard_Output, Error);
         end if;
      end if;
   end Hidden_Handler;

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

   procedure Representation_Clause (Position : in LexTokenManager.Token_Position)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 SPARK_IO.File_Sys,
   --#                                 WarningStatus.SuppressionList &
   --#         Total_Error_Count  from *,
   --#                                 CommandLineData.Content,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 WarningStatus.SuppressionList;
   is
      Error              : Error_Types.StringError;
      File               : Error_IO.File_Type;
      Error_Is_Justified : Boolean;
   begin
      Justifications.Check_Whether_Justified
        (Which_Table => Error_Context_Rec.Justifications_Data_Table,
         Line        => Position,
         Kind        => Warning_Message,
         Err_Num     => 2,
         Identifiers => Null_Justification_Identifiers,
         Match_Found => Error_Is_Justified);
      if Error_Is_Justified then
         Inc_Total_Justified_Warnings;
      else
         if WarningStatus.Is_Suppressed (The_Element => Representation_Clauses) then
            Inc_Suppressed_Warning_Counter (Warning_Type => Representation_Clauses);
         else
            Inc_Message_Count (Err_Type => Error_Types.WarningWithPosition);
            File := Error_Context_Rec.Errs;
            ErrorBuffer.Add
              (Err_File     => File,
               Err_Type     => Error_Types.WarningWithPosition,
               Pos          => Position,
               Scope        => Dictionary.GlobalScope,
               Error_Number => 2,
               Reference    => No_Reference,
               Name1        => Error_Types.NoName,
               Name2        => Error_Types.NoName,
               Name3        => Error_Types.NoName,
               Echo_Str     => Error);
            Error_Context_Rec.Errs := File;
            EchoErrorEntry (SPARK_IO.Standard_Output, Error);
         end if;
      end if;
   end Representation_Clause;

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

   procedure A_Pragma (Pragma_Name : in LexTokenManager.Lex_String;
                       Position    : in LexTokenManager.Token_Position)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Pragma_Name,
   --#                                 WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Pragma_Name,
   --#                                 SPARK_IO.File_Sys,
   --#                                 WarningStatus.SuppressionList &
   --#         Total_Error_Count  from *,
   --#                                 CommandLineData.Content,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Pragma_Name,
   --#                                 WarningStatus.SuppressionList;
   is
      Error              : Error_Types.StringError;
      File               : Error_IO.File_Type;
      Error_Is_Justified : Boolean;
   begin
      Justifications.Check_Whether_Justified
        (Which_Table => Error_Context_Rec.Justifications_Data_Table,
         Line        => Position,
         Kind        => Warning_Message,
         Err_Num     => 3,
         Identifiers => Null_Justification_Identifiers,
         Match_Found => Error_Is_Justified);
      if Error_Is_Justified then
         Inc_Total_Justified_Warnings;
      else
         if WarningStatus.Pragma_Is_Suppressed (Pragma_Name => Pragma_Name) then
            Inc_Suppressed_Warning_Counter (Warning_Type => Pragmas);
         else
            Inc_Message_Count (Err_Type => Error_Types.WarningWithPosition);
            File := Error_Context_Rec.Errs;
            ErrorBuffer.Add
              (Err_File     => File,
               Err_Type     => Error_Types.WarningWithPosition,
               Pos          => Position,
               Scope        => Dictionary.GlobalScope,
               Error_Number => 3,
               Reference    => No_Reference,
               Name1        => Error_Types.NoName,
               Name2        => Error_Types.NoName,
               Name3        => Error_Types.NoName,
               Echo_Str     => Error);
            Error_Context_Rec.Errs := File;
            EchoErrorEntry (SPARK_IO.Standard_Output, Error);
         end if;
      end if;
   end A_Pragma;

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

   procedure Add_Cut_Point (At_Line : LexTokenManager.Line_Numbers)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 At_Line,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from At_Line,
   --#                                 CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 SPARK_IO.File_Sys,
   --#                                 WarningStatus.SuppressionList &
   --#         Total_Error_Count  from *,
   --#                                 WarningStatus.SuppressionList;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      if WarningStatus.Is_Suppressed (The_Element => Default_Loop_Assertions) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Default_Loop_Assertions);
      else
         Inc_Message_Count (Err_Type => Error_Types.WarningWithoutPosition);
         File := Error_Context_Rec.Errs;
         ErrorBuffer.Add
           (Err_File     => File,
            Err_Type     => Error_Types.WarningWithoutPosition,
            Pos          => LexTokenManager.Token_Position'(Start_Line_No => At_Line,
                                                            Start_Pos     => 0),
            Scope        => Dictionary.GlobalScope,
            Error_Number => 402,
            Reference    => No_Reference,
            Name1        => Error_Types.NoName,
            Name2        => Error_Types.NoName,
            Name3        => Error_Types.NoName,
            Echo_Str     => Error);
         Error_Context_Rec.Errs := File;
         EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      end if;
   end Add_Cut_Point;

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

   procedure Semantic_Warning_With_Position
     (Err_Num  : in Natural;
      Position : in LexTokenManager.Token_Position;
      Id_Str   : in LexTokenManager.Lex_String;
      Sym      : in Dictionary.Symbol;
      Scope    : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer      from *,
   --#                                      CommandLineData.Content,
   --#                                      Dictionary.Dict,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Err_Num,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Scope,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys       from CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Scope,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList &
   --#         Potential_Invalid_Value from *,
   --#                                      CommandLineData.Content,
   --#                                      Err_Num,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList &
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Err_Num,
   --#                                      WarningStatus.SuppressionList;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      if Err_Num = 1 and then WarningStatus.Is_Suppressed (The_Element => With_Clauses) then
         Inc_Suppressed_Warning_Counter (Warning_Type => With_Clauses);

      elsif Err_Num = 4 and then WarningStatus.Is_Suppressed (The_Element => Declare_Annotations) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Declare_Annotations);

      elsif Err_Num = 5 and then WarningStatus.Is_Suppressed (The_Element => Interrupt_Handlers) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Interrupt_Handlers);

      elsif Err_Num = 7 and then WarningStatus.Is_Suppressed (The_Element => Ada2005_Reserved_Words) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Ada2005_Reserved_Words);

      elsif Err_Num = 11 and then WarningStatus.Is_Suppressed (The_Element => Others_Clauses) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Others_Clauses);

      elsif Err_Num = 12 and then WarningStatus.Is_Suppressed (The_Element => Unchecked_Conversion) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Unchecked_Conversion);

      elsif Err_Num = 169 and then WarningStatus.Is_Suppressed (The_Element => Direct_Updates) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Direct_Updates);

      elsif (Err_Num = 200 or Err_Num = 201) and then WarningStatus.Is_Suppressed (The_Element => Static_Expressions) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Static_Expressions);

      elsif Err_Num = 302
        and then not CommandLineData.Content.VCG
        and then WarningStatus.Is_Suppressed (The_Element => Expression_Reordering) then
         -- Suppress ambiguous ordering message if not
         -- generating VCs for Overflow_Check
         Inc_Suppressed_Warning_Counter (Warning_Type => Expression_Reordering);

      elsif Err_Num = 309 and then WarningStatus.Is_Suppressed (The_Element => Type_Conversions) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Type_Conversions);

      elsif Err_Num = 310 and then WarningStatus.Is_Suppressed (The_Element => Obsolescent_Features) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Obsolescent_Features);

      elsif Err_Num = 320 and then WarningStatus.Is_Suppressed (The_Element => Proof_Function_Non_Boolean) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Proof_Function_Non_Boolean);

      elsif Err_Num = 321 and then WarningStatus.Is_Suppressed (The_Element => Proof_Function_Implicit) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Proof_Function_Implicit);

      elsif (Err_Num = 322 or Err_Num = 323) and then WarningStatus.Is_Suppressed (Proof_Function_Refinement) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Proof_Function_Refinement);

      elsif Err_Num = 350 and then WarningStatus.Is_Suppressed (The_Element => Imported_Objects) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Imported_Objects);

      elsif Err_Num = 392 and then WarningStatus.Is_Suppressed (The_Element => External_Variable_Assignment) then
         Inc_Suppressed_Warning_Counter (Warning_Type => External_Variable_Assignment);

      elsif Err_Num = 394 and then WarningStatus.Is_Suppressed (The_Element => Unuseable_Private_Types) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Unuseable_Private_Types);

         -- following two separate warnings share the same supression key word
      elsif Err_Num = 396
        and then -- non-moded variable with address clause
        WarningStatus.Is_Suppressed (The_Element => Unexpected_Address_Clauses) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Unexpected_Address_Clauses);

      elsif Err_Num = 351
        and then -- constant with address clause
        WarningStatus.Is_Suppressed (The_Element => Unexpected_Address_Clauses) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Unexpected_Address_Clauses);

      elsif Err_Num = 380 and then WarningStatus.Is_Suppressed (The_Element => Style_Check_Casing) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Style_Check_Casing);
      else
         if Err_Num = 399 then
            --special case, although just a warning we want this to suppress flow analysis
            Error_Context_Rec.Severity := Semantic_Errs;
         end if;

         Inc_Message_Count (Err_Type => Error_Types.WarningWithPosition);
         File := Error_Context_Rec.Errs;
         if Dictionary.Is_Null_Symbol (Sym) then
            ErrorBuffer.Add
              (Err_File     => File,
               Err_Type     => Error_Types.WarningWithPosition,
               Pos          => Position,
               Scope        => Dictionary.GlobalScope,
               Error_Number => Err_Num,
               Reference    => No_Reference,
               Name1        => Lex_String_To_Name (Str => Id_Str),
               Name2        => Error_Types.NoName,
               Name3        => Error_Types.NoName,
               Echo_Str     => Error);
         else
            Potential_Invalid_Value := Potential_Invalid_Value
              or else Err_Num = 392 -- Read of an external variable
              or else Err_Num = 12; -- Use of an unchecked conversion

            ErrorBuffer.Add
              (Err_File     => File,
               Err_Type     => Error_Types.WarningWithPosition,
               Pos          => Position,
               Scope        => Scope,
               Error_Number => Err_Num,
               Reference    => No_Reference,
               Name1        => Symbol_To_Name (Sym => Sym),
               Name2        => Error_Types.NoName,
               Name3        => Error_Types.NoName,
               Echo_Str     => Error);
         end if;
         Error_Context_Rec.Errs := File;
         EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      end if;
   end Semantic_Warning_With_Position;

   procedure Semantic_Warning_Without_Position
     (Err_Num  : in Natural;
      Position : in LexTokenManager.Token_Position;
      Id_Str   : in LexTokenManager.Lex_String;
      Sym      : in Dictionary.Symbol;
      Scope    : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Err_Num,
   --#                                 Id_Str,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 Sym,
   --#                                 WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Num,
   --#                                 Id_Str,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 SPARK_IO.File_Sys,
   --#                                 Sym,
   --#                                 WarningStatus.SuppressionList &
   --#         Total_Error_Count  from *,
   --#                                 Err_Num,
   --#                                 WarningStatus.SuppressionList;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      if Err_Num = 400 and then WarningStatus.Is_Suppressed (The_Element => Unused_Variables) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Unused_Variables);
      elsif Err_Num = 403 and then WarningStatus.Is_Suppressed (The_Element => Constant_Variables) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Constant_Variables);
      elsif Err_Num = 405 and then WarningStatus.Is_Suppressed (The_Element => Real_RTCs) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Real_RTCs);
      elsif Err_Num = 430 and then WarningStatus.Is_Suppressed (The_Element => SLI_Generation) then
         Inc_Suppressed_Warning_Counter (Warning_Type => SLI_Generation);
      elsif Err_Num = 431 and then WarningStatus.Is_Suppressed (The_Element => Main_Program_Precondition) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Main_Program_Precondition);
      else
         Inc_Message_Count (Err_Type => Error_Types.WarningWithoutPosition);
         File := Error_Context_Rec.Errs;
         if Dictionary.Is_Null_Symbol (Sym) then
            ErrorBuffer.Add
              (Err_File     => File,
               Err_Type     => Error_Types.WarningWithoutPosition,
               Pos          => Position,
               Scope        => Dictionary.GlobalScope,
               Error_Number => Err_Num,
               Reference    => No_Reference,
               Name1        => Lex_String_To_Name (Str => Id_Str),
               Name2        => Error_Types.NoName,
               Name3        => Error_Types.NoName,
               Echo_Str     => Error);
         else
            ErrorBuffer.Add
              (Err_File     => File,
               Err_Type     => Error_Types.WarningWithoutPosition,
               Pos          => Position,
               Scope        => Scope,
               Error_Number => Err_Num,
               Reference    => No_Reference,
               Name1        => Symbol_To_Name (Sym => Sym),
               Name2        => Error_Types.NoName,
               Name3        => Error_Types.NoName,
               Echo_Str     => Error);
         end if;
         Error_Context_Rec.Errs := File;
         EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      end if;
   end Semantic_Warning_Without_Position;

   function Is_Number_With_Position (Err_Num : in Natural) return Boolean is
   begin
      return Err_Num >= 1 and then Err_Num < 400;
   end Is_Number_With_Position;

   procedure Semantic_Warning
     (Err_Num  : in Natural;
      Position : in LexTokenManager.Token_Position;
      Id_Str   : in LexTokenManager.Lex_String)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer      from *,
   --#                                      CommandLineData.Content,
   --#                                      Dictionary.Dict,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys       from CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      SPARK_IO.File_Sys,
   --#                                      WarningStatus.SuppressionList &
   --#         Potential_Invalid_Value,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      WarningStatus.SuppressionList;
   is
      Error_Is_Justified : Boolean;
   begin
      Justifications.Check_Whether_Justified
        (Which_Table => Error_Context_Rec.Justifications_Data_Table,
         Line        => Position,
         Kind        => Warning_Message,
         Err_Num     => Err_Num,
         Identifiers => Justification_Identifiers'(1      => Lex_Str_To_Justification_Identifier (Str => Id_Str),
                                                   others => Null_Justification_Identifier),
         Match_Found => Error_Is_Justified);
      if Error_Is_Justified then
         Inc_Total_Justified_Warnings;
      else
         if Is_Number_With_Position (Err_Num => Err_Num) then
            Semantic_Warning_With_Position
              (Err_Num  => Err_Num,
               Position => Position,
               Id_Str   => Id_Str,
               Sym      => Dictionary.NullSymbol,
               Scope    => Dictionary.GlobalScope);
         else
            Semantic_Warning_Without_Position
              (Err_Num  => Err_Num,
               Position => Position,
               Id_Str   => Id_Str,
               Sym      => Dictionary.NullSymbol,
               Scope    => Dictionary.GlobalScope);
         end if;
      end if;
   end Semantic_Warning;

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

   procedure SLI_Generation_Warning (Position : in LexTokenManager.Token_Position;
                                     Id_Str   : in LexTokenManager.Lex_String)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer      from *,
   --#                                      CommandLineData.Content,
   --#                                      Dictionary.Dict,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Stop_SLI,
   --#                                      WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys       from CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      WarningStatus.SuppressionList &
   --#         Potential_Invalid_Value,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Error_Context_Rec,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Stop_SLI,
   --#                                      WarningStatus.SuppressionList &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
   begin
      if Generate_SLI then
         Stop_SLI := True;
         Semantic_Warning (Err_Num  => 430,
                           Position => Position,
                           Id_Str   => Id_Str);
      end if;
   end SLI_Generation_Warning;

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

   procedure Semantic_Warning_Sym
     (Err_Num  : in Natural;
      Position : in LexTokenManager.Token_Position;
      Sym      : in Dictionary.Symbol;
      Scope    : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer      from *,
   --#                                      CommandLineData.Content,
   --#                                      Dictionary.Dict,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Scope,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys       from CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Scope,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList &
   --#         Potential_Invalid_Value,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList;
   is
      Error_Is_Justified : Boolean;
   begin
      Justifications.Check_Whether_Justified
        (Which_Table => Error_Context_Rec.Justifications_Data_Table,
         Line        => Position,
         Kind        => Warning_Message,
         Err_Num     => Err_Num,
         Identifiers => Justification_Identifiers'(1      => Symbol_To_Justification_Identifier (Sym => Sym),
                                                   others => Null_Justification_Identifier),
         Match_Found => Error_Is_Justified);
      if Error_Is_Justified then
         Inc_Total_Justified_Warnings;
      else
         if Is_Number_With_Position (Err_Num => Err_Num) then
            Semantic_Warning_With_Position
              (Err_Num  => Err_Num,
               Position => Position,
               Id_Str   => LexTokenManager.Null_String,
               Sym      => Sym,
               Scope    => Scope);
         else
            Semantic_Warning_Without_Position
              (Err_Num  => Err_Num,
               Position => Position,
               Id_Str   => LexTokenManager.Null_String,
               Sym      => Sym,
               Scope    => Scope);
         end if;
      end if;
   end Semantic_Warning_Sym;

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

   procedure SLI_Generation_Warning_Sym
     (Position : in LexTokenManager.Token_Position;
      Sym      : in Dictionary.Symbol;
      Scope    : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer      from *,
   --#                                      CommandLineData.Content,
   --#                                      Dictionary.Dict,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Scope,
   --#                                      Stop_SLI,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys       from CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Scope,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList &
   --#         Potential_Invalid_Value,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Error_Context_Rec,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Stop_SLI,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
   begin
      if Generate_SLI then
         Stop_SLI := True;
         Semantic_Warning_Sym (Err_Num  => 430,
                               Position => Position,
                               Sym      => Sym,
                               Scope    => Scope);
      end if;
   end SLI_Generation_Warning_Sym;

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

   -- Previously, LexErrors, SyntaxErrors and SyntaxRecovery didn't use
   -- the error buffer mechanism and were written direct to the error
   -- file.  This meant that attempts to NOT store strings anywhere in the
   -- error handler system were impossible.  The three routines have been
   -- altered below in an elegent bodge to use ErrorBuffer.Add.
   -- The trick has been to build the error string as now but instead of storing
   -- it, we convert it to a lex string, place it in parameter Name1 and then use
   -- the ErrorBuffer.Add mechanism.  This is not wasteful of LexTokenManager
   -- storage space because these errors are fatal anyway.
   --
   -- The result is that all errors are added to the system via ErrorBuffer.Add
   -- and remain in numeric form until PrintErrors or AppendErrors converst them.

   procedure Lex_Error (Error_Message, Recovery_Message : in String;
                        Error_Item                      : in LexTokenManager.Lex_Value)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out LexTokenManager.State;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer,
   --#         Error_Context_Rec,
   --#         Potential_Invalid_Value,
   --#         SPARK_IO.File_Sys,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Error_Item,
   --#                                      Error_Message,
   --#                                      LexTokenManager.State,
   --#                                      Recovery_Message,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      WarningStatus.SuppressionList &
   --#         LexTokenManager.State   from *,
   --#                                      Error_Item,
   --#                                      Error_Message,
   --#                                      Recovery_Message &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
      Error            : Error_Types.StringError;
      Error_Lex_String : LexTokenManager.Lex_String; --pna
   begin
      Error_Context_Rec.Severity := Fatal;
      Error                      := Error_Types.StringError'(0, Error_Types.LexErr, Error_Item.Position, E_Strings.Empty_String);

      Append_String (E_Str => Error,
                     Str   => Error_Message);
      Append_String (E_Str => Error,
                     Str   => " - ");
      Append_String (E_Str => Error,
                     Str   => Recovery_Message);

      Append_String (E_Str => Error,
                     Str   => ".");
      -- convert string to LexString so we can use ErrorBuffer.Add
      LexTokenManager.Insert_Examiner_String (Str     => Error.Message,
                                              Lex_Str => Error_Lex_String);
      Inc_Message_Count (Err_Type => Error_Types.LexErr);
      ErrorBuffer.Add
        (Err_File     => Error_Context_Rec.Errs,
         Err_Type     => Error_Types.LexErr,
         Pos          => Error_Item.Position,
         Scope        => Dictionary.GlobalScope,
         Error_Number => 0,
         Reference    => 0,
         Name1        => Lex_String_To_Name (Str => Error_Lex_String),
         Name2        => Error_Types.NoName,
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      SLI_Generation_Warning (Position => Error_Item.Position,
                              Id_Str   => Error_Lex_String);
   end Lex_Error;

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

   procedure Syntax_Error
     (Error_Item                           : in LexTokenManager.Lex_Value;
      Current_Sym, Entry_Symbol            : in SP_Symbols.SP_Symbol;
      No_Of_Terminals, No_Of_Non_Terminals : in SP_Expected_Symbols.SP_Ess_Sym_Range;
      Terminal_List, Non_Terminal_List     : in SP_Expected_Symbols.SP_Exp_Sym_List)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out LexTokenManager.State;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer,
   --#         Error_Context_Rec,
   --#         Potential_Invalid_Value,
   --#         SPARK_IO.File_Sys,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Current_Sym,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      Entry_Symbol,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Error_Item,
   --#                                      LexTokenManager.State,
   --#                                      Non_Terminal_List,
   --#                                      No_Of_Non_Terminals,
   --#                                      No_Of_Terminals,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      Terminal_List,
   --#                                      WarningStatus.SuppressionList &
   --#         LexTokenManager.State   from *,
   --#                                      Current_Sym,
   --#                                      Entry_Symbol,
   --#                                      Error_Item,
   --#                                      Non_Terminal_List,
   --#                                      No_Of_Non_Terminals,
   --#                                      No_Of_Terminals,
   --#                                      Terminal_List &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
      Error            : Error_Types.StringError;
      Error_Lex_String : LexTokenManager.Lex_String; --pna

      procedure Append_Sym_List
        (Error      : in out Error_Types.StringError;
         No_In_List : in     SP_Expected_Symbols.SP_Ess_Sym_Range;
         List       : in     SP_Expected_Symbols.SP_Exp_Sym_List;
         Last_Sep   : in     String)
      --# derives Error from *,
      --#                    Last_Sep,
      --#                    List,
      --#                    No_In_List;
      is
      begin
         AppendSym (Error => Error,
                    Sym   => List (1));
         for I in SP_Expected_Symbols.SP_Ess_Sym_Range range 2 .. No_In_List - 1 loop
            Append_String (E_Str => Error,
                           Str   => ", ");
            AppendSym (Error => Error,
                       Sym   => List (I));
         end loop;
         if No_In_List > 1 then
            Append_String (E_Str => Error,
                           Str   => Last_Sep);
            AppendSym (Error => Error,
                       Sym   => List (No_In_List));
         end if;
      end Append_Sym_List;

      procedure Append_Hint
      --# global in     Current_Sym;
      --#        in     Entry_Symbol;
      --#        in     Non_Terminal_List;
      --#        in     No_Of_Non_Terminals;
      --#        in     No_Of_Terminals;
      --#        in     Terminal_List;
      --#        in out Error;
      --# derives Error from *,
      --#                    Current_Sym,
      --#                    Entry_Symbol,
      --#                    Non_Terminal_List,
      --#                    No_Of_Non_Terminals,
      --#                    No_Of_Terminals,
      --#                    Terminal_List;
      is
         procedure Dump_State
         --# derives ;
         is
            --# hide Dump_State;
         begin
            if CommandLineData.Content.Debug.Parser then
               Debug.PrintMsg ("In ErrorHandler.Syntax_Error.Append_Hint we know:", True);
               Debug.PrintInt ("The Number of Terminals is ", Integer (No_Of_Terminals));
               Debug.PrintMsg ("The Terminal List is:", True);

               for TLI in SP_Expected_Symbols.SP_Ess_Sym_Range range 1 .. No_Of_Terminals loop
                  Debug.PrintMsg (SP_Symbols.SP_Symbol'Image (Terminal_List (TLI)), False);
                  Debug.PrintMsg (" ", False);
               end loop;
               Debug.PrintMsg ("", True);

               Debug.PrintInt ("The Number of Non-Terminals is ", Integer (No_Of_Non_Terminals));
               Debug.PrintMsg ("The Non-Terminal List is:", True);

               for NTLI in SP_Expected_Symbols.SP_Ess_Sym_Range range 1 .. No_Of_Non_Terminals loop
                  Debug.PrintMsg (SP_Symbols.SP_Symbol'Image (Non_Terminal_List (NTLI)), False);
                  Debug.PrintMsg (" ", False);
               end loop;
               Debug.PrintMsg ("", True);

               Debug.PrintMsg ("The Entry Symbol:", False);
               Debug.PrintMsg (SP_Symbols.SP_Symbol'Image (Entry_Symbol), True);

               Debug.PrintMsg ("The Current Symbol:", False);
               Debug.PrintMsg (SP_Symbols.SP_Symbol'Image (Current_Sym), True);

               Debug.Print_Lex_Str (Msg => "The current lex token is:",
                                    L   => Error_Item.Token_Str);
            end if;
         end Dump_State;

      begin
         Dump_State;

         ---------------------------------------------------------------------
         -- Hints for special cases
         --
         -- Here, we search for known special cases where we can give
         -- a more informative error message than that generated by the parser
         -- alone.  In detecting these special cases, take great care to find
         -- _exactly_ the case you're expecting, since issuing a hint which
         -- is wrong is probably just as bad as not issuing the hint at all!
         --
         -- This is a bit of a kludge - the long-term solution is to
         -- re-implement the parser generator to produce better errors in
         -- general.
         ---------------------------------------------------------------------

         if No_Of_Terminals = 0 and No_Of_Non_Terminals = 1 then
            ---------------------------------------------------------------------
            -- Case 1 - A protected type definition where the user forgets to
            -- put a Priority pragma.  This is likely to be a common mistake for
            -- beginner RavenSPARK users, so giving a more informative error here
            -- is important.
            ---------------------------------------------------------------------
            if (Non_Terminal_List (1) = SP_Symbols.protected_definition) and
              (Current_Sym = SP_Symbols.RWprocedure or Current_Sym = SP_Symbols.RWentry or Current_Sym = SP_Symbols.RWfunction)
            then
               Append_String (E_Str => Error,
                              Str   => " Pragma Priority or Interrupt_Priority is required here.");

               ---------------------------------------------------------------------
               -- Case 2 - Nested procedure body has unexpected semicolon. Can be
               -- legal if followed by a pragma Import, but definitely wrong if
               -- followed by "is".
               ---------------------------------------------------------------------
            elsif (Non_Terminal_List (1) = SP_Symbols.apragma) and
              (Current_Sym = SP_Symbols.RWis) and
              (Entry_Symbol = SP_Symbols.procedure_annotation) then
               Append_String (E_Str => Error,
                              Str   => " Unexpected semicolon on preceding procedure specification.");

               ---------------------------------------------------------------------
               -- Case 11 - A comma has been used instead of a semicolon prior to
               -- an "IN" in a moded global definition.
               ---------------------------------------------------------------------
            elsif (Non_Terminal_List (1) = SP_Symbols.global_variable) and
              (Current_Sym = SP_Symbols.RWin) and
              (Entry_Symbol = SP_Symbols.comma) then
               Append_String
                 (E_Str => Error,
                  Str   => " A semicolon and not a comma should precede an ""IN"" in a moded global definition.");
               ---------------------------------------------------------------------
               -- Case 15 - Empty parenthesis in a subprogram specification.
               ---------------------------------------------------------------------
            elsif (Non_Terminal_List (1) = SP_Symbols.formal_part_rep) and
              (Current_Sym = SP_Symbols.right_paren) and
              (Entry_Symbol = SP_Symbols.left_paren) then
               Append_String
                 (E_Str => Error,
                  Str   => " A subprogram specification without parameters should not have parentheses.");
               ---------------------------------------------------------------------
               -- Case 16 - Empty parenthesis in a subprogram call.
               ---------------------------------------------------------------------
            elsif (Non_Terminal_List (1) = SP_Symbols.name_argument_list) and
              (Current_Sym = SP_Symbols.right_paren) and
              (Entry_Symbol = SP_Symbols.left_paren) then
               Append_String (E_Str => Error,
                              Str   => " A subprogram call without parameters should not have parentheses.");
               ---------------------------------------------------------------------
               -- Case 18 - Formal parameter list starts with an FDL identifier
               ---------------------------------------------------------------------
            elsif (Non_Terminal_List (1) = SP_Symbols.formal_part_rep) and
              (Current_Sym = SP_Symbols.predefined_FDL_identifier) and
              (Entry_Symbol = SP_Symbols.left_paren) then

               Append_String (E_Str => Error,
                              Str   => " This token is a predefined FDL identifier, ");
               Append_String (E_Str => Error,
                              Str   => "and therefore may not be used in this context.");
               ---------------------------------------------------------------------
               -- Case 22 - Attempt to use unqualified array aggregate in annotation
               ---------------------------------------------------------------------
            elsif (Non_Terminal_List (1) = SP_Symbols.annotation_expression) and
              (Current_Sym = SP_Symbols.RWothers) and
              (Entry_Symbol = SP_Symbols.left_paren) then
               Append_String (E_Str => Error,
                              Str   => " Aggregate expressions in annotations must always be qualified");
               Append_String (E_Str => Error,
                              Str   => " with a subtype mark.");

               ---------------------------------------------------------------------
               -- Case 23 - "body" appears in package spec - almost certainly
               -- owing to a mis-placed inherit annotation preceding package
               -- body
               ---------------------------------------------------------------------
            elsif (Non_Terminal_List (1) = SP_Symbols.dotted_simple_name) and
              (Current_Sym = SP_Symbols.RWbody) and
              (Entry_Symbol = SP_Symbols.RWpackage) then
               Append_String (E_Str => Error,
                              Str   => " Package body cannot follow inherit annotation.");
            end if;

         elsif No_Of_Terminals = 1 and No_Of_Non_Terminals = 0 then
            ---------------------------------------------------------------------
            -- Case 3 - misplaced "is" following procedure or function annotation
            ---------------------------------------------------------------------
            if Terminal_List (1) = SP_Symbols.RWinherit and
              (Current_Sym = SP_Symbols.RWglobal or Current_Sym = SP_Symbols.RWderives) then
               Append_String (E_Str => Error,
                              Str   => " Subprogram annotation should precede reserved word ""IS"".");
               ---------------------------------------------------------------------
               -- Case 4 - Expecting Identifier, but got a predefined FDL identifier
               -- A common error for beginners!
               ---------------------------------------------------------------------
            elsif Terminal_List (1) = SP_Symbols.identifier and Current_Sym = SP_Symbols.predefined_FDL_identifier then
               Append_String (E_Str => Error,
                              Str   => " This token is a predefined FDL identifier, ");
               Append_String (E_Str => Error,
                              Str   => "and therefore may not be used in this context.");
               ---------------------------------------------------------------------
               -- Case 9 - "own" annotation in package body following "is"
               ---------------------------------------------------------------------
            elsif Terminal_List (1) = SP_Symbols.RWinherit and Current_Sym = SP_Symbols.RWown then
               Append_String (E_Str => Error,
                              Str   => " Own annotation should precede reserved word ""IS"".");
               ---------------------------------------------------------------------
               -- Case 14 - Incorrect name given in hide directive
               ---------------------------------------------------------------------
            elsif Terminal_List (1) = SP_Symbols.semicolon and Entry_Symbol = SP_Symbols.hidden_part then
               Append_String (E_Str => Error,
                              Str   => " The name in a preceding ""hide"" directive is probably incorrect.");
            end if;

         elsif No_Of_Terminals = 0 and No_Of_Non_Terminals = 0 then
            ---------------------------------------------------------------------
            -- Case 5 - Misplaced "is" _before_ a mandatory annotation
            ---------------------------------------------------------------------
            if Current_Sym = SP_Symbols.annotation_start and Entry_Symbol = SP_Symbols.RWis then
               Append_String (E_Str => Error,
                              Str   => " For packages and subprograms, annotations must ");
               Append_String (E_Str => Error,
                              Str   => "precede ""IS"".");

               ---------------------------------------------------------------------
               -- Case 6 - semicolon missing at end of annotation
               ---------------------------------------------------------------------
            elsif Current_Sym = SP_Symbols.annotation_end and Entry_Symbol = SP_Symbols.dotted_simple_name then
               Append_String (E_Str => Error,
                              Str   => " Annotations must end with a ;");

               ---------------------------------------------------------------------
               -- Case 10 - unexpected semicolon at end of subprogram specification
               ---------------------------------------------------------------------
            elsif Current_Sym = SP_Symbols.RWis and Entry_Symbol = SP_Symbols.semicolon then
               Append_String (E_Str => Error,
                              Str   => " Unexpected semicolon on preceding subprogram specification.");

               ---------------------------------------------------------------------
               -- Case 12 - reported message is "No complete DOTTED_SIMPLE_NAME can be followed by IDENTIFIER here,"
               -- Rockwell-Collins raised candidate for improvement in relation to
               -- imports in derives annotations but the possible occurance of the
               -- syntax error is much wider than this so we have to be careful with
               -- the wording of the eror message.
               ---------------------------------------------------------------------
            elsif Current_Sym = SP_Symbols.identifier and Entry_Symbol = SP_Symbols.dotted_simple_name then
               Append_String (E_Str => Error,
                              Str   => " A separator is missing between two successive names.");

               ---------------------------------------------------------------------
               -- Case 17 - declaration of an object using an FDL identifier
               ---------------------------------------------------------------------
            elsif Current_Sym = SP_Symbols.predefined_FDL_identifier and
              (Entry_Symbol = SP_Symbols.visible_part_rep or Entry_Symbol = SP_Symbols.initial_declarative_item_rep) then

               Append_String (E_Str => Error,
                              Str   => " This token is a predefined FDL identifier, ");
               Append_String (E_Str => Error,
                              Str   => "and therefore may not be used in this context.");

               ---------------------------------------------------------------------
               -- Case 19 - Attempt to label a declaration
               ---------------------------------------------------------------------
            elsif Current_Sym = SP_Symbols.left_label_paren and
              (Entry_Symbol = SP_Symbols.initial_declarative_item_rep or Entry_Symbol = SP_Symbols.RWis) then

               Append_String (E_Str => Error,
                              Str   => " Declarations may not be labelled.");

               ---------------------------------------------------------------------
               -- Case 20 - Attempt to label a proof context
               ---------------------------------------------------------------------
            elsif Current_Sym = SP_Symbols.proof_context and Entry_Symbol = SP_Symbols.sequence_of_labels then

               Append_String (E_Str => Error,
                              Str   => " Annotations may not be labelled.");

               ---------------------------------------------------------------------
               -- Case 21 - Attempt to use unqualified aggregate expression
               ---------------------------------------------------------------------
            elsif Current_Sym = SP_Symbols.arrow and Entry_Symbol = SP_Symbols.simple_expression then

               Append_String (E_Str => Error,
                              Str   => " Aggregate expressions must be qualified with a");
               Append_String (E_Str => Error,
                              Str   => " subtype mark or must specify an unconstrained");
               Append_String (E_Str => Error,
                              Str   => " array with only an others choice. Named and");
               Append_String (E_Str => Error,
                              Str   => " positional association may not be mixed.");

               ---------------------------------------------------------------------
               -- Cases 24 and 25 - type, subtype, or object following a later declarative item
               ---------------------------------------------------------------------
            elsif Entry_Symbol = SP_Symbols.later_declarative_item_rep then

               if (Current_Sym = SP_Symbols.RWsubtype or Current_Sym = SP_Symbols.RWtype) then

                  Append_String (E_Str => Error,
                                 Str   => " Types and subtypes must precede all later declarative items");
                  Append_String (E_Str => Error,
                                 Str   => " such as bodies, stubs or instantiations.");

               elsif (Current_Sym = SP_Symbols.identifier) then

                  Append_String (E_Str => Error,
                                 Str   => " Object declarations must precede all later declarative items");
                  Append_String (E_Str => Error,
                                 Str   => " such as bodies, stubs or instantiations.");

               end if;

            end if;

         elsif No_Of_Terminals = 4 and No_Of_Non_Terminals = 0 then
            ---------------------------------------------------------------------
            -- Case 7 - missing ; on the end of an own variable annotation
            ---------------------------------------------------------------------
            if Entry_Symbol = SP_Symbols.own_variable_list and
              Current_Sym = SP_Symbols.annotation_end and
              Terminal_List (1) = SP_Symbols.left_paren and
              Terminal_List (2) = SP_Symbols.comma and
              Terminal_List (3) = SP_Symbols.colon and
              Terminal_List (4) = SP_Symbols.semicolon then

               Append_String (E_Str => Error,
                              Str   => " Own variable annotation must end with a ;");
            end if;

         elsif No_Of_Terminals = 2 and No_Of_Non_Terminals = 0 then
            ---------------------------------------------------------------------
            -- Case 8 - missing ; on the end of an initializes annotation
            ---------------------------------------------------------------------
            if Entry_Symbol = SP_Symbols.package_variable_list and
              Current_Sym = SP_Symbols.annotation_end and
              Terminal_List (1) = SP_Symbols.comma and
              Terminal_List (2) = SP_Symbols.semicolon then

               Append_String (E_Str => Error,
                              Str   => " Initializes annotation must end with a ;");
            end if;

            ---------------------------------------------------------------------
            -- Case 13 - derives list applied to a function
            -- From the SPARK.LLA grammar, The two expected terminal symbols
            -- RWpre and RWreturn can only occur together in an annotation
            -- as a function constraint so we should be safe to assume that we
            -- are in an annotation associated with a function.
            ---------------------------------------------------------------------
            if Entry_Symbol = SP_Symbols.annotation_start and
              Current_Sym = SP_Symbols.RWderives and
              Terminal_List (1) = SP_Symbols.RWpre and
              Terminal_List (2) = SP_Symbols.RWreturn then

               Append_String
                 (E_Str => Error,
                  Str   => " A function never has a ""derives"" annotation." &
                    " It may have a global definition in which all the global variables are of mode in.");
            end if;

         end if;

      end Append_Hint; -- Terminal_List not ref at the moment, but likely to be needed in future.

   begin
      Error_Context_Rec.Severity := Fatal;
      Error                      :=
        Error_Types.StringError'(0, Error_Types.SyntaxErr, Error_Item.Position, E_Strings.Empty_String);

      if No_Of_Terminals /= 0 and No_Of_Non_Terminals = 0 then
         Append_Sym_List (Error      => Error,
                          No_In_List => No_Of_Terminals,
                          List       => Terminal_List,
                          Last_Sep   => " or ");
         Append_String (E_Str => Error,
                        Str   => " expected");
      elsif No_Of_Terminals = 0 and No_Of_Non_Terminals = 1 then
         Append_String (E_Str => Error,
                        Str   => "No ");
         Append_Sym_List (Error      => Error,
                          No_In_List => No_Of_Non_Terminals,
                          List       => Non_Terminal_List,
                          Last_Sep   => " nor ");
         Append_String (E_Str => Error,
                        Str   => " can start with ");
         AppendSym (Error => Error,
                    Sym   => Current_Sym);

      elsif No_Of_Terminals = 0 and No_Of_Non_Terminals > 1 then
         Append_String (E_Str => Error,
                        Str   => "Neither ");
         Append_Sym_List (Error      => Error,
                          No_In_List => No_Of_Non_Terminals,
                          List       => Non_Terminal_List,
                          Last_Sep   => " nor ");
         Append_String (E_Str => Error,
                        Str   => " can start with ");
         AppendSym (Error => Error,
                    Sym   => Current_Sym);
      elsif No_Of_Terminals /= 0 and No_Of_Non_Terminals /= 0 then
         Append_Sym_List (Error      => Error,
                          No_In_List => No_Of_Terminals,
                          List       => Terminal_List,
                          Last_Sep   => ", ");
         Append_String (E_Str => Error,
                        Str   => " or start of ");
         Append_Sym_List (Error      => Error,
                          No_In_List => No_Of_Non_Terminals,
                          List       => Non_Terminal_List,
                          Last_Sep   => " or ");
         Append_String (E_Str => Error,
                        Str   => " expected");
      else
         if SP_Relations.SP_Terminal_Like (Entry_Symbol) then
            AppendSym (Error => Error,
                       Sym   => Entry_Symbol);
            Append_String (E_Str => Error,
                           Str   => " cannot be followed by ");
         else
            Append_String (E_Str => Error,
                           Str   => "No complete ");
            AppendSym (Error => Error,
                       Sym   => Entry_Symbol);
            Append_String (E_Str => Error,
                           Str   => " can be followed by ");
         end if;
         AppendSym (Error => Error,
                    Sym   => Current_Sym);
         Append_String (E_Str => Error,
                        Str   => " here");
      end if;
      Append_String (E_Str => Error,
                     Str   => ".");

      Append_Hint;

      -- convert string to LExString so we can use ErrorBuffer.Add
      LexTokenManager.Insert_Examiner_String (Str     => Error.Message,
                                              Lex_Str => Error_Lex_String);
      Inc_Message_Count (Err_Type => Error_Types.SyntaxErr);
      ErrorBuffer.Add
        (Err_File     => Error_Context_Rec.Errs,
         Err_Type     => Error_Types.SyntaxErr,
         Pos          => Error_Item.Position,
         Scope        => Dictionary.GlobalScope,
         Error_Number => 0,
         Reference    => 0,
         Name1        => Lex_String_To_Name (Str => Error_Lex_String),
         Name2        => Error_Types.NoName,
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      SLI_Generation_Warning (Position => Error_Item.Position,
                              Id_Str   => Error_Lex_String);
   end Syntax_Error;

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

   procedure Syntax_Recovery
     (Recovery_Posn   : in LexTokenManager.Lex_Value;
      Replacement_Sym : in SP_Symbols.SP_Symbol;
      Next_Sym        : in SP_Symbols.SP_Terminal;
      No_Of_Syms      : in Natural;
      Sym_List        : in Err_Sym_List)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out LexTokenManager.State;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer,
   --#         Potential_Invalid_Value,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Dictionary.Dict,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      LexTokenManager.State,
   --#                                      Next_Sym,
   --#                                      No_Of_Syms,
   --#                                      Recovery_Posn,
   --#                                      Replacement_Sym,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      Sym_List,
   --#                                      WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys       from CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      LexTokenManager.State,
   --#                                      Next_Sym,
   --#                                      No_Of_Syms,
   --#                                      Recovery_Posn,
   --#                                      Replacement_Sym,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      Sym_List,
   --#                                      WarningStatus.SuppressionList &
   --#         LexTokenManager.State   from *,
   --#                                      Error_Context_Rec,
   --#                                      Next_Sym,
   --#                                      No_Of_Syms,
   --#                                      Recovery_Posn,
   --#                                      Replacement_Sym,
   --#                                      Sym_List &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content,
   --#                                      Error_Context_Rec;
   is
      Error, Unused_Error : Error_Types.StringError;
      Error_Lex_String    : LexTokenManager.Lex_String;
      Max_Index           : Err_Sym_Range;
   begin
      if Error_Context_Rec.Recovery_Messages then
         Error := Error_Types.StringError'(0, Error_Types.SyntaxRec, Recovery_Posn.Position, E_Strings.Empty_String);
         Append_String (E_Str => Error,
                        Str   => "The recovery action was to ");
         if Replacement_Sym = SP_Symbols.SPDEFAULT then
            Append_String (E_Str => Error,
                           Str   => "delete ");
            AppendSym (Error => Error,
                       Sym   => Sym_List (1));
         elsif Replacement_Sym in SP_Symbols.SP_Terminal then
            if No_Of_Syms = 0 then
               Append_String (E_Str => Error,
                              Str   => "insert ");
            else
               Append_String (E_Str => Error,
                              Str   => "replace ");
               AppendSym (Error => Error,
                          Sym   => Sym_List (1));
               Append_String (E_Str => Error,
                              Str   => " with ");
            end if;
            AppendSym (Error => Error,
                       Sym   => Replacement_Sym);
         else
            if Next_Sym /= SP_Symbols.SPDEFAULT then
               if Next_Sym = SP_Symbols.SPEND then
                  Append_String (E_Str => Error,
                                 Str   => "ignore all remaining tokens and ");
               else
                  Append_String (E_Str => Error,
                                 Str   => "ignore all tokens up until ");
                  AppendSym (Error => Error,
                             Sym   => Next_Sym);
                  Append_String (E_Str => Error,
                                 Str   => " and ");
               end if;
            end if;
            if No_Of_Syms /= 0 then
               Append_String (E_Str => Error,
                              Str   => "replace ");
               if No_Of_Syms > Natural (Err_Sym_List'Last) then
                  Max_Index := Err_Sym_List'Last - 1;
               else
                  Max_Index := Err_Sym_Range (No_Of_Syms);
               end if;
               for Index in Err_Sym_Range range 1 .. Max_Index loop
                  AppendSym (Error => Error,
                             Sym   => Sym_List (Index));
                  Append_String (E_Str => Error,
                                 Str   => " ");
               end loop;
               if No_Of_Syms > Natural (Err_Sym_List'Last) then
                  Append_String (E_Str => Error,
                                 Str   => " .. ");
                  AppendSym (Error => Error,
                             Sym   => Sym_List (Err_Sym_List'Last));
               end if;
               Append_String (E_Str => Error,
                              Str   => " by ");
            else
               Append_String (E_Str => Error,
                              Str   => "insert ");
            end if;
            AppendSym (Error => Error,
                       Sym   => Replacement_Sym);
         end if;

         Append_String (E_Str => Error,
                        Str   => ".");
         -- convert string to LexString so we can use ErrorBuffer.Add
         LexTokenManager.Insert_Examiner_String (Str     => Error.Message,
                                                 Lex_Str => Error_Lex_String);
         Inc_Message_Count (Err_Type => Error_Types.SyntaxRec);
         --# accept Flow, 10, Unused_Error, "Only used where we want to echo message to screen";
         ErrorBuffer.Add
           (Err_File     => Error_Context_Rec.Errs,
            Err_Type     => Error_Types.SyntaxRec,
            Pos          => Recovery_Posn.Position,
            Scope        => Dictionary.GlobalScope,
            Error_Number => 0,
            Reference    => 0,
            Name1        => Lex_String_To_Name (Str => Error_Lex_String),
            Name2        => Error_Types.NoName,
            Name3        => Error_Types.NoName,
            Echo_Str     => Unused_Error);
         --# end accept;
         -- note, no echo back to screen in this case
         SLI_Generation_Warning (Position => Recovery_Posn.Position,
                                 Id_Str   => Error_Lex_String);
      end if;
      --# accept Flow, 33, Unused_Error, "Consequence of earlier deliberate non-use";
   end Syntax_Recovery;

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

   procedure Semantic_Note
     (Err_Num  : in Natural;
      Position : in LexTokenManager.Token_Position;
      Id_Str   : in LexTokenManager.Lex_String)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Err_Num,
   --#                                 Id_Str,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 WarningStatus.SuppressionList &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Num,
   --#                                 Id_Str,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 SPARK_IO.File_Sys,
   --#                                 WarningStatus.SuppressionList &
   --#         Total_Error_Count  from *,
   --#                                 WarningStatus.SuppressionList;
   is
      File  : Error_IO.File_Type;
      Error : Error_Types.StringError;
   begin
      if WarningStatus.Is_Suppressed (The_Element => Notes) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Notes);
      else
         Inc_Message_Count (Err_Type => Error_Types.Note);
         File := Error_Context_Rec.Errs;
         ErrorBuffer.Add
           (Err_File     => File,
            Err_Type     => Error_Types.Note,
            Pos          => Position,
            Scope        => Dictionary.GlobalScope,
            Error_Number => Err_Num,
            Reference    => No_Reference,
            Name1        => Lex_String_To_Name (Str => Id_Str),
            Name2        => Error_Types.NoName,
            Name3        => Error_Types.NoName,
            Echo_Str     => Error);
         Error_Context_Rec.Errs := File;
         EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      end if;
   end Semantic_Note;

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

   procedure Dep_Semantic_Error
     (Err_Num  : in Natural;
      Position : in LexTokenManager.Token_Position;
      Id_Str1  : in LexTokenManager.Lex_String;
      Id_Str2  : in LexTokenManager.Lex_String)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Err_Num,
   --#                                 Id_Str1,
   --#                                 Id_Str2,
   --#                                 LexTokenManager.State,
   --#                                 Position &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Num,
   --#                                 Id_Str1,
   --#                                 Id_Str2,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 SPARK_IO.File_Sys &
   --#         Total_Error_Count  from *;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      Inc_Message_Count (Err_Type => Error_Types.DepSemanticErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.DepSemanticErr,
         Pos          => Position,
         Scope        => Dictionary.GlobalScope,
         Error_Number => Err_Num,
         Reference    => No_Reference,
         Name1        => Lex_String_To_Name (Str => Id_Str1),
         Name2        => Lex_String_To_Name (Str => Id_Str2),
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
   end Dep_Semantic_Error;

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

   procedure Dep_Semantic_Error_Sym
     (Err_Num  : in Natural;
      Position : in LexTokenManager.Token_Position;
      Sym1     : in Dictionary.Symbol;
      Sym2     : in Dictionary.Symbol;
      Scope    : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State  from *,
   --#                                 CommandLineData.Content,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Err_Num,
   --#                                 Position,
   --#                                 Scope,
   --#                                 Sym1,
   --#                                 Sym2 &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Num,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 SPARK_IO.File_Sys,
   --#                                 Sym1,
   --#                                 Sym2 &
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 Err_Num,
   --#                                 Position,
   --#                                 Scope,
   --#                                 Sym1,
   --#                                 Sym2 &
   --#         Total_Error_Count  from *;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      Inc_Message_Count (Err_Type => Error_Types.DepSemanticErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.DepSemanticErr,
         Pos          => Position,
         Scope        => Scope,
         Error_Number => Err_Num,
         Reference    => No_Reference,
         Name1        => Symbol_To_Name (Sym => Sym1),
         Name2        => Symbol_To_Name (Sym => Sym2),
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
   end Dep_Semantic_Error_Sym;

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

   procedure Semantic_Error
     (Err_Num   : in Natural;
      Reference : in Natural;
      Position  : in LexTokenManager.Token_Position;
      Id_Str    : in LexTokenManager.Lex_String)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer,
   --#         Error_Context_Rec,
   --#         Potential_Invalid_Value,
   --#         SPARK_IO.File_Sys,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Reference,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      WarningStatus.SuppressionList &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      Error_Context_Rec.Severity := Semantic_Errs;
      Justifications.Set_Current_Unit_Has_Semantic_Errors (Which_Table => Error_Context_Rec.Justifications_Data_Table);
      Inc_Message_Count (Err_Type => Error_Types.SemanticErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.SemanticErr,
         Pos          => Position,
         Scope        => Dictionary.GlobalScope,
         Error_Number => Err_Num,
         Reference    => Reference,
         Name1        => Lex_String_To_Name (Str => Id_Str),
         Name2        => Error_Types.NoName,
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      SLI_Generation_Warning (Position => Position,
                              Id_Str   => Id_Str);
   end Semantic_Error;

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

   procedure Semantic_Error2
     (Err_Num   : in Natural;
      Reference : in Natural;
      Position  : in LexTokenManager.Token_Position;
      Id_Str1   : in LexTokenManager.Lex_String;
      Id_Str2   : in LexTokenManager.Lex_String)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer,
   --#         Error_Context_Rec,
   --#         Potential_Invalid_Value,
   --#         SPARK_IO.File_Sys,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      Id_Str1,
   --#                                      Id_Str2,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Reference,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      WarningStatus.SuppressionList &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      Justifications.Set_Current_Unit_Has_Semantic_Errors (Which_Table => Error_Context_Rec.Justifications_Data_Table);
      Error_Context_Rec.Severity := Semantic_Errs;
      Inc_Message_Count (Err_Type => Error_Types.SemanticErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.SemanticErr,
         Pos          => Position,
         Scope        => Dictionary.GlobalScope,
         Error_Number => Err_Num,
         Reference    => Reference,
         Name1        => Lex_String_To_Name (Str => Id_Str1),
         Name2        => Lex_String_To_Name (Str => Id_Str2),
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      SLI_Generation_Warning (Position => Position,
                              Id_Str   => Id_Str1);
   end Semantic_Error2;

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

   procedure Semantic_Error_Sym
     (Err_Num   : in Natural;
      Reference : in Natural;
      Position  : in LexTokenManager.Token_Position;
      Sym       : in Dictionary.Symbol;
      Scope     : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer,
   --#         Error_Context_Rec,
   --#         Potential_Invalid_Value,
   --#         SPARK_IO.File_Sys,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Reference,
   --#                                      Scope,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      Justifications.Set_Current_Unit_Has_Semantic_Errors (Which_Table => Error_Context_Rec.Justifications_Data_Table);
      Error_Context_Rec.Severity := Semantic_Errs;
      Inc_Message_Count (Err_Type => Error_Types.SemanticErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.SemanticErr,
         Pos          => Position,
         Scope        => Scope,
         Error_Number => Err_Num,
         Reference    => Reference,
         Name1        => Symbol_To_Name (Sym => Sym),
         Name2        => Error_Types.NoName,
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      SLI_Generation_Warning_Sym (Position => Position,
                                  Sym      => Sym,
                                  Scope    => Scope);
   end Semantic_Error_Sym;

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

   procedure Semantic_Error_Sym2
     (Err_Num   : in Natural;
      Reference : in Natural;
      Position  : in LexTokenManager.Token_Position;
      Sym       : in Dictionary.Symbol;
      Sym2      : in Dictionary.Symbol;
      Scope     : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer,
   --#         Error_Context_Rec,
   --#         Potential_Invalid_Value,
   --#         SPARK_IO.File_Sys,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Reference,
   --#                                      Scope,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      Sym,
   --#                                      Sym2,
   --#                                      WarningStatus.SuppressionList &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      Justifications.Set_Current_Unit_Has_Semantic_Errors (Which_Table => Error_Context_Rec.Justifications_Data_Table);
      Error_Context_Rec.Severity := Semantic_Errs;
      Inc_Message_Count (Err_Type => Error_Types.SemanticErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.SemanticErr,
         Pos          => Position,
         Scope        => Scope,
         Error_Number => Err_Num,
         Reference    => Reference,
         Name1        => Symbol_To_Name (Sym => Sym),
         Name2        => Symbol_To_Name (Sym => Sym2),
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      SLI_Generation_Warning_Sym (Position => Position,
                                  Sym      => Sym,
                                  Scope    => Scope);
   end Semantic_Error_Sym2;

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

   procedure Semantic_Error_Lex1_Sym1
     (Err_Num   : in Natural;
      Reference : in Natural;
      Position  : in LexTokenManager.Token_Position;
      Id_Str    : in LexTokenManager.Lex_String;
      Sym       : in Dictionary.Symbol;
      Scope     : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer,
   --#         Error_Context_Rec,
   --#         Potential_Invalid_Value,
   --#         SPARK_IO.File_Sys,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Reference,
   --#                                      Scope,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      Sym,
   --#                                      WarningStatus.SuppressionList &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      Justifications.Set_Current_Unit_Has_Semantic_Errors (Which_Table => Error_Context_Rec.Justifications_Data_Table);
      Error_Context_Rec.Severity := Semantic_Errs;
      Inc_Message_Count (Err_Type => Error_Types.SemanticErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.SemanticErr,
         Pos          => Position,
         Scope        => Scope,
         Error_Number => Err_Num,
         Reference    => Reference,
         Name1        => Lex_String_To_Name (Str => Id_Str),
         Name2        => Symbol_To_Name (Sym => Sym),
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      SLI_Generation_Warning (Position => Position,
                              Id_Str   => Id_Str);
   end Semantic_Error_Lex1_Sym1;

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

   procedure Semantic_Error_Lex1_Sym2
     (Err_Num   : in Natural;
      Reference : in Natural;
      Position  : in LexTokenManager.Token_Position;
      Id_Str    : in LexTokenManager.Lex_String;
      Sym       : in Dictionary.Symbol;
      Sym2      : in Dictionary.Symbol;
      Scope     : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer,
   --#         Error_Context_Rec,
   --#         Potential_Invalid_Value,
   --#         SPARK_IO.File_Sys,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      Id_Str,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Reference,
   --#                                      Scope,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      Sym,
   --#                                      Sym2,
   --#                                      WarningStatus.SuppressionList &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      Justifications.Set_Current_Unit_Has_Semantic_Errors (Which_Table => Error_Context_Rec.Justifications_Data_Table);
      Error_Context_Rec.Severity := Semantic_Errs;
      Inc_Message_Count (Err_Type => Error_Types.SemanticErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.SemanticErr,
         Pos          => Position,
         Scope        => Scope,
         Error_Number => Err_Num,
         Reference    => Reference,
         Name1        => Lex_String_To_Name (Str => Id_Str),
         Name2        => Symbol_To_Name (Sym => Sym),
         Name3        => Symbol_To_Name (Sym => Sym2),
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      SLI_Generation_Warning (Position => Position,
                              Id_Str   => Id_Str);
   end Semantic_Error_Lex1_Sym2;

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

   procedure Semantic_Error_Sym3
     (Err_Num   : in Natural;
      Reference : in Natural;
      Position  : in LexTokenManager.Token_Position;
      Sym       : in Dictionary.Symbol;
      Sym2      : in Dictionary.Symbol;
      Sym3      : in Dictionary.Symbol;
      Scope     : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Stop_SLI;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer,
   --#         Error_Context_Rec,
   --#         Potential_Invalid_Value,
   --#         SPARK_IO.File_Sys,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      Err_Num,
   --#                                      LexTokenManager.State,
   --#                                      Position,
   --#                                      Reference,
   --#                                      Scope,
   --#                                      SPARK_IO.File_Sys,
   --#                                      Stop_SLI,
   --#                                      Sym,
   --#                                      Sym2,
   --#                                      Sym3,
   --#                                      WarningStatus.SuppressionList &
   --#         Stop_SLI                from *,
   --#                                      CommandLineData.Content;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      Justifications.Set_Current_Unit_Has_Semantic_Errors (Which_Table => Error_Context_Rec.Justifications_Data_Table);
      Error_Context_Rec.Severity := Semantic_Errs;
      Inc_Message_Count (Err_Type => Error_Types.SemanticErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.SemanticErr,
         Pos          => Position,
         Scope        => Scope,
         Error_Number => Err_Num,
         Reference    => Reference,
         Name1        => Symbol_To_Name (Sym => Sym),
         Name2        => Symbol_To_Name (Sym => Sym2),
         Name3        => Symbol_To_Name (Sym => Sym3),
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      SLI_Generation_Warning_Sym (Position => Position,
                                  Sym      => Sym,
                                  Scope    => Scope);
   end Semantic_Error_Sym3;

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

   procedure Control_Flow_Error (Err_Type : in Control_Flow_Err_Type;
                                 Position : in LexTokenManager.Token_Position)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Err_Type,
   --#                                 Position &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 SPARK_IO.File_Sys &
   --#         Total_Error_Count  from *;
   is
      Error : Error_Types.StringError;
      File  : Error_IO.File_Type;
   begin
      -- Note, no justification check here, these are serious structural errors in the code
      Error_Context_Rec.Severity := Flow_Errs;
      Inc_Message_Count (Err_Type => Error_Types.UncondFlowErr);
      File := Error_Context_Rec.Errs;
      ErrorBuffer.Add
        (Err_File     => File,
         Err_Type     => Error_Types.ControlFlowErr,
         Pos          => Position,
         Scope        => Dictionary.GlobalScope,
         Error_Number => Control_Flow_Err_Type'Pos (Err_Type) + Error_Types.ControlFlowErrOffset,
         Reference    => No_Reference,
         Name1        => Error_Types.NoName,
         Name2        => Error_Types.NoName,
         Name3        => Error_Types.NoName,
         Echo_Str     => Error);
      Error_Context_Rec.Errs := File;
      EchoErrorEntry (SPARK_IO.Standard_Output, Error);
   end Control_Flow_Error;

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

   procedure Data_Flow_Error
     (Err_Type : in Data_Flow_Err_Type;
      Position : in LexTokenManager.Token_Position;
      Var_Sym  : in Dictionary.Symbol;
      Scope    : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State  from *,
   --#                                 CommandLineData.Content,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 Var_Sym &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 SPARK_IO.File_Sys,
   --#                                 Var_Sym &
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 Var_Sym &
   --#         Total_Error_Count  from *,
   --#                                 CommandLineData.Content,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Var_Sym;
   is
      Error              : Error_Types.StringError;
      File               : Error_IO.File_Type;
      Error_Is_Justified : Boolean;

      function Obtain_Error_Number (Err_Type : Data_Flow_Err_Type) return Natural is
         Result : Natural;
      begin
         case Err_Type is
            when Expn_Undefined | Stmt_Undefined | Invariant_Exp =>
               Result := Data_Flow_Err_Type'Pos (Err_Type) + Error_Types.UncondFlowErrorOffset;
            when Expn_May_Be_Undefined | Stmt_May_Be_Undefined =>
               Result := Data_Flow_Err_Type'Pos (Err_Type) + Error_Types.CondFlowErrorOffset;
         end case;
         return Result;
      end Obtain_Error_Number;

   begin -- Data_Flow_Error
      Justifications.Check_Whether_Justified
        (Which_Table => Error_Context_Rec.Justifications_Data_Table,
         Line        => Position,
         Kind        => Flow_Message,
         Err_Num     => Obtain_Error_Number (Err_Type => Err_Type),
         Identifiers => Justification_Identifiers'(1      => Symbol_To_Justification_Identifier (Sym => Var_Sym),
                                                   others => Null_Justification_Identifier),
         Match_Found => Error_Is_Justified);
      if Error_Is_Justified then
         Inc_Total_Justified_Warnings;
      else
         File := Error_Context_Rec.Errs;
         case Err_Type is
            when Expn_Undefined | Stmt_Undefined | Invariant_Exp =>
               Error_Context_Rec.Severity := Flow_Errs;
               Inc_Message_Count (Err_Type => Error_Types.UncondFlowErr);
               ErrorBuffer.Add
                 (Err_File     => File,
                  Err_Type     => Error_Types.UncondFlowErr,
                  Pos          => Position,
                  Scope        => Scope,
                  Error_Number => Data_Flow_Err_Type'Pos (Err_Type) + Error_Types.UncondFlowErrorOffset,
                  Reference    => No_Reference,
                  Name1        => Symbol_To_Name (Sym => Var_Sym),
                  Name2        => Error_Types.NoName,
                  Name3        => Error_Types.NoName,
                  Echo_Str     => Error);

            when Expn_May_Be_Undefined | Stmt_May_Be_Undefined =>
               Error_Context_Rec.Severity := Flow_Warning;
               Inc_Message_Count (Err_Type => Error_Types.CondlFlowErr);
               ErrorBuffer.Add
                 (Err_File     => File,
                  Err_Type     => Error_Types.CondlFlowErr,
                  Pos          => Position,
                  Scope        => Scope,
                  Error_Number => Data_Flow_Err_Type'Pos (Err_Type) + Error_Types.CondFlowErrorOffset,
                  Reference    => No_Reference,
                  Name1        => Symbol_To_Name (Sym => Var_Sym),
                  Name2        => Error_Types.NoName,
                  Name3        => Error_Types.NoName,
                  Echo_Str     => Error);
         end case;
         Error_Context_Rec.Errs := File;
         EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      end if;
   end Data_Flow_Error;

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

   procedure Ineffective_Stmt
     (Position : in LexTokenManager.Token_Position;
      Var_Sym  : in Dictionary.Symbol;
      Scope    : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State  from *,
   --#                                 CommandLineData.Content,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 Var_Sym &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 SPARK_IO.File_Sys,
   --#                                 Var_Sym &
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 Var_Sym &
   --#         Total_Error_Count  from *,
   --#                                 CommandLineData.Content,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Var_Sym;
   is
      Error              : Error_Types.StringError;
      File               : Error_IO.File_Type;
      Error_Is_Justified : Boolean;
   begin
      Justifications.Check_Whether_Justified
        (Which_Table => Error_Context_Rec.Justifications_Data_Table,
         Line        => Position,
         Kind        => Flow_Message,
         Err_Num     => 10,
         Identifiers => Justification_Identifiers'(1      => Symbol_To_Justification_Identifier (Sym => Var_Sym),
                                                   others => Null_Justification_Identifier),
         Match_Found => Error_Is_Justified);
      if Error_Is_Justified then
         Inc_Total_Justified_Warnings;
      else
         Error_Context_Rec.Severity := Flow_Errs;
         Inc_Message_Count (Err_Type => Error_Types.UncondFlowErr);
         File := Error_Context_Rec.Errs;
         ErrorBuffer.Add
           (Err_File     => File,
            Err_Type     => Error_Types.IneffectiveStat,
            Pos          => Position,
            Scope        => Scope,
            Error_Number => 10,
            Reference    => No_Reference,
            Name1        => Symbol_To_Name (Sym => Var_Sym),
            Name2        => Error_Types.NoName,
            Name3        => Error_Types.NoName,
            Echo_Str     => Error);
         Error_Context_Rec.Errs := File;
         EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      end if;
   end Ineffective_Stmt;

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

   procedure Stability_Error
     (Err_Type        : in Stability_Err_Type;
      Position        : in LexTokenManager.Token_Position;
      Stability_Index : in Index_Type)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Stability_Index &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 SPARK_IO.File_Sys,
   --#                                 Stability_Index &
   --#         Total_Error_Count  from *,
   --#                                 CommandLineData.Content,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position;
   is
      Error              : Error_Types.StringError;
      File               : Error_IO.File_Type;
      Error_Is_Justified : Boolean;
   begin
      Justifications.Check_Whether_Justified
        (Which_Table => Error_Context_Rec.Justifications_Data_Table,
         Line        => Position,
         Kind        => Flow_Message,
         Err_Num     => Stability_Err_Type'Pos (Err_Type) + Error_Types.StabilityErrOffset,
         Identifiers => Null_Justification_Identifiers,
         Match_Found => Error_Is_Justified);

      if Error_Is_Justified then
         Inc_Total_Justified_Warnings;
      else
         Error_Context_Rec.Severity := Flow_Errs;
         Inc_Message_Count (Err_Type => Error_Types.UncondFlowErr);
         File := Error_Context_Rec.Errs;
         ErrorBuffer.Add
           (Err_File     => File,
            Err_Type     => Error_Types.StabilityErr,
            Pos          => Position,
            Scope        => Dictionary.GlobalScope,
            Error_Number => Stability_Err_Type'Pos (Err_Type) + Error_Types.StabilityErrOffset,
            Reference    => No_Reference,
            Name1        => Error_Types.Names'(Name_Sort => Error_Types.StabilityIndex,
                                               Name_Sym  => Dictionary.NullSymbol,
                                               Name_Str  => LexTokenManager.Null_String,
                                               Pos       => Index_Type'Pos (Stability_Index)),
            Name2        => Error_Types.NoName,
            Name3        => Error_Types.NoName,
            Echo_Str     => Error);
         Error_Context_Rec.Errs := File;
         EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      end if;
   end Stability_Error;

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

   procedure Dependency_Error
     (Err_Type       : in Dependency_Err_Type;
      Position       : in LexTokenManager.Token_Position;
      Import_Var_Sym : in Dictionary.Symbol;
      Export_Var_Sym : in Dictionary.Symbol;
      Scope          : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State  from *,
   --#                                 CommandLineData.Content,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 Export_Var_Sym,
   --#                                 Import_Var_Sym,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 Export_Var_Sym,
   --#                                 Import_Var_Sym,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 SPARK_IO.File_Sys &
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 Export_Var_Sym,
   --#                                 Import_Var_Sym,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope &
   --#         Total_Error_Count  from *,
   --#                                 CommandLineData.Content,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 Export_Var_Sym,
   --#                                 Import_Var_Sym,
   --#                                 LexTokenManager.State,
   --#                                 Position;
   is
      Error              : Error_Types.StringError;
      File               : Error_IO.File_Type;
      Error_Is_Justified : Boolean;
   begin
      case Err_Type is
         when Not_Used | Ineff_Init | Ineff_Local_Init | Policy_Violation =>
            -- Unconditional error cases

            Justifications.Check_Whether_Justified
              (Which_Table => Error_Context_Rec.Justifications_Data_Table,
               Line        => Position,
               Kind        => Flow_Message,
               Err_Num     => Dependency_Err_Type'Pos (Err_Type) + Error_Types.UncondDependencyErrorOffset,
               Identifiers => Justification_Identifiers'(1 => Symbol_To_Justification_Identifier (Sym => Export_Var_Sym),
                                                         2 => Symbol_To_Justification_Identifier (Sym => Import_Var_Sym)),
               Match_Found => Error_Is_Justified);

            if Error_Is_Justified then
               Inc_Total_Justified_Warnings;
            else
               File                       := Error_Context_Rec.Errs;
               Error_Context_Rec.Severity := Flow_Errs;
               Inc_Message_Count (Err_Type => Error_Types.UncondDependencyErr);
               ErrorBuffer.Add
                 (Err_File     => File,
                  Err_Type     => Error_Types.UncondDependencyErr,
                  Pos          => Position,
                  Scope        => Scope,
                  Error_Number => Dependency_Err_Type'Pos (Err_Type) + Error_Types.UncondDependencyErrorOffset,
                  Reference    => No_Reference,
                  Name1        => Symbol_To_Name (Sym => Import_Var_Sym),
                  Name2        => Symbol_To_Name (Sym => Export_Var_Sym),
                  Name3        => Error_Types.NoName,
                  Echo_Str     => Error);
               Error_Context_Rec.Errs := File;
               EchoErrorEntry (SPARK_IO.Standard_Output, Error);
            end if;

         when May_Be_Used | Uninitialised | Integrity_Violation | May_Be_Integrity_Violation =>
            -- Conditional error cases

            Justifications.Check_Whether_Justified
              (Which_Table => Error_Context_Rec.Justifications_Data_Table,
               Line        => Position,
               Kind        => Flow_Message,
               Err_Num     => Dependency_Err_Type'Pos (Err_Type) + Error_Types.CondDependencyErrorOffset,
               Identifiers => Justification_Identifiers'(1 => Symbol_To_Justification_Identifier (Sym => Export_Var_Sym),
                                                         2 => Symbol_To_Justification_Identifier (Sym => Import_Var_Sym)),
               Match_Found => Error_Is_Justified);

            if Error_Is_Justified then
               Inc_Total_Justified_Warnings;
            else
               File                       := Error_Context_Rec.Errs;
               Error_Context_Rec.Severity := Flow_Warning;
               Inc_Message_Count (Err_Type => Error_Types.CondlDependencyErr);
               ErrorBuffer.Add
                 (Err_File     => File,
                  Err_Type     => Error_Types.CondlDependencyErr,
                  Pos          => Position,
                  Scope        => Scope,
                  Error_Number => Dependency_Err_Type'Pos (Err_Type) + Error_Types.CondDependencyErrorOffset,
                  Reference    => No_Reference,
                  Name1        => Symbol_To_Name (Sym => Import_Var_Sym),
                  Name2        => Symbol_To_Name (Sym => Export_Var_Sym),
                  Name3        => Error_Types.NoName,
                  Echo_Str     => Error);
               Error_Context_Rec.Errs := File;
               EchoErrorEntry (SPARK_IO.Standard_Output, Error);
            end if;
      end case;
   end Dependency_Error;

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

   procedure Usage_Error
     (Err_Type : in Usage_Err_Type;
      Position : in LexTokenManager.Token_Position;
      Var_Sym  : in Dictionary.Symbol;
      Scope    : in Dictionary.Scopes)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State  from *,
   --#                                 CommandLineData.Content,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 Var_Sym &
   --#         Echo_Accumulator,
   --#         Error_Context_Rec,
   --#         SPARK_IO.File_Sys  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 Echo_Accumulator,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 SPARK_IO.File_Sys,
   --#                                 Var_Sym &
   --#         ErrorBuffer.Buffer from *,
   --#                                 CommandLineData.Content,
   --#                                 Dictionary.Dict,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Scope,
   --#                                 Var_Sym &
   --#         Total_Error_Count  from *,
   --#                                 CommandLineData.Content,
   --#                                 Error_Context_Rec,
   --#                                 Err_Type,
   --#                                 LexTokenManager.State,
   --#                                 Position,
   --#                                 Var_Sym;
   is
      Error              : Error_Types.StringError;
      File               : Error_IO.File_Type;
      Error_Is_Justified : Boolean;
   begin
      Justifications.Check_Whether_Justified
        (Which_Table => Error_Context_Rec.Justifications_Data_Table,
         Line        => Position,
         Kind        => Flow_Message,
         Err_Num     => Usage_Err_Type'Pos (Err_Type) + Error_Types.UsageErrOffset,
         Identifiers => Justification_Identifiers'(1      => Symbol_To_Justification_Identifier (Sym => Var_Sym),
                                                   others => Null_Justification_Identifier),
         Match_Found => Error_Is_Justified);

      if Error_Is_Justified then
         Inc_Total_Justified_Warnings;
      else
         File                       := Error_Context_Rec.Errs;
         Error_Context_Rec.Severity := Flow_Errs;
         Inc_Message_Count (Err_Type => Error_Types.UncondDependencyErr);
         ErrorBuffer.Add
           (Err_File     => File,
            Err_Type     => Error_Types.UsageErr,
            Pos          => Position,
            Scope        => Scope,
            Error_Number => Usage_Err_Type'Pos (Err_Type) + Error_Types.UsageErrOffset,
            Reference    => No_Reference,
            Name1        => Symbol_To_Name (Sym => Var_Sym),
            Name2        => Error_Types.NoName,
            Name3        => Error_Types.NoName,
            Echo_Str     => Error);
         Error_Context_Rec.Errs := File;
         EchoErrorEntry (SPARK_IO.Standard_Output, Error);
      end if;
   end Usage_Error;

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

   procedure Put_Error_Pointers (Listing : in SPARK_IO.File_Type;
                                 Errors  : in Error_Sets)
   --# global in     CommandLineData.Content;
   --#        in     Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Errors,
   --#                                Error_Context_Rec,
   --#                                Listing;
   is
      Err_Pos      : Natural;
      Last_Err_Pos : Natural;
      Curr_Pos     : Natural;
      Err_Num      : Positive;
      First_One    : Boolean;

      function Width_Of (Err_Count : Natural) return Positive is
         Size : Positive;
      begin
         if Err_Count < 10 then
            Size := 1;
         elsif Err_Count < 100 then
            Size := 2;
         elsif Err_Count < 1000 then
            Size := 3;
         else
            Size := 4;
         end if;
         return Size;
      end Width_Of;

   begin
      Last_Err_Pos := 0;
      Curr_Pos     := 0;
      First_One    := True;

      --# assert True; -- for RTC generation

      for I in Error_Set_Positions range 1 .. Errors.Length loop

         --# assert True; -- for RTC generation

         if Error_Has_Position_Inline (Err_Type => Errors.Content (I).Error.ErrorType) then
            if First_One then
               Put_Spaces (File => Listing,
                           N    => Source_Line_Indent);
               First_One := False;
            end if;

            Err_Pos := Errors.Content (I).Error.Position.Start_Pos;

            if Err_Pos = 0 then
               Err_Pos := 1;
            end if;

            --# assert True; -- for RTC generation

            if Err_Pos = Last_Err_Pos then
               Put_Char (File => Listing,
                         Item => ',');
            else
               if Curr_Pos > Err_Pos then
                  New_Line (File    => Listing,
                            Spacing => 1);
                  Move_To_Indent
                    (Source_File => Listing,
                     Line        => Error_Context_Rec.Current_Line,
                     Indent      => Source_Line_Indent,
                     Position    => Err_Pos - 1);
               elsif Curr_Pos = 0 then
                  Move_To_Indent
                    (Source_File => Listing,
                     Line        => Error_Context_Rec.Current_Line,
                     Indent      => 0,
                     Position    => Err_Pos - 1);
               else
                  Put_Spaces (File => Listing,
                              N    => Err_Pos - Curr_Pos);
               end if;
               Curr_Pos := Err_Pos;
               Put_Char (File => Listing,
                         Item => '^');
            end if;
            Err_Num := Errors.Content (I).Err_Num;

            --# accept Flow, 41, "Mode-specific code";
            if CommandLineData.Content.Plain_Output then -- Expect stable condition
               Curr_Pos := Curr_Pos + 1;
            else
               Put_Integer (File  => Listing,
                            Item  => Err_Num,
                            Width => Width_Of (Err_Count => Err_Num),
                            Base  => 10);
               Curr_Pos := (Curr_Pos + Width_Of (Err_Count => Err_Num)) + 1;
            end if;
            --# end accept;

            Last_Err_Pos := Err_Pos;
         end if;
      end loop;

      --# assert True; -- for RTC generation

      if not First_One then
         New_Line (File    => Listing,
                   Spacing => 1);
      end if;
   end Put_Error_Pointers;

   procedure Put_Error_Messages
     (Listing     : in     SPARK_IO.File_Type;
      Errors      : in     Error_Sets;
      Start_Pos   : in     Natural;
      Accumulator : in out ErrorAccumulator.T)
   --# global in     CommandLineData.Content;
   --#        in out SPARK_IO.File_Sys;
   --# derives Accumulator       from *,
   --#                                Errors,
   --#                                Start_Pos &
   --#         SPARK_IO.File_Sys from *,
   --#                                Accumulator,
   --#                                CommandLineData.Content,
   --#                                Errors,
   --#                                Listing,
   --#                                Start_Pos;
   is
      The_Error      : Error_Struct;
      New_Start      : Natural;
      Started_Active : Boolean;
      Indent         : Natural;
      Line_Length    : Natural;
      Explanation    : E_Strings.T;
   begin

      Indent      := 11;
      Line_Length := Error_Line_Length;

      for I in Error_Set_Positions range 1 .. Errors.Length loop
         The_Error := Errors.Content (I);

         Started_Active := ErrorAccumulator.Is_Active (This => Accumulator);

         if ErrorAccumulator.Is_Active (This => Accumulator) then
            ErrorAccumulator.Add
              (This    => Accumulator,
               Error   => The_Error,
               End_Pos => Line_Length,
               Indent  => Indent,
               Listing => Listing);
         end if;

         if not ErrorAccumulator.Is_Active (This => Accumulator) then

            -- put a trailing blank line after compound messages.
            if Started_Active then
               New_Line (File    => Listing,
                         Spacing => 2);
            end if;

            Output_Error_Marker
              (File       => Listing,
               Err_Type   => The_Error.Error.ErrorType,
               Message_Id => The_Error.Error.MessageId,
               Err_Count  => The_Error.Err_Num);

            if ErrorAccumulator.Is_Error_Start (The_Error => The_Error.Error) then
               -- Message is of akind that will be "accumulated" before printing.  We don't want
               -- the explanation to appear over and over again, only once at the end of the completed
               -- message.  So we extract explanation from message here and pass it into ErrorAccumulator
               -- where it is stored and appended to the error mesage when a later Flush operation is
               -- performed.
               Split_String_At_Explanation (E_Str       => The_Error.Error.Message,
                                            Explanation => Explanation);
               PrintLine
                 (Listing      => Listing,
                  Start_Pos    => Start_Pos,
                  End_Pos      => Line_Length,
                  Indent       => Indent,
                  Line         => The_Error.Error.Message,
                  Add_New_Line => False,
                  New_Start    => New_Start);

               ErrorAccumulator.Start_Msg
                 (This         => Accumulator,
                  Start_Error  => The_Error,
                  Start_Indent => New_Start,
                  Explanation  => Explanation,
                  Line_Length  => Line_Length,
                  Indent       => Indent);  -- in rather than recalculate them in error accumulator
            else
               -- leave message text unchanged and display it
               --# accept Flow, 10, New_Start, "Returned parameter not needed in this case";
               PrintLine
                 (Listing      => Listing,
                  Start_Pos    => Start_Pos,
                  End_Pos      => Line_Length,
                  Indent       => Indent,
                  Line         => The_Error.Error.Message,
                  Add_New_Line => False,
                  New_Start    => New_Start);
               --# end accept;

               -- Terminate message
               New_Line (File    => Listing,
                         Spacing => 1);

            end if;

         end if;
      end loop;
   end Put_Error_Messages;

   procedure Put_Error_Messages_XML
     (Listing     : in     SPARK_IO.File_Type;
      Errors      : in     Error_Sets;
      Start_Pos   : in     Natural;
      Accumulator : in out ErrorAccumulator.T)
   --# global in out SPARK_IO.File_Sys;
   --#        in out XMLReport.State;
   --# derives Accumulator,
   --#         XMLReport.State   from *,
   --#                                Accumulator,
   --#                                Errors,
   --#                                Start_Pos &
   --#         SPARK_IO.File_Sys from *,
   --#                                Accumulator,
   --#                                Errors,
   --#                                Listing,
   --#                                Start_Pos,
   --#                                XMLReport.State;
   is
      The_Error      : Error_Struct;
      New_Start      : Natural;
      Started_Active : Boolean;
      Indent         : Natural;
      Line_Length    : Natural;
      Explanation    : E_Strings.T;
   begin

      Indent      := 0;
      Line_Length := XML_Error_Line_Length;

      for I in Error_Set_Positions range 1 .. Errors.Length loop
         The_Error               := Errors.Content (I);
         The_Error.Error.Message := SPARK_XML.Filter_String (Str => The_Error.Error.Message);

         Started_Active := ErrorAccumulator.Is_Active (This => Accumulator);

         if ErrorAccumulator.Is_Active (This => Accumulator) then
            ErrorAccumulator.Add
              (This    => Accumulator,
               Error   => The_Error,
               End_Pos => Line_Length,
               Indent  => Indent,
               Listing => Listing);
         end if;

         if not ErrorAccumulator.Is_Active (This => Accumulator) then

            if Started_Active then
               XMLReport.End_Message (Report => Listing);
               New_Line (File    => Listing,
                         Spacing => 1);
            end if;

            XMLReport.Start_Message
              (Class  => Get_Error_Class (Err_Class => The_Error.Error.ErrorType),
               Code   => Convert_Message_Id (Message_Id => The_Error.Error.MessageId,
                                             Err_Type   => The_Error.Error.ErrorType),
               Line   => Integer (The_Error.Error.Position.Start_Line_No),
               Offset => The_Error.Error.Position.Start_Pos,
               Report => Listing);

            if ErrorAccumulator.Is_Error_Start (The_Error => The_Error.Error) then
               -- Message is of akind that will be "accumulated" before printing.  We don't want
               -- the explanation to appear over and over again, only once at the end of the completed
               -- message.  So we extract explanation from message here and pass it into ErrorAccumulator
               -- where it is stored and appended to the error mesage when a later Flush operation is
               -- performed.
               Split_String_At_Explanation (E_Str       => The_Error.Error.Message,
                                            Explanation => Explanation);
               PrintLine
                 (Listing      => Listing,
                  Start_Pos    => Start_Pos,
                  End_Pos      => Line_Length,
                  Indent       => Indent,
                  Line         => The_Error.Error.Message,
                  Add_New_Line => False,
                  New_Start    => New_Start);

               ErrorAccumulator.Start_Msg
                 (This         => Accumulator,
                  Start_Error  => The_Error,
                  Start_Indent => New_Start,
                  Explanation  => Explanation,
                  Line_Length  => Line_Length,
                  Indent       => Indent);  -- in rather than recalculate them in error accumulator
            else
               -- leave message text unchanged and display it
               --# accept Flow, 10, New_Start, "Returned parameter not needed in this case";
               PrintLine
                 (Listing      => Listing,
                  Start_Pos    => Start_Pos,
                  End_Pos      => Line_Length,
                  Indent       => Indent,
                  Line         => The_Error.Error.Message,
                  Add_New_Line => False,
                  New_Start    => New_Start);
               --# end accept;

               -- Terminate message
               XMLReport.End_Message (Report => Listing);

            end if;
         end if;
      end loop;
   end Put_Error_Messages_XML;

   procedure PrintErrors (Listing : in SPARK_IO.File_Type;
                          Purpose : in Error_Types.ConversionRequestSource)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --# derives Conversions.State,
   --#         Error_Context_Rec  from CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Listing,
   --#                                 Purpose,
   --#                                 SPARK_IO.File_Sys &
   --#         ErrorBuffer.Buffer from * &
   --#         SPARK_IO.File_Sys  from *,
   --#                                 CommandLineData.Content,
   --#                                 Conversions.State,
   --#                                 Dictionary.Dict,
   --#                                 ErrorBuffer.Buffer,
   --#                                 Error_Context_Rec,
   --#                                 LexTokenManager.State,
   --#                                 Listing,
   --#                                 Purpose,
   --#                                 WarningStatus.SuppressionList;
      is separate;

   procedure AppendErrors (Report  : in SPARK_IO.File_Type;
                           Purpose : in Error_Types.ConversionRequestSource)
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out XMLReport.State;
   --# derives Conversions.State,
   --#         Error_Context_Rec,
   --#         XMLReport.State   from CommandLineData.Content,
   --#                                Conversions.State,
   --#                                Dictionary.Dict,
   --#                                Error_Context_Rec,
   --#                                LexTokenManager.State,
   --#                                Purpose,
   --#                                Report,
   --#                                SPARK_IO.File_Sys,
   --#                                XMLReport.State &
   --#         SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Conversions.State,
   --#                                Dictionary.Dict,
   --#                                Error_Context_Rec,
   --#                                LexTokenManager.State,
   --#                                Purpose,
   --#                                Report,
   --#                                WarningStatus.SuppressionList,
   --#                                XMLReport.State;
      is separate;

   procedure Index_Manager_Error
     (S                 : in String;
      Source_File       : in LexTokenManager.Lex_String;
      Line_No           : in Positive;
      Col_No            : in Positive;
      Token_String      : in E_Strings.T;
      Is_Token_Filename : in Boolean;
      Is_Fatal          : in Boolean)
   --# global in     CommandLineData.Content;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Error_Context_Rec;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Error_Context_Rec,
   --#         Total_Error_Count from *,
   --#                                Is_Fatal,
   --#                                WarningStatus.SuppressionList &
   --#         SPARK_IO.File_Sys from *,
   --#                                Col_No,
   --#                                CommandLineData.Content,
   --#                                Is_Fatal,
   --#                                Is_Token_Filename,
   --#                                LexTokenManager.State,
   --#                                Line_No,
   --#                                S,
   --#                                Source_File,
   --#                                Token_String,
   --#                                WarningStatus.SuppressionList;
   is
      Str        : E_Strings.T;
      Tmp_Col_No : Positive;
   begin
      if not Is_Fatal and then WarningStatus.Is_Suppressed (The_Element => Index_Manager_Duplicates) then
         Inc_Suppressed_Warning_Counter (Warning_Type => Index_Manager_Duplicates);
      else
         if Is_Fatal then
            Inc_Message_Count (Err_Type => Error_Types.SyntaxErr);
         else
            Inc_Message_Count (Err_Type => Error_Types.WarningWithoutPosition);
         end if;
         -- Adjust column number to take account of lookahead
         if Col_No > 1 then
            Tmp_Col_No := Col_No - 1;
         else
            Tmp_Col_No := Col_No;
         end if;
         Str := LexTokenManager.Lex_String_To_String (Lex_Str => Source_File);
         if E_Strings.Get_Length (E_Str => Str) > 0 then
            if CommandLineData.Content.Plain_Output or else CommandLineData.Content.Brief then
               Str := FileSystem.Just_File (Fn  => Str,
                                            Ext => True);
            end if;
         else
            Str := E_Strings.Empty_String;
         end if;

         if CommandLineData.Content.Brief then
            ScreenEcho.Put_ExaminerString (Str);
            ScreenEcho.Put_Char (':');
            ScreenEcho.Put_Integer (Line_No, 0, 10);
            ScreenEcho.Put_Char (':');
            ScreenEcho.Put_Integer (Tmp_Col_No, 0, 10);
            ScreenEcho.Put_String (": ");
            ScreenEcho.Put_String (S);
         else
            ScreenEcho.Put_String ("In index file ");
            ScreenEcho.Put_ExaminerString (Str);
            ScreenEcho.Put_String (" at line ");
            ScreenEcho.Put_Integer (Line_No, 0, 10);
            ScreenEcho.Put_String (" column ");
            ScreenEcho.Put_Integer (Tmp_Col_No, 0, 10);
            ScreenEcho.Put_String (": ");
            ScreenEcho.Put_String (S);
         end if;

         if E_Strings.Get_Length (E_Str => Token_String) > 0 then
            if Is_Token_Filename then
               if CommandLineData.Content.Plain_Output then
                  Str := FileSystem.Just_File (Fn  => Token_String,
                                               Ext => True);
               elsif CommandLineData.Content.Brief then
                  Str := FileSystem.Just_File (Fn  => Token_String,
                                               Ext => True);
               else
                  Str := Token_String;
               end if;
            else
               Str := Token_String;
            end if;
            ScreenEcho.Put_String (": ");
            ScreenEcho.Put_ExaminerLine (Str);
         else
            ScreenEcho.New_Line (1);
         end if;
      end if;
   end Index_Manager_Error;

   -- exported operations concerned with error justification mechanism ------------------------------

   procedure Start_Unit
   --# global in out Error_Context_Rec;
   --# derives Error_Context_Rec from *;
   is
   begin
      Justifications.Start_Unit (Which_Table => Error_Context_Rec.Justifications_Data_Table);
   end Start_Unit;

   procedure End_Unit
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in     WarningStatus.SuppressionList;
   --#        in out Conversions.State;
   --#        in out Echo_Accumulator;
   --#        in out ErrorBuffer.Buffer;
   --#        in out Error_Context_Rec;
   --#        in out Potential_Invalid_Value;
   --#        in out SPARK_IO.File_Sys;
   --#        in out Total_Error_Count;
   --# derives Conversions.State,
   --#         Echo_Accumulator,
   --#         ErrorBuffer.Buffer,
   --#         Error_Context_Rec,
   --#         Potential_Invalid_Value,
   --#         SPARK_IO.File_Sys,
   --#         Total_Error_Count       from *,
   --#                                      CommandLineData.Content,
   --#                                      Conversions.State,
   --#                                      Dictionary.Dict,
   --#                                      Echo_Accumulator,
   --#                                      ErrorBuffer.Buffer,
   --#                                      Error_Context_Rec,
   --#                                      LexTokenManager.State,
   --#                                      SPARK_IO.File_Sys,
   --#                                      WarningStatus.SuppressionList;
   is
      It : Justifications.Unmatched_Justification_Iterator;
   begin
      -- First report all justifications in the unit just being ended that have failed to match
      -- But only if we aren't ignoring justifications
      if CommandLineData.Content.Justification_Option /= CommandLineData.Ignore then
         Justifications.First_Unmatched_Justification (It          => It,
                                                       Which_Table => Error_Context_Rec.Justifications_Data_Table);
         while not Justifications.Is_Null_Iterator (It => It) loop
            Semantic_Warning
              (Err_Num  => 121,
               Position => Justifications.Error_Position (It => It),
               Id_Str   => LexTokenManager.Null_String);
            Justifications.Next_Unmatched_Justification (It          => It,
                                                         Which_Table => Error_Context_Rec.Justifications_Data_Table);
         end loop;
      end if;
      -- Then discard data for now-completed unit
      Justifications.End_Unit (Which_Table => Error_Context_Rec.Justifications_Data_Table);
   end End_Unit;

   procedure Start_Justification
     (Position                       : in     LexTokenManager.Token_Position;
      Line                           : in     LexTokenManager.Line_Numbers;
      Kind                           : in     Justification_Kinds;
      Err_Num                        : in     Natural;
      Identifiers                    : in     Justification_Identifiers;
      Applies_To_All                 : in     Boolean;
      Explanation                    : in     E_Strings.T;
      Maximum_Justifications_Reached :    out Boolean)
   --# global in out Error_Context_Rec;
   --# derives Error_Context_Rec              from *,
   --#                                             Applies_To_All,
   --#                                             Err_Num,
   --#                                             Explanation,
   --#                                             Identifiers,
   --#                                             Kind,
   --#                                             Line,
   --#                                             Position &
   --#         Maximum_Justifications_Reached from Error_Context_Rec;
   is
   begin
      Justifications.Start_Justification
        (Which_Table                    => Error_Context_Rec.Justifications_Data_Table,
         Position                       => Position,
         Line                           => Line,
         Kind                           => Kind,
         Err_Num                        => Err_Num,
         Identifiers                    => Identifiers,
         Applies_To_All                 => Applies_To_All,
         Explanation                    => Explanation,
         Maximum_Justifications_Reached => Maximum_Justifications_Reached);
   end Start_Justification;

   procedure End_Justification (Line          : in     LexTokenManager.Line_Numbers;
                                Unmatched_End :    out Boolean)
   --# global in out Error_Context_Rec;
   --# derives Error_Context_Rec,
   --#         Unmatched_End     from Error_Context_Rec,
   --#                                Line;
   is
   begin
      Justifications.End_Justification
        (Which_Table   => Error_Context_Rec.Justifications_Data_Table,
         Line          => Line,
         Unmatched_End => Unmatched_End);
   end End_Justification;

   procedure Set_File_Open_Error
   --# global out File_Open_Error;
   --# derives File_Open_Error from ;
   is
   begin
      File_Open_Error := True;
   end Set_File_Open_Error;

   function Get_Errors_Type return Exit_Code
   --# global in File_Open_Error;
   --#        in Total_Error_Count;
   is
      Return_Value : Exit_Code := 0;
   begin
      if File_Open_Error then
         Return_Value := 8;
      elsif Total_Error_Count.Explicit_Error_Count (Syntax_Or_Semantic) /= 0 then
         Return_Value := 3;
      elsif Total_Error_Count.Explicit_Error_Count (Flow) /= 0 then
         Return_Value := 2;
      elsif Total_Error_Count.Explicit_Error_Count (Warning) /= 0 then
         Return_Value := 1;
      end if;
      return Return_Value;
   end Get_Errors_Type;

begin
   Error_Context_Rec := Null_Error_Context;
   Echo_Accumulator  := ErrorAccumulator.Clear;
   Total_Error_Count := Null_Total_Error_Counts;
end ErrorHandler;