------------------------------------------------------------------------------ -- 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;