--- /dev/null
+------------------------------------------------------------------------------
+-- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- 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;
projects / gcc.git / commitdiff