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

--------------------------------------------------------------------------------
--  ErrorHandler
--
--  Purpose:
--    The package ErrorHandler is used to report almost all warnings and errors
--    detected by the Examiner during analysis and produce summaries of the
--    number of warnings and errors encountered.
--
--    ErrorHandler is also responsible for the definition and suppression
--    of warnings specified in the warning control file (see Examiner User
--    Manual section 4.6)
--
--    The processing of justifications using the accept annotation
--   (see Examiner User Manual section 9.1) is also managed by ErrorHandler.
--
--    The Examiner will terminate with a status code dependent on whether an
--    error has occurred and if applicable the class of error.  The ErrorHandler
--    package provides a function for determining the status code.  The exit
--    codes are declared below.
--
--    Errors are accumulated as they are encountered in ErrorContexts.
--    The ErrorHandler only manages a single ErrorContext (represented
--    by the own variable ErrorContext) but an ErrorContext for each source
--    file read is maintained by the ContextManager.
--
--    The main ErrorHandler interface provides subprograms to manage
--    ErrorContexts, add various classes of errors and warnings to the
--    accumulated errors and others to initialize, reset and list or print the
--    accumulated warnings and errors or summaries thereof.
--
--    Another section of the ErrorHandler interface is concerned with the
--    Warning Control file and listing the warning messages that have been
--    suppressed.
--
--    A further part of the ErrorHandler interface manages Justifications.
--
--  Clients:
--    The ErrorHandler module is used for reporting almost all errors except
--    errors detected within the command line (See examiner.adb) and fatal
--    errors which immediately terminate the Examiner by calling
--    SystemErrors.FatalError.
--    Consequently ErrorHandler is used by many parts of the Examiner and has
--    many clients, for instance, the FlowAnalyser and Sem.
--    ErrorHandler is also used by SPARKmake.
--
--  Use:
--    Reporting Errors and ErrorContexts:
--
--    (1) When a source file (or configuration file) is opened initialize the
--        ErrorContext by calling ErrorHandler.ErrorInit
--       (or errorHandler.SparkMakeInit from SPARKmake).
--        This ErrorContext is retrieved by calling GetErrorContext and is
--        associated with the source file and saved by calling
--        ContextManager.SetContext (See mainloop.adb).
--
--    (2) For each compilation unit (or a configuration file) to be analysed
--        retrieve the ErrorContext associated with the file containing the
--        compilation unit by calling ContextManager.GetErrorContext and set
--        the current ErrorContext maintained by the ErrorHandler to the
--        retrieved ErrorContext by calling ErrorHandler.SetErrorContext
--        (See mainloop.adb)
--
--     (3) Prior to analysis a body or package initialization call
--         ErrorHandler.ErrorReset to reset the severity of the ErrorContext as
--         this property only applies to a single body or package
--         initialization (See sem-compunit.adb).
--
--     (4) To add a warning or error to the accumulated messages of the
--         ErrorContext call an appropriate interface subprogram from those
--         declared below.
--
--     (5) On completing analysis of each subprogram body
--        (subprogram_implementation) call ErrorHandler.FlushEchoMessages to
--         complete any messages relating to the subprogram that are sent to
--         the screen (standard output) (See sem-compunit.adb).
--
--     (6) After the analysis of each unit ErrorHandler.GetErrorSeverity may
--         be called to determine the worst severity of any errors encountered.
--         The severity levels are declared below (See sem-compunit.adb).
--
--     (7) Call ErrorHander.PrintErrors to generate a listing file annotated
--         with the accumulated error messages for the corresponding source
--         or configuration file (See mainloop.adb).
--
--         Call ErrorHandler.AppendErrors to add errors related to a source
--         or configuration file to the report file (see mainloop.adb).
--
--     (8) Call ErrorHandler.EchoTotalErrorCount after all files have been
--         analysed to display the total error count on the screen
--         (standard_output) (See mainloop.adb).
--
--     (9) Call ErrorHandler.GetErrorsType to obtain the exit code which
--         defines (the worst) type of error encountered during analysis.
--         See below for definition of values.
--
--    (10) If references to Ada LRM 83 or 95, SPARK 83 or 95,
--         Examiner User Manual, VCG or RTC Manuals or
--         Barnes "High Integrity Software" are associated with any warning or
--         error messages issued may be listed to a file by calling
--         ErrorHandler.OutputReferenceList. It is normally called to add
--         these to the report file unless the -brief switch is specified
--         (See mainloop.adb).
--
--    (11) If it is not possible to open any input file (configuration file,
--         meta file or source file), ErrorHandler.SetFileOpenError should
--         be called to register this failure.  The failure is not recorded as
--         part of an ErrorContext and related to a single file but as a
--         pervasive event (See mainloop.adb).
--
--     Warning File:
--
--     (1) Read in the warning control file by calling
--         ErrorHandler.ReadWarningFile (See mainloop.adb).
--
--         Warnings which are correctly designated in the warning control file
--         (see Examiner User Manual 9.2.1) will now be suppressed.
--
--     (2) A list of suppressed may be written to a file by calling
--         ErrorHandler.OutputWarningList.  It is called in mainloop.adb
--         to write the list to the report file.
--
--     Justifications using Accept Annotations:
--
--     (1) Call ErrorHandler.StartUnit when a new unit is to be analysed
--         (see sem-compunit.adb).
--
--     (2) Call ErrorHandler.StartJustification when an accept annoation is
--         encountered (See sem-compunit-wf_justification_statement.adb).
--
--         The errors justified by the accept annotation will no longer be
--         reported except in the justification summary.
--
--     (3) Call ErrorHandler.EndJustification when an end accept annotation is
--         encountered (See sem-compunit-wf_justification_statement.adb).
--
--     (4) Call ErrorHandler.EndUnit when the analysis of a unit is complete
--         (See sem-compunit.adb).
--
--  Extension:
--    Warnings:
--
--    To add a new warning
--
--    (1) Choose a unique warning number within the range defined by
--        Error_Types.ErrNumRange - distinct from any number listed
--        in the Examiner User Manual section 6.3 "Warning Messages".
--
--    (2) Consider whether the warning is to be suppressible and if suppressible
--        whether it is a severe warning.
--
--    (3) If it is to be suppressible a new keyword must be introduced.
--
--    If the warning is to be suppressible...
--
--    (4) Add a suitable enumeration element to the type Warning_Elements putting
--        it into the correct part of the list depending on whether it is a
--        severe (starred) warning or not.
--        Keep Unexpected_Address_Clauses as the last  non-severe element of
--        the enumeration or it corrupts the subtype definition of
--        "Severe_Warnings".
--
--    (5) In errorhandler-warningstatus.adb, procedure Get_Description,
--        add an extra case alternative to describe the new warning.
--
--    (6) In errorhandler-warningstatus-readwarningfile.adb extend procedure
--        Process_Option to recognise new keyword.
--
--    (7) In the body of ErrorHandler, in procedures Semantic_Warning_With_Position
--        or Semantic_Warning_Without_Position, add if/elsif clauses to increment
--        counters, rather than display warning, when suppression has been
--        selected.

--    For all warnings independent of suppression
--
--    (8) If the chosen error number is less than 400 add an extra case
--        alternative to procedure WarningWithPosition define the new warning
--        text and its explanation in file
--        errorhandler-conversions-tostring-warningwithposition.adb.
--
--        If the chosen error number is greater or equal to 400 add an extra
--        case alternative to procedure WarningWithoutPosition define the new
--        warning text and its explanation in file
--        errorhandler-conversions-tostring-warningwithoutposition.adb.
--
--        In either of the above two cases the format of the warning text to be
--        added is a catenation of strings to an E_String.T for the standard
--        warning text followed by a number of comment lines starting with --!.
--        The text in the comments starting with --! constitute the error
--        explanation which is given when the Examiner -error_explanation
--        command line switch is set to first or every_occurrence.
--
--        Two new files are automatically generated from the above two files
--        during the build process to provide SPARK procedures which incorporate
--        the error explanations see
--        errorhandler-conversions-tostring-warningwithposition-warningwithpositionexpl.adb and
--        errorhandler-conversions-tostring-warningwithoutposition-warningwithoutpositionexpl.adb.
--
--    To add a new note
--
--    (1) Choose a unique note number within the range defined by
--        Error_Types.ErrNumRange - distinct from any number listed
--        in the Examiner User Manual section 6.4 "Notes".
--
--    (2) Add an extra case alternative to procedure Note in
--        errorhandler-conversions-tostring-note.adb defining the text and
--        explanation of the note as described for warnings (8).
--
--    To add a new semantic error
--    (excluding those related to inconsistencies between abstract and refined
--     dependency relations)
--
--    (1) Choose a unique semantic error number within the range defined by
--        Error_Types.ErrNumRange - distinct from any number listed
--        in the Examiner User Manual section 6.2 "Semantic Errors".
--
--    (2) Add an extra case alternative to procedure SemanticErr in
--        errorhandler-conversions-tostring-semanticerr.adb defining the text
--        and explanation of the semantic error as described for warnings (8).
--
--    (3) If the error message contains a reference to a document which is
--        already in the list of document references maintained in
--        errorhandler-conversions-tostring-appendreference.adb, then when a
--        semantic error reporting subprogram is called the document reference
--        number may be given.
--
--    (4) If the message contains a reference to a document which is not in
--        the list of documents in
--        errorhandler-conversions-tostring-appendreference.adb then in the file
--        increment the value of the constant  MaxReferences and add a new
--        document reference as the last element of the constant array
--        ReferenceTable.
--
--    To add a new error related to inconsistencies between abstract and
--    refined dependency relations
--
--    (1) Choose a unique semantic error number within the range defined by
--        Error_Types.ErrNumRange - distinct from any number listed
--        in the Examiner User Manual section 8.3.7
--        "Inconsistencies between abstract and refined dependency relations".
--
--    (2) Add an extra case alternative to procedure DepSemanticErr in
--        errorhandler-conversions-tostring-depsemanticerr.adb defining the text
--        and explanation of the semantic error as described for warnings (8).
--
--    To add a new control-flow error
--
--    (1) Choose a unique control-flow error number within the range defined by
--        Error_Types.ErrNumRange - distinct from any number listed
--        in the Examiner User Manual section 7.2 "Control-flow Errors".
--
--    (2) Add a new enumeration literal to the type ControlFlowErrType declared
--        below to represent the new error.
--
--    (3) Add an extra case alternative to procedure ControlFlowError in
--        errorhandler-conversions-tostring-controlflowerror.adb defining the
--        text and explanation of the control-flow error as described for
--        warnings (8). Additionally associate the chosen error number
--        with the text using a comment with the syntax --! <name> ErrorNumber.
--
--    To add a new data-flow error
--
--    (1) Choose a unique data-flow error number within the range defined by
--        Error_Types.ErrNumRange - distinct from any number listed
--        in the Examiner User Manual section 8.3
--        "Data and information-flow Errors".
--
--    (2) Add a new enumeration literal to the type DataFlowErrType declared
--        below to represent the new error.
--
--    (3) In errorhandler.adb, procedure DataFlowError, add the new data-flow
--        enumeration to the appropriate alternative of the case statement
--        dependent on whether the new error is a conditional or unconditional
--        flow-error.
--
--    (4) Add an extra case alternative to either procedure CondlFlowErr or
--        procedure UncondFlowErr in
--        errorhandler-conversions-tostring-condlflowerr.adb or
--        errorhandler-conversions-tostring-uncondflowerr.adb respectively
--        defining the text and explanation of the data-flow error as described
--        for warnings (8). Additionally associate the chosen error number
--        with the text using a comment with the syntax --! <name> ErrorNumber.
--
--    To add a new information-flow error
--
--    (1) Choose a unique information-flow error number within the range defined
--        by Error_Types.ErrNumRange - distinct from any number listed
--        in the Examiner User Manual section 8.3
--        "Data and information-flow Errors".
--
--    (2) Add a new enumeration literal to one of the types FullDependErrType,
--        StabilityErrType, IndexType or UsageErrType dependent on the category
--        of the error to be reported.  If a new litereral is to be added to
--        FullDependencyErrType it must appear immediately before NotUsedNew so
--        that it is in the subtype DependencyErrType.
--
--    (3) If the error is of the subtype DependencyErrType determine whether
--        the error is a conditional or unconditional flow error and
--        Add the new enumeration literal to the appropriate case alternative
--        of the procedure DependencyError in errorhandler.adb.
--
--    (4) Add an extra case alternative to the appropriate procedure
--        CondlDependency, IneffectiveStatement, StabilityError,
--        UncondDependency or UsageError in
--        errorhandler-conversions-tostring-condldependency.adb
--        errorhandler-conversions-tostring-ineffectivestatement.adb
--        errorhandler-conversions-tostring-stabilityerror.adb
--        errorhandler-conversions-tostring-unconddependency.adb
--        errorhandler-conversions-tostring-usageerror.adb
--        respectively defining the text and explanation of the information-flow
--        error as described for warnings (8).
--        Additionally associate the chosen error number with the text using a
--        comment with the syntax --! <name> ErrorNumber.
--
--    Lexical and syntax errors are not extended in this package but are
--    extended within the SPARKLex and SPParser subsystems.
--
--    It is not expected that the Justification interface will be extended.
--
--------------------------------------------------------------------------------

with Dictionary;
with Error_IO;
with Error_Types;
with ExaminerConstants;
with E_Strings;
with LexTokenManager;
with SPARK_IO;
with SP_Expected_Symbols;
with SP_Symbols;

use type Dictionary.Scopes;
use type Dictionary.Symbol;
use type Error_Types.Error_Class;
use type Error_Types.Names;
use type Error_Types.NumericError;
use type Error_Types.StringError;
use type LexTokenManager.Line_Numbers;
use type LexTokenManager.Str_Comp_Result;
use type LexTokenManager.Token_Position;
use type SPARK_IO.File_Status;
use type SPARK_IO.File_Type;
use type SP_Expected_Symbols.SP_Ess_Sym_Range;
use type SP_Symbols.SP_Symbol;

pragma Elaborate_All (SPARK_IO);

--# inherit Ada.Characters.Handling,
--#         Ada.Characters.Latin_1,
--#         CommandLineData,
--#         CommandLineHandler,
--#         Dictionary,
--#         Error_IO,
--#         Error_Types,
--#         ExaminerConstants,
--#         E_Strings,
--#         FileSystem,
--#         LexTokenManager,
--#         ScreenEcho,
--#         SPARK_IO,
--#         SPARK_XML,
--#         SP_Expected_Symbols,
--#         SP_Relations,
--#         SP_Symbols,
--#         SystemErrors,
--#         XMLReport;

package ErrorHandler
--# own Error_Context;
--# initializes Error_Context;
is

   -- Used to define the most serious sort of error encountered in an analysis
   -- Fatal is most serious and No_Error the least.
   type Error_Level is (Fatal, Semantic_Errs, Flow_Errs, Flow_Warning, No_Error);

   -- Enumeration literals representing the different sorts of control-flow
   -- error that may be reported.
   type Control_Flow_Err_Type is (Misplaced_Exit, Misplaced_Return, Missing_Return, Return_In_Proc);

   -- Enumeration literals representing the different sorts of data-flow
   -- error that may be reported.
   type Data_Flow_Err_Type is (Expn_Undefined, Expn_May_Be_Undefined, Invariant_Exp, Stmt_Undefined, Stmt_May_Be_Undefined);

   -- Enumeration literals representing the different sorts of information-flow
   -- errors related to dependencies that may be reported.
   -- Only the enumeration literals contained within the subtype
   -- Dependency_Err_Type may be used externally.
   type Full_Depend_Err_Type is (
                                 Not_Used,
                                 May_Be_Used,
                                 Uninitialised,
                                 Ineff_Init, -- this is own var of embedded pack
                                 Ineff_Local_Init,
                                 Integrity_Violation,
                                 May_Be_Integrity_Violation,
                                 Policy_Violation,
                                 Not_Used_New,
                                 May_Be_Used_New,
                                 Not_Used_Continue,
                                 May_Be_Used_Continue);
   subtype Dependency_Err_Type is Full_Depend_Err_Type range Not_Used .. Policy_Violation;

   -- Enumeration literals representing the different sorts of information-flow
   -- errors related to stable conditional expressions that may be reported.
   type Stability_Err_Type is (Stable_Exit_Cond, Stable_Fork_Cond);

   -- Enumeration literals representing the different sorts of information-flow
   -- errors related to stable expressions in loops that may be reported.
   type Index_Type is (Index_Zero, Index_One, Larger_Index);

   -- Enumeration literals representing the different sorts of information-flow
   -- errors related miscellaneous errors that may be reported.
   type Usage_Err_Type is (
                           Unused_Import,
                           Undefined_Export,
                           Undefined_Var,
                           Unreferenced_Var,
                           Redefined_Import,
                           Ineffective_Import,
                           Referenced_But_Not_In_Partition,
                           Updated_But_Not_In_Partition,
                           Uninitialized_Protected_Element);

   type Err_Sym_Range is range 1 .. 5;
   --# assert Err_Sym_Range'Base is Short_Short_Integer; -- For GNAT

   -- An array of parser symbols used in reporting and recovering from
   -- syntax errors (see spparser.adb).
   type Err_Sym_List is array (Err_Sym_Range) of SP_Symbols.SP_Symbol;

   -- A list of enumeration literals representing each of the suppressible
   -- warnings (and a general literal for notes).
   -- The literals up to and including Main_Program_Precondition are considered
   -- to be severe warnings in that they detect uses that may affect the
   -- semantics of the program.
   -- When severe warnings are suppressed in the list of suppressed warnings
   -- issued by the Examiner they are suffixed with a '*' character.
   -- Non-severe warnings do not have a suffix character.
   type Warning_Elements is (Pragmas,
                             Hidden_Parts,
                             Handler_Parts,
                             Representation_Clauses,
                             Interrupt_Handlers,
                             Static_Expressions,
                             Style_Check_Casing,
                             External_Variable_Assignment,
                             Unchecked_Conversion,
                             Imported_Objects,
                             Real_RTCs,
                             Default_Loop_Assertions,
                             Expression_Reordering,
                             Unexpected_Address_Clauses,
                             Main_Program_Precondition,
                             -- those below are not "severe"
                             Proof_Function_Non_Boolean,
                             Proof_Function_Implicit,
                             Proof_Function_Refinement,
                             Direct_Updates,
                             With_Clauses,
                             Unused_Variables,
                             Unuseable_Private_Types,
                             Constant_Variables,
                             Type_Conversions,
                             SLI_Generation,
                             Index_Manager_Duplicates,
                             Declare_Annotations,
                             Others_Clauses,
                             Ada2005_Reserved_Words,
                             Obsolescent_Features,
                             Notes);

   -- "Severe" warnings are for language elements that potentially change the
   -- semantics of a program.  These are indicated with an additional note
   -- in the report file, even if they are suppressed.
   subtype Severe_Warnings is Warning_Elements range Pragmas .. Main_Program_Precondition;

   type Count is range 0 .. ExaminerConstants.MaxErrorsPerFile;
   --# assert Count'Base is Integer; -- for the Large Examiner

   -- An array of counters, one for eaach type of suppressible warning
   -- This forms part of the error context and is not expexted to be
   -- accessed externally.
   type Counters is array (Warning_Elements) of Count;

   ------- Types used for justification of expected errors and warnings --------

   -- A justification may be applied to a warning or a flow-error.
   type Justification_Kinds is (Flow_Message, Warning_Message);

   -- When a message is marked as expected it is unknown whether it will
   -- eventually have to match it using a LexString or Symbol (because the error
   -- may be added using, say, Semantic_Warning or Semantic_Warning_Sym).
   -- Since both forms available in wf_justification_statement
   -- both are stored in the justification table and the right one is picked
   -- when comparisons are needed.
   -- Note that we only have both values for simple identifier like X, if the
   -- item being added is of the form P.Q.X then we can only have, and only
   -- need, the symbol because warnings for objects of this form are always
   -- added with a symbol.
   type Justification_Identifier is record
      String_Form : LexTokenManager.Lex_String;
      Symbol_Form : Dictionary.Symbol;
   end record;

   Null_Justification_Identifier : constant Justification_Identifier :=
     Justification_Identifier'(String_Form => LexTokenManager.Null_String,
                               Symbol_Form => Dictionary.NullSymbol);

   -- A message that we may want to suppress may have more than one idenfiier
   -- that needs to match (e.g. information flow dependency errors).
   -- There are not any errors that refer to more than two but, in any case
   -- the behaviour is made generic by using an array of identifiers.
   Max_Justification_Identifier_Length : constant := 2;
   subtype Justification_Identifier_Index is Integer range 1 .. Max_Justification_Identifier_Length;
   type Justification_Identifiers is array (Justification_Identifier_Index) of Justification_Identifier;
   Null_Justification_Identifiers : constant Justification_Identifiers :=
     Justification_Identifiers'(others => Null_Justification_Identifier);

   ---------------- End of Justification type declarations ---------------------

   -- An Error_Context maintains all the warning and error information related
   -- to a single source or configuration file.
   type Error_Contexts is private;
   Null_Error_Context : constant Error_Contexts;

   -- This constant is used to indicate that the warning or error message
   -- does not refer to any document.
   -- At the moment references are represented as simple Natural numbers
   -- and the list of references is held as a array, Reference_Table declared in
   -- errorhandler-conversions-tostring-appendreference.adb.
   -- Currently there are 22 reference entries.  It would be better if this
   -- constant and the reference table were made more controlled and abstract.
   No_Reference : constant Natural := 0;

   -- Total_Error_Counts used to create summary counts of errors for
   -- screen echo at end of Examination.
   -- Note the special handling of the count of suppressed warnings
   -- which does not form part of the grand total.  This has been done for
   -- consistency with the way error counts in report files are generated.
   -- A total error count is maintained by ErrorHandler and it is not expected
   -- that this declaration will be used externally.
   type Counted_Error_Kinds is (Syntax_Or_Semantic, Flow, Warning);
   type Explicit_Error_Counts is array (Counted_Error_Kinds) of Count;
   type Total_Error_Counts is record
      Grand_Total          : Count;
      Explicit_Error_Count : Explicit_Error_Counts;
      Suppressed_Warnings  : Count;
      Justified_Warnings   : Count;
   end record;
   Null_Total_Error_Counts : constant Total_Error_Counts :=
     Total_Error_Counts'
     (Grand_Total          => Count'First,
      Explicit_Error_Count => Explicit_Error_Counts'(Counted_Error_Kinds => Count'First),
      Suppressed_Warnings  => Count'First,
      Justified_Warnings   => Count'First);

   -- Exit codes for the Examiner
   -- 0   = Success with no unjustified errors or warnings
   -- 1   = Unjustified Warnings
   -- 2   = Unjustified Flow Errors
   -- 3   = Syntax/Semantic Errors
   -- 4-7 = Reserved
   -- 8   = Invocation Error e.g. contradictory command-line switches
   -- 9   = Internal Error e.g. table overflow or internal exception
   subtype Exit_Code is Integer range 0 .. 9;

   -- Error numbers used when reporting success in automatic flow analysis mode
   No_Error_Default   : constant Error_Types.ErrNumRange := 0;
   No_Error_Info_Flow : constant Error_Types.ErrNumRange := 1;
   No_Error_Data_Flow : constant Error_Types.ErrNumRange := 2;

   -- Flushes any pending message text in the Echo_Accumulator, which is part of
   -- the Error_Context maintained by the Error_Handler, to the standard output.
   -- It should be called on the completion of analysis of each subprogram
   -- implementation.
   procedure Flush_Echo_Messages;
   --# global in out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from *,
   --#                                Error_Context;

   -- This subporgram initializes the current Error_Context and is called when
   -- a new source file or configuration file is opened for reading.
   procedure Error_Init (Source_File_Name : in E_Strings.T;
                         Echo             : in Boolean);
   --# global in     Dictionary.Dict;
   --#        in out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context     from *,
   --#                                Dictionary.Dict,
   --#                                Echo,
   --#                                Source_File_Name,
   --#                                SPARK_IO.File_Sys &
   --#         SPARK_IO.File_Sys from *,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Source_File_Name;

   -- This subprogram is similar to Error_Init but is for use by SPARKmake
   -- rather than the Examiner.
   procedure Spark_Make_Init;
   --# global in     Dictionary.Dict;
   --#        in out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context     from *,
   --#                                SPARK_IO.File_Sys &
   --#         SPARK_IO.File_Sys from *,
   --#                                Dictionary.Dict,
   --#                                Error_Context;

   -- Obtains the current Error_Context from the ErrorHandler.
   procedure Get_Error_Context (Context : out Error_Contexts);
   --# global in     Dictionary.Dict;
   --#        in out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Context,
   --#         Error_Context     from Error_Context,
   --#                                SPARK_IO.File_Sys &
   --#         SPARK_IO.File_Sys from *,
   --#                                Dictionary.Dict,
   --#                                Error_Context;

   -- Sets the current Error_Context of the ErrorHandler to the one supplied
   -- by the parameter Context.
   procedure Set_Error_Context (Context : in Error_Contexts);
   --# global in     Dictionary.Dict;
   --#        in out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from Context,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                SPARK_IO.File_Sys;

   -- Called prior to analysis of a body or package initialization
   -- to reset the severity property of the Error_Context and as
   -- this property only applies to a single body or package initialization.
   -- Similarly, the invalid value detection only applies to a single body
   -- and so this is also reset.
   procedure Error_Reset;
   --# global in out Error_Context;
   --# derives Error_Context from *;

   -- Returns the severity property from the current Error_Context.
   procedure Get_Error_Severity (Severity : out Error_Level);
   --# global in Error_Context;
   --# derives Severity from Error_Context;

   --  This function returns TRUE if a syntax error or a semantic
   --  error has already been met.
   function Syntax_Or_Semantic_Error return Boolean;
   --# global in Error_Context;

   -- True when the analysed body potentially contains invalid values
   -- from reading an external variable or using an unchecked conversion.
   function Possibly_Invalid_Values return Boolean;
   --# global in Error_Context;

   --  The function returns TRUE if we are still generating SLI.
   function Generate_SLI return Boolean;
   --# global in CommandLineData.Content;
   --#        in Error_Context;

   -- Called to report successful analysis of a unit.  A successful analysis
   -- may be determined by calling the procedure Get_Error_Severity.
   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 Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                SPARK_IO.File_Sys,
   --#                                Subprog_Str;

   -- Reports a warning that a hidden body has been encountered.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                SPARK_IO.File_Sys,
   --#                                Unit_Str,
   --#                                Unit_Typ;

   -- Reports a warning that a hidden exception handler has been encountered.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                SPARK_IO.File_Sys,
   --#                                Unit_Str,
   --#                                Unit_Typ;

   -- Reports a warning that an unrecognised representation clause has been
   -- encountered.
   procedure Representation_Clause (Position : in LexTokenManager.Token_Position);
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                SPARK_IO.File_Sys;

   -- Reports a warning that an unrecognised pragma has been encountered.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Pragma_Name,
   --#                                SPARK_IO.File_Sys;

   -- Warns that a cut point has been introduced into a loop by inserting a
   -- default assertion.
   procedure Add_Cut_Point (At_Line : LexTokenManager.Line_Numbers);
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from At_Line,
   --#                                CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                LexTokenManager.State,
   --#                                SPARK_IO.File_Sys;

   -- This subprogram is called to report a semantic warning involving a single
   -- named entity represented by a LexString.
   -- See the package header documentation for a description of warnings and
   -- their definition.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                Id_Str,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                SPARK_IO.File_Sys;

   --  This subprogram is called to report that we stop the SLI
   --  generation.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Id_Str,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                SPARK_IO.File_Sys;

   -- This subprogram is called to report a semantic warning involving a single
   -- named entity represented by a Dictionary.Symbol.
   -- See the package header documentation for a description of warnings and
   -- their definition.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys,
   --#                                Sym;

   -- This subprogram is called to report a note involving a single
   -- Reports a lexical error detected by SPARKlex.
   procedure Lex_Error (Error_Message, Recovery_Message : in String;
                        Error_Item                      : in LexTokenManager.Lex_Value);
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in out Error_Context;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys     from CommandLineData.Content,
   --#                                    Dictionary.Dict,
   --#                                    Error_Context,
   --#                                    Error_Item,
   --#                                    Error_Message,
   --#                                    LexTokenManager.State,
   --#                                    Recovery_Message,
   --#                                    SPARK_IO.File_Sys &
   --#         LexTokenManager.State from *,
   --#                                    Error_Item,
   --#                                    Error_Message,
   --#                                    Recovery_Message;

   -- Reports an error detected by SPParser.
   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 out Error_Context;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys     from CommandLineData.Content,
   --#                                    Current_Sym,
   --#                                    Dictionary.Dict,
   --#                                    Entry_Symbol,
   --#                                    Error_Context,
   --#                                    Error_Item,
   --#                                    LexTokenManager.State,
   --#                                    Non_Terminal_List,
   --#                                    No_Of_Non_Terminals,
   --#                                    No_Of_Terminals,
   --#                                    SPARK_IO.File_Sys,
   --#                                    Terminal_List &
   --#         LexTokenManager.State from *,
   --#                                    Current_Sym,
   --#                                    Entry_Symbol,
   --#                                    Error_Item,
   --#                                    Non_Terminal_List,
   --#                                    No_Of_Non_Terminals,
   --#                                    No_Of_Terminals,
   --#                                    Terminal_List;

   -- Reports on a syntax error recovery action taken by SPParser.
   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 out Error_Context;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys     from CommandLineData.Content,
   --#                                    Dictionary.Dict,
   --#                                    Error_Context,
   --#                                    LexTokenManager.State,
   --#                                    Next_Sym,
   --#                                    No_Of_Syms,
   --#                                    Recovery_Posn,
   --#                                    Replacement_Sym,
   --#                                    SPARK_IO.File_Sys,
   --#                                    Sym_List &
   --#         LexTokenManager.State from *,
   --#                                    Error_Context,
   --#                                    Next_Sym,
   --#                                    No_Of_Syms,
   --#                                    Recovery_Posn,
   --#                                    Replacement_Sym,
   --#                                    Sym_List;

   -- named entity represented by a LexString.
   -- See the package header documentation for a description of notes and
   -- their definition.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                Id_Str,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                SPARK_IO.File_Sys;

   -- This subprogram is called to report inconsistencies between abstract and
   -- refined dependency relations involving two named entities represented by
   -- LexStrings.
   -- See the package header documentation for a description of these errors and
   -- their definition.
   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 Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                Id_Str1,
   --#                                Id_Str2,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                SPARK_IO.File_Sys;

   -- This subprogram is called to report inconsistencies between abstract and
   -- refined dependency relations involving two named entities represented by
   -- Dictionary.Symbols.
   -- See the package header documentation for a description of these errors and
   -- their definition.
   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 Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys,
   --#                                Sym1,
   --#                                Sym2;

   -- This subprogram is called to report a semantic error involving a single
   -- named entity represented by a LexString.
   -- The parameter "Reference" facilitates referencing a document within
   -- the warning.  A list of document references is maintained in
   -- errorhandler-conversions-tostring-appendreference.adb.  If a document is
   -- not referenced then the constant ErrorHandler.No_Reference should be used
   -- to signify this.
   -- See the package header documentation for a description of semantic errors
   -- and their definition.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                Id_Str,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Reference,
   --#                                SPARK_IO.File_Sys;

   -- This subprogram is called to report a semantic error involving two
   -- named entitities represented by LexStrings.
   -- The parameter "Reference" facilitates referencing a document within
   -- the warning.  A list of document references is maintained in
   -- errorhandler-conversions-tostring-appendreference.adb.  If a document is
   -- not referenced then the constant ErrorHandler.No_Reference should be used
   -- to signify this.
   -- See the package header documentation for a description of semantic errors
   -- and their definition.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                Id_Str1,
   --#                                Id_Str2,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Reference,
   --#                                SPARK_IO.File_Sys;

   -- This subprogram is called to report a semantic error involving a single
   -- named entity represented by a Dictionary.Symbol.
   -- The parameter "Reference" facilitates referencing a document within
   -- the warning.  A list of document references is maintained in
   -- errorhandler-conversions-tostring-appendreference.adb.  If a document is
   -- not referenced then the constant ErrorHandler.No_Reference should be used
   -- to signify this.
   -- See the package header documentation for a description of semantic errors
   -- and their definition.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Reference,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys,
   --#                                Sym;

   -- This subprogram is called to report a semantic error involving two
   -- named entitities represented by Dictionary.Symbols.
   -- The parameter "Reference" facilitates referencing a document within
   -- the warning.  A list of document references is maintained in
   -- errorhandler-conversions-tostring-appendreference.adb.  If a document is
   -- not referenced then the constant ErrorHandler.No_Reference should be used
   -- to signify this.
   -- See the package header documentation for a description of semantic errors
   -- and their definition.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Reference,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys,
   --#                                Sym,
   --#                                Sym2;

   -- This subprogram is called to report a semantic error involving two
   -- named entitities represented one by a LexString and one by a
   -- Dictionary.Symbol.
   -- The parameter "Reference" facilitates referencing a document within
   -- the warning.  A list of document references is maintained in
   -- errorhandler-conversions-tostring-appendreference.adb.  If a document is
   -- not referenced then the constant ErrorHandler.No_Reference should be used
   -- to signify this.
   -- See the package header documentation for a description of semantic errors
   -- and their definition.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                Id_Str,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Reference,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys,
   --#                                Sym;

   -- This subprogram is called to report a semantic error involving three
   -- named entitities represented one by a LexString and two by
   -- Dictionary.Symbols.
   -- The parameter "Reference" facilitates referencing a document within
   -- the warning.  A list of document references is maintained in
   -- errorhandler-conversions-tostring-appendreference.adb.  If a document is
   -- not referenced then the constant ErrorHandler.No_Reference should be used
   -- to signify this.
   -- See the package header documentation for a description of semantic errors
   -- and their definition.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                Id_Str,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Reference,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys,
   --#                                Sym,
   --#                                Sym2;

   -- This subprogram is called to report a semantic error involving three
   -- named entitities represented by Dictionary.Symbols.
   -- The parameter "Reference" facilitates referencing a document within
   -- the warning.  A list of document references is maintained in
   -- errorhandler-conversions-tostring-appendreference.adb.  If a document is
   -- not referenced then the constant ErrorHandler.No_Reference should be used
   -- to signify this.
   -- See the package header documentation for a description of semantic errors
   -- and their definition.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Num,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Reference,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys,
   --#                                Sym,
   --#                                Sym2,
   --#                                Sym3;

   -- This subprogram is called to report a control-flow error.
   -- See the package header documentation for a description of control-flow
   -- errors and their definition.
   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 Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Type,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                SPARK_IO.File_Sys;

   -- This subprogram is called to report a data-flow error involving a single
   -- named entity represented by a Dictionary.Symbol.
   -- See the package header documentation for a description of data-flow errors
   -- and their definition.
   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 Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Type,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys,
   --#                                Var_Sym;

   -- This subprogram is called to report an ineffective statement involving a
   -- single named entity represented by a Dictionary.Symbol.
   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 Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys,
   --#                                Var_Sym;

   -- This subprogram is called to report a stable conditional or a stable
   -- expression in a loop.
   -- See the package header documentation for a description of information-flow
   -- errors and their definition.
   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 Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Type,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                SPARK_IO.File_Sys,
   --#                                Stability_Index;

   -- This subprogram is called to report a dependency error involving two
   -- named entitities, the imported and exported variables, represented by
   -- Dictionary.Symbols.
   -- See the package header documentation for a description of information-flow
   -- errors and their definition.
   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 Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Type,
   --#                                Export_Var_Sym,
   --#                                Import_Var_Sym,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys;

   -- This subprogram is called to report a usage error involving a single
   -- named entitity represented by a Dictionary.Symbol.
   -- See the package header documentation for a description of information-flow
   -- errors and their definition.
   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 Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                Err_Type,
   --#                                LexTokenManager.State,
   --#                                Position,
   --#                                Scope,
   --#                                SPARK_IO.File_Sys,
   --#                                Var_Sym;

   -- Read_Warning_File reads in and parses the warning control file specified on
   -- the command line.  It sets up an internal store (part of the state
   -- represented by the own variable Error_Context) which records which warnings
   -- have been suppressed by the inclusion of their keyword in the warning file.
   -- See the package header documentation for a description of the use of the
   -- warning file and the definition of suppressible warnings.
   procedure Read_Warning_File;
   --# global in     CommandLineData.Content;
   --#        in out Error_Context;
   --#        in out LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         LexTokenManager.State,
   --#         SPARK_IO.File_Sys     from CommandLineData.Content,
   --#                                    Error_Context,
   --#                                    LexTokenManager.State,
   --#                                    SPARK_IO.File_Sys;

   -- Output_Warning_List writes out a list of the warnings to the file parameter
   -- "To_File" that are currently suppressed based on the internal store of
   -- warnings suppressed by reading the warning control file (part of the state
   -- represented by the own variable Error_Context).
   -- See the package header documentation for a description of the use of the
   -- warning file and the definition of suppressible warnings.
   procedure Output_Warning_List (To_File : in SPARK_IO.File_Type);
   --# global in     CommandLineData.Content;
   --#        in     Error_Context;
   --#        in     LexTokenManager.State;
   --#        in out SPARK_IO.File_Sys;
   --#        in out XMLReport.State;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Error_Context,
   --#                                LexTokenManager.State,
   --#                                To_File,
   --#                                XMLReport.State &
   --#         XMLReport.State   from *,
   --#                                CommandLineData.Content,
   --#                                Error_Context;

   -- Output_Reference_List writes out a list of the document references that are
   -- associated with reported semantic erros to the file parameter "To_File"
   -- See the package header documentation for a description of semantic errors
   -- and document references.
   procedure Output_Reference_List (To_File : in SPARK_IO.File_Type);
   --# global in     CommandLineData.Content;
   --#        in     Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Error_Context,
   --#                                To_File;

   -- This subprogram writes a source listing to the file parameter "Listing"
   -- in which the accumulated reported warnings and errors are interspersed
   -- with program text to indicate the location of the warning or error.
   -- A table showing the successful justifications encountered in the source
   -- file and a summary of the suppressed warnings are appended to the end of
   -- the listing file.
   -- The parameter "Purpose" identifies the type of listing that is being
   -- generated and is used in conjunction with the -error_explanations command
   -- line switch to control the generation of extended messages.
   -- For this subprogram, given its use, it is likely that Purpose
   -- will either be For_Listing - indicating this is a sorce listing or
   -- For_Report_Indexed_Files used when listing the configuration file.
   procedure PrintErrors (Listing : in SPARK_IO.File_Type;
                          Purpose : in Error_Types.ConversionRequestSource);
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                LexTokenManager.State,
   --#                                Listing,
   --#                                Purpose,
   --#                                SPARK_IO.File_Sys;

   -- Append_Errors extends the report file passed as the parameter "Report"
   -- adding the accumulated errors from the current Error_Context.
   -- A table showing the successful justifications encountered within the
   -- current Error_Context and a summary of the suppressed warnings are
   -- added after the reported warnings and errors.
   -- The parameter "Purpose" identifies the type of listing that is being
   -- generated and is used in conjunction with the -error_explanations command
   -- line switch to control the generation of extended messages.
   -- For this subprogram, given its use, it is likely that Purpose
   -- will either be For_Report_Selected_Files - indicating this is a file that
   -- is explicitly given on the command line or in a meta file, or
   -- For_Report_Indexed_Files - indicating that this is a file which was accessed
   -- indirectly via an index file..
   procedure AppendErrors (Report  : in SPARK_IO.File_Type;
                           Purpose : in Error_Types.ConversionRequestSource);
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --#        in out XMLReport.State;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys,
   --#         XMLReport.State   from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                LexTokenManager.State,
   --#                                Purpose,
   --#                                Report,
   --#                                SPARK_IO.File_Sys,
   --#                                XMLReport.State;

   --  This procedure write at the standard output an error in an
   --  index file.
   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 out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context     from *,
   --#                                Is_Fatal &
   --#         SPARK_IO.File_Sys from *,
   --#                                Col_No,
   --#                                CommandLineData.Content,
   --#                                Error_Context,
   --#                                Is_Fatal,
   --#                                Is_Token_Filename,
   --#                                LexTokenManager.State,
   --#                                Line_No,
   --#                                S,
   --#                                Source_File,
   --#                                Token_String;

   -- When called writes the total warnings and errors encountered during the
   -- Examiner run to the standard output.
   procedure Echo_Total_Error_Count;
   --# global in     CommandLineData.Content;
   --#        in     Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                CommandLineData.Content,
   --#                                Error_Context;

   -- Call this subprogram if it is not possible to open a required input file
   -- during analysis.  It will record the fact that this has happened and
   -- it will be reflected in the exit code returned by a call to Get_Errors_Type.
   procedure Set_File_Open_Error;
   --# global in out Error_Context;
   --# derives Error_Context from *;

   -- At the end of an Examiner run call this subprogram to obtain an exit code
   -- reflecting the most severe type of error encountered during the run.
   -- The exit code so obtained can then be used in a call to Set_Exit_Status.
   function Get_Errors_Type return Exit_Code;
   --# global in Error_Context;

   ------ Exported calls concerned with the error justification mechanism ------

   -- Called at the start of analysis of each unit to initialize the
   -- justification state for the unit.
   -- The justification state is part of the state represented by the own
   -- variable Error_Context.
   procedure Start_Unit;
   --# global in out Error_Context;
   --# derives Error_Context from *;

   -- Called at the end of analysis of each unit to close the
   -- justification state for the unit.
   -- The justification state is part of the state represented by the own
   -- variable Error_Context.
   procedure End_Unit;
   --# global in     CommandLineData.Content;
   --#        in     Dictionary.Dict;
   --#        in     LexTokenManager.State;
   --#        in out Error_Context;
   --#        in out SPARK_IO.File_Sys;
   --# derives Error_Context,
   --#         SPARK_IO.File_Sys from CommandLineData.Content,
   --#                                Dictionary.Dict,
   --#                                Error_Context,
   --#                                LexTokenManager.State,
   --#                                SPARK_IO.File_Sys;

   -- Called when an accept annotation is encountered in the source text to
   -- register the justification.
   -- If the maximum allowed justifications within a unit has been reached when
   -- registering the justification the parameter Maximum_Justifications_Reached
   -- is True but justification is registered.
   -- The Maximum_Justifications_Reached is only ever set True once, when the
   -- table first fills up.  If the table is already full then False is returned.
   -- at the point of call where the table first fills, not at every call thereafter.
   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;
   --# derives Error_Context                  from *,
   --#                                             Applies_To_All,
   --#                                             Err_Num,
   --#                                             Explanation,
   --#                                             Identifiers,
   --#                                             Kind,
   --#                                             Line,
   --#                                             Position &
   --#         Maximum_Justifications_Reached from Error_Context;

   -- Called when an end accept annotation is encountered in the source text to
   -- end the scope of a justification.
   -- The parameter Unmatched_End returns True if there is no accept annotation
   -- matching the end accept annotation provided the Justification table
   -- is not full in which case it will always return False to avoid false
   -- alarms.
   procedure End_Justification (Line          : in     LexTokenManager.Line_Numbers;
                                Unmatched_End :    out Boolean);
   --# global in out Error_Context;
   --# derives Error_Context,
   --#         Unmatched_End from Error_Context,
   --#                            Line;

private --------------------------------------------------------------

   -- The following declarations define a Data Table which is a core component
   -- of the Justification structure.
   -- A Data_Table_Table_Entry defines a single element of the table and contains
   -- all the information associated with a single justification.
   -- Data_Tables defines the array of Data_Table_Entries which holds all the
   -- justifications for a unit.
   Max_Table_Entries : constant := ExaminerConstants.MaxJustificationsPerFile;
   type Data_Table_Ptr is range 0 .. Max_Table_Entries;
   type Data_Table_Entry is record
      Kind           : Justification_Kinds;
      Err_Num        : Natural;
      Identifiers    : Justification_Identifiers;
      Applies_To_All : Boolean;
      Explanation    : E_Strings.T;
      -- location of the justification clause for error reporting purposes
      Position : LexTokenManager.Token_Position;
      -- location of start justify (for multiple clauses this is the line of the justify statement as a whole)
      Start_Line : LexTokenManager.Line_Numbers;
      -- location of end justify or end of unit (const End_Line_Of_Unit_Marker) if there is no matching end justify
      End_Line    : LexTokenManager.Line_Numbers;
      End_Found   : Boolean;   -- explicit end justify found or not
      Match_Count : Natural;
      -- number of times this justification matched last line where match occurred linkage
      Match_Line : LexTokenManager.Line_Numbers;
      Previous   : Data_Table_Ptr;
   end record;
   -- Initializing constants for Data Tables
   End_Of_List            : constant Data_Table_Ptr   := 0;
   Empty_Data_Table_Entry : constant Data_Table_Entry :=
     Data_Table_Entry'
     (Kind           => Flow_Message,
      Err_Num        => 0,
      Identifiers    => Null_Justification_Identifiers,
      Applies_To_All => False,
      Explanation    => E_Strings.Empty_String,
      Position       => LexTokenManager.Token_Position'(Start_Line_No => 0,
                                                        Start_Pos     => 0),
      Start_Line     => 0,
      End_Line       => 0,
      End_Found      => False,
      Match_Count    => 0,
      Match_Line     => 0,
      Previous       => End_Of_List);

   -- Data_Tables defines the array of Data_Table_Entries representing all the
   -- justifications for a unit.
   subtype Data_Table_Index is Data_Table_Ptr range 1 .. Max_Table_Entries;
   type Data_Tables is array (Data_Table_Index) of Data_Table_Entry;
   -- Initializing constant
   Empty_Data_Table : constant Data_Tables := Data_Tables'(Data_Table_Index => Empty_Data_Table_Entry);

   -- The Stack is the second major component of the justification structure
   -- A Stack_Record is a single element of the stack, Unit_Stack_Array is the
   -- stack storage and Unit_Stacks is the complete stack including a stack
   -- pointer.
   Max_Stack_Size : constant := 10; -- Perhaps move this to ExaminerConstants later
   type Stack_Ptrs is range 0 .. Max_Stack_Size;
   subtype Stack_Index is Stack_Ptrs range 1 .. Max_Stack_Size;
   type Stack_Record is record
      List_Items             : Data_Table_Ptr;
      Semantic_Error_In_Unit : Boolean;
   end record;
   type Unit_Stack_Array is array (Stack_Index) of Stack_Record;
   type Unit_Stacks is record
      Vector : Unit_Stack_Array;
      Ptr    : Stack_Ptrs;
   end record;
   -- initializing constant
   Empty_Stack : constant Unit_Stacks :=
     Unit_Stacks'
     (Ptr    => 0,
      Vector => Unit_Stack_Array'(Stack_Index => Stack_Record'(List_Items             => End_Of_List,
                                                               Semantic_Error_In_Unit => False)));

   -- The justification structure including a Data_Table, a Unit_Stack, a pointer
   -- for the current entry in the Data_Table and a Boolean indicating whether
   -- the justification table is accepting more entries (is not full).
   type Justifications_Data_Tables is record
      Data_Table             : Data_Tables;
      Current_Slot           : Data_Table_Ptr;
      Accepting_More_Entries : Boolean;
      Unit_Stack             : Unit_Stacks;
   end record;
   -- initializing constant
   Empty_Justifications_Data_Table : constant Justifications_Data_Tables :=
     Justifications_Data_Tables'
     (Data_Table             => Empty_Data_Table,
      Current_Slot           => End_Of_List,
      Accepting_More_Entries => True,
      Unit_Stack             => Empty_Stack);
   --------- End of justification table data structure definitions -------------

   -- We can now declare the actual announced private type
   -- The private type Error_Contexts contains a Justification_Table which is
   -- itself a complex data structure used to track the justification of
   -- expected flow errors and warnings.
   -- It is part of Error_Contexts because we need a different copy of the data
   -- structure for each file we are examining.
   -- The data structure types can be declared here because they are only used
   -- in the body of ErrorHandler and in the embedded package Justifications.
   --
   -- More details of the rationale for the Justifications Table data structure
   -- can be found in ErrorHandler.Justifications.adb
   --
   type Error_Contexts is record
      Recovery_Messages         : Boolean;
      Echo                      : Boolean;
      Severity                  : Error_Level;
      Num_Errs                  : Count;
      Num_Message               : Count;
      Line_No                   : LexTokenManager.Line_Numbers;
      Current_Line              : E_Strings.T;
      Errs                      : Error_IO.File_Type;
      Source                    : SPARK_IO.File_Type;
      Source_File_Name          : E_Strings.T;
      Counter                   : Counters;
      Justifications_Data_Table : Justifications_Data_Tables;
   end record;

   Null_Error_Context : constant Error_Contexts :=
     Error_Contexts'
     (Recovery_Messages         => False,
      Echo                      => False,
      Severity                  => Error_Level'First,
      Num_Errs                  => Count'First,
      Num_Message               => Count'First,
      Line_No                   => LexTokenManager.Line_Numbers'First,
      Current_Line              => E_Strings.Empty_String,
      Errs                      => Error_IO.Null_File,
      Source                    => SPARK_IO.Null_File,
      Source_File_Name          => E_Strings.Empty_String,
      Counter                   => Counters'(others => Count'First),
      Justifications_Data_Table => Empty_Justifications_Data_Table);
end ErrorHandler;