From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wr1-x436.google.com (mail-wr1-x436.google.com [IPv6:2a00:1450:4864:20::436]) by sourceware.org (Postfix) with ESMTPS id 436953858291 for ; Fri, 4 Nov 2022 13:57:00 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 436953858291 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com Received: by mail-wr1-x436.google.com with SMTP id o4so7181642wrq.6 for ; Fri, 04 Nov 2022 06:57:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=3yIblqAJsXzBDQTawuDCAGDyfvTvT4r0WO7C+zDsL40=; b=HgBmvDF10NrQP8FFp85umIKzc/aBQsXxzoaRb5h2GottscJyu31aaA19eRnG+brG6d 1rIVekbdtoG433lnqMOD7CSCMXNOupe4BupV26yX3tZpaftzJGbivKSktt80abx/aKg/ gwpQd8lUU907D0ackT5lFTGOUPG+fxTHV//L54scO5tZcmqUsPxqs1I9A4YGAZMZ3Krw tQqb5tvCi1A9DJqhTKyhGH3jIlcuM62cHFHdAlYqBiSrXFLxg3cPmt9wBUVpyJyF7Mkw zGgA+T2VBPtpChnWOWc/U1C3osO8scCDRKaoYujeAay7MC0oXF82iEOF+PO+do8dRV73 b2Ag== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=3yIblqAJsXzBDQTawuDCAGDyfvTvT4r0WO7C+zDsL40=; b=uiGEo0TjKy2ecktbfZgGUlNiR0ng8Do3d92QaD+2O3rK4HGfuKAeE+MEcz28EUiCvN iogjeXCXYmtpXeaCPQMuRx3dLejTxJgRNjgDcQWS0CXg0u0TRUOcLSalrSdfZ/i33ihQ 8n5LoHhGvz/KSMwp2rjSKp/P0Fw+DKFQDtwqTe9Jpeh7qq0EB5oLPsAtZSUsYNx4JECf V+aQB74tqKpZQfWrgENPc6V5jcZAbdF3zf6csMInwWcHI/zKilrILPNaH6UJdxIcic4o ph3LBuXvdJhiszXJAmjjGv2PITKtKJ3bfj7gTv2zmn7C56YO0Ye+IXcHab7RXY37H82P 5UPw== X-Gm-Message-State: ACrzQf3vWmdoWvFFK3k12CzO1PPLjOtpTrOk44AIhhNO2G+NvGpNFyW4 6LFIZaPz5pkMZfLSk4hHXyXAekr3C17pUA== X-Google-Smtp-Source: AMsMyM4TkfpOL4gQkj7nh5LhSx+uFiOGTnv9ZD8v0ePxCGmfMmdFQKEl3O7UC4JniNcX+aBT8bxOiQ== X-Received: by 2002:adf:f411:0:b0:234:f58a:d5f6 with SMTP id g17-20020adff411000000b00234f58ad5f6mr22402033wro.304.1667570218860; Fri, 04 Nov 2022 06:56:58 -0700 (PDT) Received: from localhost.localdomain (static-176-191-105-132.ftth.abo.bbox.fr. [176.191.105.132]) by smtp.gmail.com with ESMTPSA id b21-20020a05600c06d500b003b95ed78275sm2776220wmn.20.2022.11.04.06.56.58 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 04 Nov 2022 06:56:58 -0700 (PDT) From: =?UTF-8?q?Marc=20Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Ghjuvan Lacambre Subject: [COMMITTED] ada: Remove sa_messages Date: Fri, 4 Nov 2022 14:56:54 +0100 Message-Id: <20221104135654.86140-1-poulhies@adacore.com> X-Mailer: git-send-email 2.34.1 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Status: No, score=-12.8 required=5.0 tests=BAYES_00,DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,GIT_PATCH_0,KAM_ASCII_DIVIDERS,KAM_SHORT,RCVD_IN_DNSWL_NONE,SPF_HELO_NONE,SPF_PASS,TXREP autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org List-Id: From: Ghjuvan Lacambre 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