ada: Remove sa_messages

Spark and CodePeer do not depend on this unit anymore.

gcc/ada/

	* sa_messages.ads, sa_messages.adb: Remove files.

2 files changed, 0 insertions, 806 deletions

diff --git a/gcc/ada/sa_messages.adb b/gcc/ada/sa_messages.adb
deleted file mode 100644
index b9b4e93..0000000
--- a/gcc/ada/sa_messages.adb
+++ /dev/null
@@ -1,539 +0,0 @@
-------------------------------------------------------------------------------
---                       C O D E P E E R / S P A R K                        --
---                                                                          --
---                     Copyright (C) 2015-2022, AdaCore                     --
---                                                                          --
--- This is free software;  you can redistribute it  and/or modify it  under --
--- terms of the  GNU General Public License as published  by the Free Soft- --
--- ware  Foundation;  either version 3,  or (at your option) any later ver- --
--- sion.  This software is distributed in the hope  that it will be useful, --
--- but WITHOUT ANY WARRANTY;  without even the implied warranty of MERCHAN- --
--- TABILITY 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  this  software;   see  file --
--- COPYING3.  If not, go to http://www.gnu.org/licenses for a complete copy --
--- of the license.                                                          --
---                                                                          --
-------------------------------------------------------------------------------
-
-pragma Ada_2012;
-
-with Ada.Directories; use Ada.Directories;
-with Ada.Strings.Unbounded.Hash;
-
-with Ada.Text_IO;     use Ada.Text_IO;
-with GNATCOLL.JSON;   use GNATCOLL.JSON;
-
-package body SA_Messages is
-
-   -----------------------
-   -- Local subprograms --
-   -----------------------
-
-   function "<" (Left, Right : SA_Message) return Boolean is
-     (if Left.Kind /= Right.Kind then
-         Left.Kind < Right.Kind
-      else
-         Left.Kind in Check_Kind
-           and then Left.Check_Result < Right.Check_Result);
-
-   function "<" (Left, Right : Simple_Source_Location) return Boolean is
-      (if Left.File_Name /= Right.File_Name then
-          Left.File_Name < Right.File_Name
-       elsif Left.Line /= Right.Line then
-          Left.Line < Right.Line
-       else
-          Left.Column < Right.Column);
-
-   function "<" (Left, Right : Source_Locations) return Boolean is
-     (if Left'Length /= Right'Length then
-         Left'Length < Right'Length
-      elsif Left'Length = 0 then
-         False
-      elsif Left (Left'Last) /= Right (Right'Last) then
-         Left (Left'Last) < Right (Right'Last)
-      else
-         Left (Left'First .. Left'Last - 1) <
-           Right (Right'First .. Right'Last - 1));
-
-   function "<" (Left, Right : Source_Location) return Boolean is
-     (Left.Locations < Right.Locations);
-
-   function Base_Location
-     (Location : Source_Location) return Simple_Source_Location is
-     (Location.Locations (1));
-
-   function Hash (Key : SA_Message) return Hash_Type;
-   function Hash (Key : Source_Location) return Hash_Type;
-
-   ---------
-   -- "<" --
-   ---------
-
-   function "<" (Left, Right : Message_And_Location) return Boolean is
-     (if Left.Message = Right.Message
-      then Left.Location < Right.Location
-      else Left.Message < Right.Message);
-
-   ------------
-   -- Column --
-   ------------
-
-   function Column (Location : Source_Location) return Column_Number is
-     (Base_Location (Location).Column);
-
-   ---------------
-   -- File_Name --
-   ---------------
-
-   function File_Name (Location : Source_Location) return String is
-     (To_String (Base_Location (Location).File_Name));
-
-   function File_Name (Location : Source_Location) return Unbounded_String is
-     (Base_Location (Location).File_Name);
-
-   ------------------------
-   -- Enclosing_Instance --
-   ------------------------
-
-   function Enclosing_Instance
-     (Location : Source_Location) return Source_Location_Or_Null is
-     (Count     => Location.Count - 1,
-      Locations => Location.Locations (2 .. Location.Count));
-
-   ----------
-   -- Hash --
-   ----------
-
-   function Hash (Key : Message_And_Location) return Hash_Type is
-     (Hash (Key.Message) + Hash (Key.Location));
-
-   function Hash (Key : SA_Message) return Hash_Type is
-   begin
-      return Result : Hash_Type :=
-                        Hash_Type'Mod (Message_Kind'Pos (Key.Kind))
-      do
-         if Key.Kind in Check_Kind then
-            Result := Result +
-              Hash_Type'Mod (SA_Check_Result'Pos (Key.Check_Result));
-         end if;
-      end return;
-   end Hash;
-
-   function Hash (Key : Source_Location) return Hash_Type is
-   begin
-      return Result : Hash_Type := Hash_Type'Mod (Key.Count) do
-         for Loc of Key.Locations loop
-            Result := Result + Hash (Loc.File_Name);
-            Result := Result + Hash_Type'Mod (Loc.Line);
-            Result := Result + Hash_Type'Mod (Loc.Column);
-         end loop;
-      end return;
-   end Hash;
-
-   ---------------
-   -- Iteration --
-   ---------------
-
-   function Iteration (Location : Source_Location) return Iteration_Id is
-     (Base_Location (Location).Iteration);
-
-   ----------
-   -- Line --
-   ----------
-
-   function Line (Location : Source_Location) return Line_Number is
-     (Base_Location (Location).Line);
-
-   --------------
-   -- Location --
-   --------------
-
-   function Location
-     (Item : Message_And_Location) return Source_Location is
-     (Item.Location);
-
-   ----------
-   -- Make --
-   ----------
-
-   function Make
-     (File_Name          : String;
-      Line               : Line_Number;
-      Column             : Column_Number;
-      Iteration          : Iteration_Id;
-      Enclosing_Instance : Source_Location_Or_Null) return Source_Location
-   is
-   begin
-      return Result : Source_Location
-                        (Count => Enclosing_Instance.Count + 1)
-      do
-         Result.Locations (1) :=
-           (File_Name => To_Unbounded_String (File_Name),
-            Line      => Line,
-            Column    => Column,
-            Iteration => Iteration);
-
-         Result.Locations (2 .. Result.Count) := Enclosing_Instance.Locations;
-      end return;
-   end Make;
-
-   ------------------
-   -- Make_Msg_Loc --
-   ------------------
-
-   function Make_Msg_Loc
-     (Msg : SA_Message;
-      Loc : Source_Location) return Message_And_Location
-   is
-   begin
-      return Message_And_Location'(Count    => Loc.Count,
-                                   Message  => Msg,
-                                   Location => Loc);
-   end Make_Msg_Loc;
-
-   -------------
-   -- Message --
-   -------------
-
-   function Message (Item : Message_And_Location) return SA_Message is
-     (Item.Message);
-
-   package Field_Names is
-
-      --  A Source_Location value is represented in JSON as a two or three
-      --  field value having fields Message_Kind (a string) and Locations (an
-      --  array); if the Message_Kind indicates a check kind, then a third
-      --  field is present: Check_Result (a string). The element type of the
-      --  Locations array is a value having at least 4 fields:
-      --  File_Name (a string), Line (an integer), Column (an integer),
-      --  and Iteration_Kind (an integer); if the Iteration_Kind field
-      --  has the value corresponding to the enumeration literal Numbered,
-      --  then two additional integer fields are present, Iteration_Number
-      --  and Iteration_Of_Total.
-
-      Check_Result       : constant String := "Check_Result";
-      Column             : constant String := "Column";
-      File_Name          : constant String := "File_Name";
-      Iteration_Kind     : constant String := "Iteration_Kind";
-      Iteration_Number   : constant String := "Iteration_Number";
-      Iteration_Of_Total : constant String := "Iteration_Total";
-      Line               : constant String := "Line";
-      Locations          : constant String := "Locations";
-      Message_Kind       : constant String := "Message_Kind";
-      Messages           : constant String := "Messages";
-   end Field_Names;
-
-   package body Writing is
-      File : File_Type;
-      --  The file to which output will be written (in Close, not in Write)
-
-      Messages : JSON_Array;
-      --  Successive calls to Write append messages to this list
-
-      -----------------------
-      -- Local subprograms --
-      -----------------------
-
-      function To_JSON_Array
-        (Locations : Source_Locations) return JSON_Array;
-      --  Represent a Source_Locations array as a JSON_Array
-
-      function To_JSON_Value
-        (Location : Simple_Source_Location) return JSON_Value;
-      --  Represent a Simple_Source_Location as a JSON_Value
-
-      -----------
-      -- Close --
-      -----------
-
-      procedure Close is
-         Value : constant JSON_Value := Create_Object;
-
-      begin
-         --  only one field for now
-         Set_Field (Value, Field_Names.Messages, Messages);
-         Put_Line (File, Write (Item => Value, Compact => False));
-         Clear (Messages);
-         Close (File => File);
-      end Close;
-
-      -------------
-      -- Is_Open --
-      -------------
-
-      function Is_Open return Boolean is (Is_Open (File));
-
-      ----------
-      -- Open --
-      ----------
-
-      procedure Open (File_Name : String) is
-      begin
-         Create (File => File, Mode => Out_File, Name => File_Name);
-         Clear (Messages);
-      end Open;
-
-      -------------------
-      -- To_JSON_Array --
-      -------------------
-
-      function To_JSON_Array
-        (Locations : Source_Locations) return JSON_Array
-      is
-      begin
-         return Result : JSON_Array := Empty_Array do
-            for Location of Locations loop
-               Append (Result, To_JSON_Value (Location));
-            end loop;
-         end return;
-      end To_JSON_Array;
-
-      -------------------
-      -- To_JSON_Value --
-      -------------------
-
-      function To_JSON_Value
-        (Location : Simple_Source_Location) return JSON_Value
-      is
-      begin
-         return Result : constant JSON_Value := Create_Object do
-            Set_Field (Result, Field_Names.File_Name, Location.File_Name);
-            Set_Field (Result, Field_Names.Line, Integer (Location.Line));
-            Set_Field (Result, Field_Names.Column, Integer (Location.Column));
-            Set_Field (Result, Field_Names.Iteration_Kind, Integer'(
-                       Iteration_Kind'Pos (Location.Iteration.Kind)));
-
-            if Location.Iteration.Kind = Numbered then
-               Set_Field (Result, Field_Names.Iteration_Number,
-                          Location.Iteration.Number);
-               Set_Field (Result, Field_Names.Iteration_Of_Total,
-                          Location.Iteration.Of_Total);
-            end if;
-         end return;
-      end To_JSON_Value;
-
-      -----------
-      -- Write --
-      -----------
-
-      procedure Write (Message : SA_Message; Location : Source_Location) is
-         Value : constant JSON_Value := Create_Object;
-
-      begin
-         Set_Field (Value, Field_Names.Message_Kind, Message.Kind'Img);
-
-         if Message.Kind in Check_Kind then
-            Set_Field
-              (Value, Field_Names.Check_Result, Message.Check_Result'Img);
-         end if;
-
-         Set_Field
-           (Value, Field_Names.Locations, To_JSON_Array (Location.Locations));
-         Append (Messages, Value);
-      end Write;
-   end Writing;
-
-   package body Reading is
-      File       : File_Type;
-      --  The file from which messages are read (in Open, not in Read)
-
-      Messages   : JSON_Array;
-      --  The list of messages that were read in from File
-
-      Next_Index : Positive;
-      --  The index of the message in Messages which will be returned by the
-      --  next call to Get.
-
-      Parse_Full_Path : Boolean := True;
-      --  if the full path or only the base name of the file should be parsed
-
-      -----------
-      -- Close --
-      -----------
-
-      procedure Close is
-      begin
-         Clear (Messages);
-         Close (File);
-      end Close;
-
-      ----------
-      -- Done --
-      ----------
-
-      function Done return Boolean is (Next_Index > Length (Messages));
-
-      ---------
-      -- Get --
-      ---------
-
-      function Get return Message_And_Location is
-         Value : constant JSON_Value := Get (Messages, Next_Index);
-
-         function Get_Message (Kind :  Message_Kind) return SA_Message;
-         --  Return SA_Message of given kind, filling in any non-discriminant
-         --  by reading from Value.
-
-         function Make
-           (Location : Source_Location;
-            Message  : SA_Message) return Message_And_Location;
-         --  Constructor
-
-         function To_Location
-           (Encoded   : JSON_Array;
-            Full_Path : Boolean) return Source_Location;
-         --  Decode a Source_Location from JSON_Array representation
-
-         function To_Simple_Location
-           (Encoded   : JSON_Value;
-            Full_Path : Boolean) return Simple_Source_Location;
-         --  Decode a Simple_Source_Location from JSON_Value representation
-
-         -----------------
-         -- Get_Message --
-         -----------------
-
-         function Get_Message (Kind :  Message_Kind) return SA_Message is
-         begin
-            --  If we had AI12-0086, then we could use aggregates here (which
-            --  would be better than field-by-field assignment for the usual
-            --  maintainability reasons). But we don't, so we won't.
-
-            return Result : SA_Message (Kind => Kind) do
-               if Kind in Check_Kind then
-                  Result.Check_Result :=
-                    SA_Check_Result'Value
-                      (Get (Value, Field_Names.Check_Result));
-               end if;
-            end return;
-         end Get_Message;
-
-         ----------
-         -- Make --
-         ----------
-
-         function Make
-           (Location : Source_Location;
-            Message  : SA_Message) return Message_And_Location
-         is
-           (Count => Location.Count, Message => Message, Location => Location);
-
-         -----------------
-         -- To_Location --
-         -----------------
-
-         function To_Location
-           (Encoded   : JSON_Array;
-            Full_Path : Boolean) return Source_Location is
-         begin
-            return Result : Source_Location (Count => Length (Encoded)) do
-               for I in Result.Locations'Range loop
-                  Result.Locations (I) :=
-                    To_Simple_Location (Get (Encoded, I), Full_Path);
-               end loop;
-            end return;
-         end To_Location;
-
-         ------------------------
-         -- To_Simple_Location --
-         ------------------------
-
-         function To_Simple_Location
-           (Encoded   : JSON_Value;
-            Full_Path : Boolean) return Simple_Source_Location
-         is
-            function Get_Iteration_Id
-              (Kind : Iteration_Kind) return Iteration_Id;
-            --  Given the discriminant for an Iteration_Id value, return the
-            --  entire value.
-
-            ----------------------
-            -- Get_Iteration_Id --
-            ----------------------
-
-            function Get_Iteration_Id (Kind : Iteration_Kind)
-              return Iteration_Id
-            is
-            begin
-               --  Initialize non-discriminant fields, if any
-
-               return Result : Iteration_Id (Kind => Kind) do
-                  if Kind = Numbered then
-                     Result :=
-                       (Kind     => Numbered,
-                        Number   =>
-                          Get (Encoded, Field_Names.Iteration_Number),
-                        Of_Total =>
-                          Get (Encoded, Field_Names.Iteration_Of_Total));
-                  end if;
-               end return;
-            end Get_Iteration_Id;
-
-            --  Local variables
-
-            FN : constant Unbounded_String :=
-                   Get (Encoded, Field_Names.File_Name);
-
-         --  Start of processing for To_Simple_Location
-
-         begin
-            return
-              (File_Name =>
-                 (if Full_Path then
-                     FN
-                  else
-                     To_Unbounded_String (Simple_Name (To_String (FN)))),
-               Line      =>
-                 Line_Number (Integer'(Get (Encoded, Field_Names.Line))),
-               Column    =>
-                 Column_Number (Integer'(Get (Encoded, Field_Names.Column))),
-               Iteration =>
-                 Get_Iteration_Id
-                   (Kind => Iteration_Kind'Val (Integer'(Get
-                              (Encoded, Field_Names.Iteration_Kind)))));
-         end To_Simple_Location;
-
-      --  Start of processing for Get
-
-      begin
-         Next_Index := Next_Index + 1;
-
-         return Make
-           (Message  =>
-              Get_Message
-                (Message_Kind'Value (Get (Value, Field_Names.Message_Kind))),
-            Location =>
-              To_Location
-                (Get (Value, Field_Names.Locations), Parse_Full_Path));
-      end Get;
-
-      -------------
-      -- Is_Open --
-      -------------
-
-      function Is_Open return Boolean is (Is_Open (File));
-
-      ----------
-      -- Open --
-      ----------
-
-      procedure Open (File_Name : String; Full_Path : Boolean := True) is
-         File_Text : Unbounded_String := Null_Unbounded_String;
-
-      begin
-         Parse_Full_Path := Full_Path;
-         Open (File => File, Mode => In_File, Name => File_Name);
-
-         --  File read here, not in Get, but that's an implementation detail
-
-         while not End_Of_File (File) loop
-            Append (File_Text, Get_Line (File));
-         end loop;
-
-         Messages   := Get (Read (File_Text), Field_Names.Messages);
-         Next_Index := 1;
-      end Open;
-   end Reading;
-
-end SA_Messages;
diff --git a/gcc/ada/sa_messages.ads b/gcc/ada/sa_messages.ads
deleted file mode 100644
index c448397..0000000
--- a/gcc/ada/sa_messages.ads
+++ /dev/null
@@ -1,267 +0,0 @@
-------------------------------------------------------------------------------
---                       C O D E P E E R / S P A R K                        --
---                                                                          --
---                     Copyright (C) 2015-2022, AdaCore                     --
---                                                                          --
--- This is free software;  you can redistribute it  and/or modify it  under --
--- terms of the  GNU General Public License as published  by the Free Soft- --
--- ware  Foundation;  either version 3,  or (at your option) any later ver- --
--- sion.  This software is distributed in the hope  that it will be useful, --
--- but WITHOUT ANY WARRANTY;  without even the implied warranty of MERCHAN- --
--- TABILITY 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  this  software;   see  file --
--- COPYING3.  If not, go to http://www.gnu.org/licenses for a complete copy --
--- of the license.                                                          --
---                                                                          --
-------------------------------------------------------------------------------
-
-pragma Ada_2012;
-
-with Ada.Containers;        use Ada.Containers;
-with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;
-
-package SA_Messages is
-
-   --  This package can be used for reading/writing a file containing a
-   --  sequence of static anaysis results. Each element can describe a runtime
-   --  check whose outcome has been statically determined, or it might be a
-   --  warning or diagnostic message. It is expected that typically CodePeer
-   --  will do the writing and SPARK will do the reading; this will allow SPARK
-   --  to get the benefit of CodePeer's analysis.
-   --
-   --  Each item is represented as a pair consisting of a message and an
-   --  associated source location. Source locations may refer to a location
-   --  within the expansion of an instance of a generic; this is represented
-   --  by combining the corresponding location within the generic with the
-   --  location of the instance (repeated if the instance itself occurs within
-   --  a generic). In addition, the type Iteration_Id is intended for use in
-   --  distinguishing messages which refer to a specific iteration of a loop
-   --  (this case can arise, for example, if CodePeer chooses to unroll a
-   --  for-loop). This data structure is only general enough to support the
-   --  kinds of unrolling that are currently planned for CodePeer. For
-   --  example, an Iteration_Id can only identify an iteration of the nearest
-   --  enclosing loop of the associated File/Line/Column source location.
-   --  This is not a problem because CodePeer doesn't unroll loops which
-   --  contain other loops.
-
-   type Message_Kind is (
-
-      --  Check kinds
-
-      Array_Index_Check,
-      Divide_By_Zero_Check,
-      Tag_Check,
-      Discriminant_Check,
-      Range_Check,
-      Overflow_Check,
-      Assertion_Check,
-
-      --  Warning kinds
-
-      Suspicious_Range_Precondition_Warning,
-      Suspicious_First_Precondition_Warning,
-      Suspicious_Input_Warning,
-      Suspicious_Constant_Operation_Warning,
-      Unread_In_Out_Parameter_Warning,
-      Unassigned_In_Out_Parameter_Warning,
-      Non_Analyzed_Call_Warning,
-      Procedure_Does_Not_Return_Warning,
-      Check_Fails_On_Every_Call_Warning,
-      Unknown_Call_Warning,
-      Dead_Store_Warning,
-      Dead_Outparam_Store_Warning,
-      Potentially_Dead_Store_Warning,
-      Same_Value_Dead_Store_Warning,
-      Dead_Block_Warning,
-      Infinite_Loop_Warning,
-      Dead_Edge_Warning,
-      Plain_Dead_Edge_Warning,
-      True_Dead_Edge_Warning,
-      False_Dead_Edge_Warning,
-      True_Condition_Dead_Edge_Warning,
-      False_Condition_Dead_Edge_Warning,
-      Unrepeatable_While_Loop_Warning,
-      Dead_Block_Continuation_Warning,
-      Local_Lock_Of_Global_Object_Warning,
-      Analyzed_Module_Warning,
-      Non_Analyzed_Module_Warning,
-      Non_Analyzed_Procedure_Warning,
-      Incompletely_Analyzed_Procedure_Warning);
-
-   --  Assertion_Check includes checks for user-defined PPCs (both specific
-   --  and class-wide), Assert pragma checks, subtype predicate checks,
-   --  type invariant checks (specific and class-wide), and checks for
-   --  implementation-defined assertions such as Assert_And_Cut, Assume,
-   --  Contract_Cases, Default_Initial_Condition, Initial_Condition,
-   --  Loop_Invariant, Loop_Variant, Refined_Post, and Subprogram_Variant.
-   --
-   --  It might be nice to distinguish these different kinds of assertions
-   --  as is done in SPARK's VC_Kind enumeration type, but any distinction
-   --  which isn't already present in CP's BE_Message_Subkind enumeration type
-   --  would require more work on the CP side.
-   --
-   --  The warning kinds are pretty much a copy of the set of
-   --  Be_Message_Subkind values for which CP's Is_Warning predicate returns
-   --  True; see descriptive comment for each in CP's message_kinds.ads .
-
-   subtype Check_Kind is Message_Kind
-     range Array_Index_Check .. Assertion_Check;
-   subtype Warning_Kind is Message_Kind
-     range Message_Kind'Succ (Check_Kind'Last) .. Message_Kind'Last;
-
-   --  Possible outcomes of the static analysis of a runtime check
-   --
-   --  Not_Statically_Known_With_Low_Severity could be used instead of of
-   --  Not_Statically_Known if there is some reason to believe that (although
-   --  the tool couldn't prove it) the check is likely to always pass (in CP
-   --  terms, if the corresponding CP message has severity Low as opposed to
-   --  Medium). It's not clear yet whether SPARK will care about this
-   --  distinction.
-
-   type SA_Check_Result is
-     (Statically_Known_Success,
-      Not_Statically_Known_With_Low_Severity,
-      Not_Statically_Known,
-      Statically_Known_Failure);
-
-   type SA_Message (Kind : Message_Kind := Message_Kind'Last) is record
-      case Kind is
-         when Check_Kind =>
-            Check_Result : SA_Check_Result;
-
-         when Warning_Kind =>
-            null;
-      end case;
-   end record;
-
-   type Source_Location_Or_Null (<>) is private;
-   Null_Location : constant Source_Location_Or_Null;
-   subtype Source_Location is Source_Location_Or_Null with
-     Dynamic_Predicate => Source_Location /= Null_Location;
-
-   type Line_Number is new Positive;
-   type Column_Number is new Positive;
-
-   function File_Name (Location : Source_Location) return String;
-   function File_Name (Location : Source_Location) return Unbounded_String;
-   function Line      (Location : Source_Location) return Line_Number;
-   function Column    (Location : Source_Location) return Column_Number;
-
-   type Iteration_Kind is (None, Initial, Subsequent, Numbered);
-   --  None is for the usual no-unrolling case.
-   --  Initial and Subsequent are for use in the case where only the first
-   --  iteration of a loop (or some part thereof, such as the termination
-   --  test of a while-loop) is unrolled.
-   --  Numbered is for use in the case where a for-loop with a statically
-   --  known number of iterations is fully unrolled.
-
-   subtype Iteration_Number is Integer range 1 .. 255;
-   subtype Iteration_Total  is Integer range 2 .. 255;
-
-   type Iteration_Id (Kind : Iteration_Kind := None) is record
-      case Kind is
-         when Numbered =>
-            Number   : Iteration_Number;
-            Of_Total : Iteration_Total;
-         when others =>
-            null;
-      end case;
-   end record;
-
-   function Iteration (Location : Source_Location) return Iteration_Id;
-
-   function Enclosing_Instance
-     (Location : Source_Location) return Source_Location_Or_Null;
-   --  For a source location occurring within the expansion of an instance of a
-   --  generic unit, the Line, Column, and File_Name selectors will indicate a
-   --  location within the generic; the Enclosing_Instance selector yields the
-   --  location of the declaration of the instance.
-
-   function Make
-     (File_Name : String;
-      Line      : Line_Number;
-      Column    : Column_Number;
-      Iteration : Iteration_Id;
-      Enclosing_Instance : Source_Location_Or_Null) return Source_Location;
-   --  Constructor
-
-   type Message_And_Location (<>) is private;
-
-   function Location (Item : Message_And_Location) return Source_Location;
-   function Message (Item : Message_And_Location) return SA_Message;
-
-   function Make_Msg_Loc
-     (Msg : SA_Message;
-      Loc : Source_Location) return Message_And_Location;
-   --  Selectors
-
-   function "<" (Left, Right : Message_And_Location) return Boolean;
-   function Hash (Key : Message_And_Location) return Hash_Type;
-   --  Actuals for container instances
-
-   File_Extension : constant String; -- ".json" (but could change in future)
-   --  Clients may wish to use File_Extension in constructing
-   --  File_Name parameters for calls to Open.
-
-   package Writing is
-      function Is_Open return Boolean;
-
-      procedure Open (File_Name : String) with
-        Precondition  => not Is_Open,
-        Postcondition => Is_Open;
-      --  Behaves like Text_IO.Create with respect to error cases
-
-      procedure Write (Message : SA_Message; Location : Source_Location);
-
-      procedure Close with
-        Precondition  => Is_Open,
-        Postcondition => not Is_Open;
-      --  Behaves like Text_IO.Close with respect to error cases
-   end Writing;
-
-   package Reading is
-      function Is_Open return Boolean;
-
-      procedure Open (File_Name : String; Full_Path : Boolean := True) with
-        Precondition  => not Is_Open,
-        Postcondition => Is_Open;
-      --  Behaves like Text_IO.Open with respect to error cases
-
-      function Done return Boolean with
-        Precondition => Is_Open;
-
-      function Get return Message_And_Location with
-        Precondition => not Done;
-
-      procedure Close with
-        Precondition  => Is_Open,
-        Postcondition => not Is_Open;
-      --  Behaves like Text_IO.Close with respect to error cases
-   end Reading;
-
-private
-   type Simple_Source_Location is record
-      File_Name : Unbounded_String := Null_Unbounded_String;
-      Line      : Line_Number      := Line_Number'Last;
-      Column    : Column_Number    := Column_Number'Last;
-      Iteration : Iteration_Id     := (Kind => None);
-   end record;
-
-   type Source_Locations is
-     array (Natural range <>) of Simple_Source_Location;
-
-   type Source_Location_Or_Null (Count : Natural) is record
-      Locations : Source_Locations (1 .. Count);
-   end record;
-
-   Null_Location : constant Source_Location_Or_Null :=
-                     (Count => 0, Locations => (others => <>));
-
-   type Message_And_Location (Count : Positive) is record
-      Message  : SA_Message;
-      Location : Source_Location (Count => Count);
-   end record;
-
-   File_Extension : constant String := ".json";
-end SA_Messages;