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

with CommandLineData;
with Fatal;
with ScreenEcho;
with Version;

package body SystemErrors is

   type Error_Kinds is (Static_Limit, Operating_System_Limit, Internal_Error);

   type Sys_Err_To_Err_Kind_Table is array (Sys_Err_Type) of Error_Kinds;

   SETEK : constant Sys_Err_To_Err_Kind_Table :=
     Sys_Err_To_Err_Kind_Table'
     (String_Table_Overflow                    => Static_Limit,
      Syntax_Tree_Overflow                     => Static_Limit,
      Parse_Stack_Overflow                     => Static_Limit,
      Symbol_Table_Overflow_Dynamic            => Operating_System_Limit,
      Invalid_Syntax_Tree                      => Internal_Error,
      Invalid_Symbol_Table                     => Internal_Error,
      Empty_Heap                               => Static_Limit,
      Relation_Stack_Overflow                  => Static_Limit,
      Relation_Stack_Underflow                 => Internal_Error,
      Invalid_Init                             => Internal_Error,
      Error_Position_Wrong                     => Internal_Error,
      Expression_Stack_Corrupt                 => Internal_Error,
      Expression_Stack_Underflow               => Internal_Error,
      Expression_Stack_Overflow                => Static_Limit,
      Type_Context_Stack_Corrupt               => Internal_Error,
      Type_Context_Stack_Underflow             => Internal_Error,
      Type_Context_Stack_Overflow              => Static_Limit,
      List_Overflow_In_Expression              => Static_Limit,
      List_Overflow_In_Dependency_Clause       => Static_Limit,
      List_Overflow_In_Procedure_Call          => Static_Limit,
      Case_Stack_Underflow                     => Internal_Error,
      Case_Stack_Overflow                      => Static_Limit,
      VCG_Graph_Size_Exceeded                  => Static_Limit,
      VCG_Heap_Is_Exhausted                    => Static_Limit,
      VCG_Heap_Is_Corrupted                    => Internal_Error,
      Ref_List_Key_Cell_Missing                => Internal_Error,
      Flow_Analyser_Expression_Limit           => Static_Limit,
      Case_Statement_Nesting_Limit             => Static_Limit,
      Error_Handler_Temporary_Files            => Operating_System_Limit,
      Error_Handler_Source                     => Operating_System_Limit,
      Disk_Full_Error                          => Operating_System_Limit,
      Math_Error                               => Internal_Error,
      Too_Many_Nested_Arrays                   => Static_Limit,
      Too_Many_Nested_Records                  => Static_Limit,
      Context_Unit_Stack_Overflow              => Static_Limit,
      Context_Unit_Stack_Underflow             => Internal_Error,
      Context_File_Heap_Overflow               => Static_Limit,
      Context_Unit_Heap_Overflow               => Static_Limit,
      Too_Many_File_Lines                      => Static_Limit,
      Index_Stack_Full                         => Static_Limit,
      Index_Component_List_Full                => Static_Limit,
      Too_Many_Errors                          => Static_Limit,
      Warning_Name_Too_Long                    => Static_Limit,
      Unit_Name_In_Index_Too_Long              => Static_Limit,
      File_Name_In_Index_Too_Long              => Static_Limit,
      Too_Many_Suppressed_Warnings             => Static_Limit,
      Unit_Nesting_Too_Deep                    => Static_Limit,
      Statement_Stack_Underflow                => Internal_Error,
      Statement_Stack_Overflow                 => Static_Limit,
      Wf_Compilation_Unit_Stack_Overflow       => Static_Limit,
      Wf_Compilation_Unit_Stack_Underflow      => Internal_Error,
      Too_Many_Flow_Analyser_Expressions       => Static_Limit,
      Too_Many_Params_In_Procedure_Call        => Static_Limit,
      Statistics_Usage_Greater_Than_Table_Size => Static_Limit,
      Aggregate_Stack_Under_Flow               => Internal_Error,
      Aggregate_Stack_Over_Flow                => Static_Limit,
      Meta_File_Stack_Overflow                 => Static_Limit,
      Lex_Stack_Overflow                       => Static_Limit,
      Lex_Stack_Underflow                      => Internal_Error,
      Component_Manager_Overflow               => Static_Limit,
      Component_Error_Overflow                 => Static_Limit,
      Syntax_Tree_Walk_Error                   => Internal_Error,
      Precondition_Failure                     => Internal_Error,
      Postcondition_Failure                    => Internal_Error,
      Assertion_Failure                        => Internal_Error,
      Unimplemented_Feature                    => Internal_Error,
      XML_Schema_Error                         => Internal_Error,
      XML_Generation_Error                     => Internal_Error,
      Illegal_XML_Generation_Attempt           => Internal_Error,
      String_Over_Flow                         => Internal_Error,
      Queue_Overflow                           => Static_Limit,
      XRef_Table_Full                          => Operating_System_Limit,
      Invalid_Index                            => Internal_Error,
      Other_Internal_Error                     => Internal_Error);

   procedure Stop_Program (Error_Kind : in Error_Kinds)
   --# derives null from Error_Kind;
   --# post False; -- does not terminate normally
   is
      --# hide Stop_Program;
   begin
      case Error_Kind is
         when Static_Limit =>
            raise Fatal.Static_Limit;
         when Operating_System_Limit =>
            raise Fatal.Operating_System_Limit;
         when Internal_Error =>
            raise Fatal.Internal_Error;
      end case;
   end Stop_Program;

   procedure Display_Cause (Error_Kind : in Error_Kinds)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Error_Kind;
   is
   begin
      case Error_Kind is
         when Static_Limit =>
            ScreenEcho.Put_Line ("* Internal static tool limit reached");
         when Operating_System_Limit =>
            ScreenEcho.Put_Line ("* Operating system limit reached");
         when Internal_Error =>
            ScreenEcho.Put_Line ("* Unexpected internal error");
      end case;
   end Display_Cause;

   procedure Display_Box (Sys_Err : in Sys_Err_Type;
                          Msg     : in String)
   --# global in out SPARK_IO.File_Sys;
   --# derives SPARK_IO.File_Sys from *,
   --#                                Msg,
   --#                                Sys_Err;
   is
   begin
      -- print 'big box' on screen to draw attention to error
      ScreenEcho.Put_Line ("*****************************************************************************");
      ScreenEcho.Put_Line ("* A fatal error has occurred");
      ScreenEcho.Put_String ("* ");

      case Sys_Err is
         when String_Table_Overflow =>
            ScreenEcho.Put_Line ("String table overflow");
         when Syntax_Tree_Overflow =>
            ScreenEcho.Put_Line ("Syntax tree overflow");
         when Parse_Stack_Overflow =>
            ScreenEcho.Put_Line ("Parse stack overflow");
         when Symbol_Table_Overflow_Dynamic =>
            ScreenEcho.Put_Line ("Symbol table allocation overflow");
         when Invalid_Syntax_Tree =>
            ScreenEcho.Put_Line ("Invalid syntax tree");
         when Invalid_Symbol_Table =>
            ScreenEcho.Put_Line ("Internal Symbol Table Error");
         when Empty_Heap =>
            ScreenEcho.Put_Line ("Empty heap");
         when Relation_Stack_Overflow =>
            ScreenEcho.Put_Line ("Relation stack overflow");
         when Relation_Stack_Underflow =>
            ScreenEcho.Put_Line ("Relation stack underflow");
         when Invalid_Init =>
            ScreenEcho.Put_Line ("Failure in initialisation");
         when Error_Position_Wrong =>
            ScreenEcho.Put_Line ("An error is incorrectly positioned");
         when Expression_Stack_Corrupt =>
            ScreenEcho.Put_Line ("The expression stack is corrupt");
         when Expression_Stack_Underflow =>
            ScreenEcho.Put_Line ("Expression stack underflow");
         when Expression_Stack_Overflow =>
            ScreenEcho.Put_Line ("Expression stack overflow");
         when Type_Context_Stack_Corrupt =>
            ScreenEcho.Put_Line ("The type context stack is corrupt");
         when Type_Context_Stack_Underflow =>
            ScreenEcho.Put_Line ("Type context stack underflow");
         when Type_Context_Stack_Overflow =>
            ScreenEcho.Put_Line ("Type context stack overflow");
         when List_Overflow_In_Expression =>
            ScreenEcho.Put_Line ("List overflow in expression");
         when List_Overflow_In_Dependency_Clause =>
            ScreenEcho.Put_Line ("List overflow in dependency clause");
         when List_Overflow_In_Procedure_Call =>
            ScreenEcho.Put_Line ("List overflow in procedure call");
         when Case_Stack_Underflow =>
            ScreenEcho.Put_Line ("Case statement stack underflow");
         when Case_Stack_Overflow =>
            ScreenEcho.Put_Line ("Case statement stack overflow");
         when VCG_Graph_Size_Exceeded =>
            ScreenEcho.Put_Line ("Maximum graph size in VC Generator exceeded");
         when VCG_Heap_Is_Exhausted =>
            ScreenEcho.Put_Line ("VC Generator Heap is Exhausted");
         when VCG_Heap_Is_Corrupted =>
            ScreenEcho.Put_Line ("VC Generator Heap is Corrupted");
         when Ref_List_Key_Cell_Missing =>
            ScreenEcho.Put_Line ("Referenced Variable List Error");
         when Flow_Analyser_Expression_Limit =>
            ScreenEcho.Put_Line ("Flow analyser expression limit reached");
         when Case_Statement_Nesting_Limit =>
            ScreenEcho.Put_Line ("Case statement nesting limit reached");
         when Error_Handler_Temporary_Files =>
            ScreenEcho.Put_Line ("Unable to open temporary file in ErrorHandler");
         when Error_Handler_Source =>
            ScreenEcho.Put_Line ("Unable to open source file in ErrorHandler");
         when Disk_Full_Error =>
            ScreenEcho.Put_Line ("File write operation failed, disk is full");
         when Math_Error =>
            ScreenEcho.Put_Line ("Internal error in static expression evaluator");
         when Too_Many_Nested_Arrays =>
            ScreenEcho.Put_Line ("Array constant nested too deeply");
         when Too_Many_Nested_Records =>
            ScreenEcho.Put_Line ("Record constant nested too deeply");
         when Context_Unit_Stack_Overflow =>
            ScreenEcho.Put_Line ("Too many pending units in context manager");
         when Context_Unit_Stack_Underflow =>
            ScreenEcho.Put_Line ("Internal error in context manager: stack underflow");
         when Context_File_Heap_Overflow =>
            ScreenEcho.Put_Line ("Too many files in examination");
         when Context_Unit_Heap_Overflow =>
            ScreenEcho.Put_Line ("Too many units in examination");
         when Too_Many_File_Lines =>
            ScreenEcho.Put_Line ("Too many lines in source file");
         when Index_Stack_Full =>
            ScreenEcho.Put_Line ("Index files too deeply nested");
         when Index_Component_List_Full =>
            ScreenEcho.Put_Line ("Too many components in index file entry");
         when Too_Many_Errors =>
            ScreenEcho.Put_Line ("Too many errors in a single file");
         when Warning_Name_Too_Long =>
            ScreenEcho.Put_Line ("Line too long in warning control file");
         when Unit_Name_In_Index_Too_Long =>
            ScreenEcho.Put_Line ("Unit name too long in index file");
         when File_Name_In_Index_Too_Long =>
            ScreenEcho.Put_Line ("File name too long in index file");
         when Too_Many_Suppressed_Warnings =>
            ScreenEcho.Put_Line ("Too many suppressed warnings for a single file");
         when Unit_Nesting_Too_Deep =>
            ScreenEcho.Put_Line ("Units too deeply nested");
         when Statement_Stack_Underflow =>
            ScreenEcho.Put_Line ("VCG statement stack underflow");
         when Statement_Stack_Overflow =>
            ScreenEcho.Put_Line ("VCG statement stack overflow");
         when Wf_Compilation_Unit_Stack_Overflow =>
            ScreenEcho.Put_Line ("Well-formation checker error: compilation unit stack overflow");
         when Wf_Compilation_Unit_Stack_Underflow =>
            ScreenEcho.Put_Line ("Internal error in well-formation checker: compilation unit stack underflow");
         when Too_Many_Flow_Analyser_Expressions =>
            ScreenEcho.Put_Line ("Too many expressions in flow analyser");
         when Too_Many_Params_In_Procedure_Call =>
            ScreenEcho.Put_Line ("Too many parameters in procedure call");
         when Statistics_Usage_Greater_Than_Table_Size =>
            ScreenEcho.Put_Line ("Reported table usage larger than table size");
         when Aggregate_Stack_Under_Flow =>
            ScreenEcho.Put_Line ("Aggregate stack underflow");
         when Aggregate_Stack_Over_Flow =>
            ScreenEcho.Put_Line ("Aggregate stack overflow");
         when Meta_File_Stack_Overflow =>
            ScreenEcho.Put_Line ("Stack overflow while processing meta file");
         when Lex_Stack_Overflow =>
            ScreenEcho.Put_Line ("Stack overflow in LexTokenStacks");
         when Lex_Stack_Underflow =>
            ScreenEcho.Put_Line ("Stack under flow in LexTokenStacks");
         when Component_Manager_Overflow =>
            ScreenEcho.Put_Line ("Record component manager overflow");
         when Component_Error_Overflow =>
            ScreenEcho.Put_Line ("Record component error-manager overflow");
         when Syntax_Tree_Walk_Error =>
            ScreenEcho.Put_Line ("Syntax tree walk error");
         when Precondition_Failure =>
            ScreenEcho.Put_Line ("Precondition failure");
         when Postcondition_Failure =>
            ScreenEcho.Put_Line ("Postcondition failure");
         when Assertion_Failure =>
            ScreenEcho.Put_Line ("Run-time assertion failure");
         when Unimplemented_Feature =>
            ScreenEcho.Put_Line ("Use of an unimplemented SPARK language construct or Examiner feature");
         when XML_Schema_Error =>
            ScreenEcho.Put_Line ("Error initialising schema");
         when XML_Generation_Error =>
            ScreenEcho.Put_Line ("Internal failure of the XML report generator");
         when Illegal_XML_Generation_Attempt =>
            ScreenEcho.Put_Line ("The Examiner attempted to generate invalid XML");
         when String_Over_Flow =>
            ScreenEcho.Put_Line ("String operation overflowed");
         when Queue_Overflow =>
            ScreenEcho.Put_Line ("Queue operation overflowed");
         when XRef_Table_Full =>
            ScreenEcho.Put_Line ("Cross-references table full");
         when Invalid_Index =>
            ScreenEcho.Put_Line ("Invalid index into container");
            -- Add additional errors here...
         when Other_Internal_Error =>
            ScreenEcho.Put_Line ("Other internal error");
      end case;
      if Msg /= "" then
         ScreenEcho.Put_String ("* ");
         ScreenEcho.Put_Line (Msg);
      end if;
   end Display_Box;

   procedure Fatal_Error (Sys_Err : in Sys_Err_Type;
                          Msg     : in String) is
      --# hide Fatal_Error;
      Error_Kind : Error_Kinds;
   begin
      Error_Kind := SETEK (Sys_Err);

      case Sys_Err is
         when VCG_Graph_Size_Exceeded | VCG_Heap_Is_Exhausted =>

            -- Following SEPR 2272, these are both caught and handled using
            -- semantic warning 409 in VCG.Generate_VCs_Local
            -- and no longer terminate the Examiner.
            -- Therefore, no need for a display box here unless -debug
            -- is active.
            if CommandLineData.Content.Debug.Enabled then
               Display_Box (Sys_Err, Msg);
               Display_Cause (Error_Kind);
            end if;

         when others =>
            Display_Box (Sys_Err, Msg);
            Display_Cause (Error_Kind);
      end case;

      Stop_Program (Error_Kind);
   end Fatal_Error;

   procedure RT_Assert (C       : in Boolean;
                        Sys_Err : in Sys_Err_Type;
                        Msg     : in String) is
      --# hide RT_Assert;
   begin
      if not C then
         Fatal_Error (Sys_Err, Msg);
      end if;
   end RT_Assert;

   procedure RT_Warning (C   : in Boolean;
                         Msg : in String) is
      --# hide RT_Warning;
   begin
      if not C then
         -- If would be great to put out a proper source file/positiom here,
         -- but that would need a circular inherit with LexTokenManager, so not
         -- possible.  We might also be in a position where this is no
         -- source position to report.
         --
         -- BUT..report "examiner.adb:1:1: " here to make sure that the GPS
         -- or GNATBench pick it up.
         ScreenEcho.Put_String ("examiner.adb:1:1: Internal warning. ");
         ScreenEcho.Put_String (Msg);
         ScreenEcho.Put_String (". Validity of analysis is not affected, but please report this ");
         ScreenEcho.Put_String ("matter via ");
         ScreenEcho.Put_Line (Version.Toolset_Support_Line2);
      end if;

   end RT_Warning;

end SystemErrors;