[Ada] Add sa_messages.ad[sb] for SPARK 2014

These new source files will make it possible to build SPARK 2014 from
a snapshot of GCC FSF sources.

2018-08-21  Pierre-Marie de Rodat  <derodat@adacore.com>

gcc/ada/

	* sa_messages.ads, sa_messages.adb: New source files.

From-SVN: r263706

gcc/ada/ChangeLog

+2018-08-21  Pierre-Marie de Rodat  <derodat@adacore.com>
+
+	* sa_messages.ads, sa_messages.adb: New source files.
+
 2018-08-03  Pierre-Marie de Rodat  <derodat@adacore.com>
 
 	Reverts

gcc/ada/sa_messages.adb

+------------------------------------------------------------------------------
+--                       C O D E P E E R / S P A R K                        --
+--                                                                          --
+--                     Copyright (C) 2015-2018, 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;

gcc/ada/sa_messages.ads

+------------------------------------------------------------------------------
+--                       C O D E P E E R / S P A R K                        --
+--                                                                          --
+--                     Copyright (C) 2015-2018, 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, and Refined_Post.
+   --
+   --  TBD: 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;