From: Pierre-Marie de Rodat Date: Tue, 21 Aug 2018 14:44:25 +0000 (+0000) Subject: [Ada] Add sa_messages.ad[sb] for SPARK 2014 X-Git-Tag: basepoints/gcc-10~4654 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=d40800cfe589cf55e074ed151c7a607d5680997a;p=thirdparty%2Fgcc.git [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 gcc/ada/ * sa_messages.ads, sa_messages.adb: New source files. From-SVN: r263706 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 792811fb989c..9bbcc9d8f96f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,7 @@ +2018-08-21 Pierre-Marie de Rodat + + * sa_messages.ads, sa_messages.adb: New source files. + 2018-08-03 Pierre-Marie de Rodat Reverts diff --git a/gcc/ada/sa_messages.adb b/gcc/ada/sa_messages.adb new file mode 100644 index 000000000000..30ae48c0f719 --- /dev/null +++ b/gcc/ada/sa_messages.adb @@ -0,0 +1,539 @@ +------------------------------------------------------------------------------ +-- 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; diff --git a/gcc/ada/sa_messages.ads b/gcc/ada/sa_messages.ads new file mode 100644 index 000000000000..93226a7e7e37 --- /dev/null +++ b/gcc/ada/sa_messages.ads @@ -0,0 +1,267 @@ +------------------------------------------------------------------------------ +-- 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;