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