* [COMMITTED] ada: Remove sa_messages
@ 2022-11-04 13:56 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2022-11-04 13:56 UTC (permalink / raw)
To: gcc-patches; +Cc: Ghjuvan Lacambre
From: Ghjuvan Lacambre <lacambre@adacore.com>
Spark and CodePeer do not depend on this unit anymore.
gcc/ada/
* sa_messages.ads, sa_messages.adb: Remove files.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/sa_messages.adb | 539 ----------------------------------------
gcc/ada/sa_messages.ads | 267 --------------------
2 files changed, 806 deletions(-)
delete mode 100644 gcc/ada/sa_messages.adb
delete mode 100644 gcc/ada/sa_messages.ads
diff --git a/gcc/ada/sa_messages.adb b/gcc/ada/sa_messages.adb
deleted file mode 100644
index b9b4e932b43..00000000000
--- 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 c4483974984..00000000000
--- 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;
--
2.34.1
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-11-04 13:57 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-11-04 13:56 [COMMITTED] ada: Remove sa_messages Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).