1------------------------------------------------------------------------------ 2-- C O D E P E E R / S P A R K -- 3-- -- 4-- Copyright (C) 2015-2019, AdaCore -- 5-- -- 6-- This is free software; you can redistribute it and/or modify it under -- 7-- terms of the GNU General Public License as published by the Free Soft- -- 8-- ware Foundation; either version 3, or (at your option) any later ver- -- 9-- sion. This software is distributed in the hope that it will be useful, -- 10-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN- -- 11-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -- 12-- License for more details. You should have received a copy of the GNU -- 13-- General Public License distributed with this software; see file -- 14-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy -- 15-- of the license. -- 16-- -- 17------------------------------------------------------------------------------ 18 19pragma Ada_2012; 20 21with Ada.Containers; use Ada.Containers; 22with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; 23 24package SA_Messages is 25 26 -- This package can be used for reading/writing a file containing a 27 -- sequence of static anaysis results. Each element can describe a runtime 28 -- check whose outcome has been statically determined, or it might be a 29 -- warning or diagnostic message. It is expected that typically CodePeer 30 -- will do the writing and SPARK will do the reading; this will allow SPARK 31 -- to get the benefit of CodePeer's analysis. 32 -- 33 -- Each item is represented as a pair consisting of a message and an 34 -- associated source location. Source locations may refer to a location 35 -- within the expansion of an instance of a generic; this is represented 36 -- by combining the corresponding location within the generic with the 37 -- location of the instance (repeated if the instance itself occurs within 38 -- a generic). In addition, the type Iteration_Id is intended for use in 39 -- distinguishing messages which refer to a specific iteration of a loop 40 -- (this case can arise, for example, if CodePeer chooses to unroll a 41 -- for-loop). This data structure is only general enough to support the 42 -- kinds of unrolling that are currently planned for CodePeer. For 43 -- example, an Iteration_Id can only identify an iteration of the nearest 44 -- enclosing loop of the associated File/Line/Column source location. 45 -- This is not a problem because CodePeer doesn't unroll loops which 46 -- contain other loops. 47 48 type Message_Kind is ( 49 50 -- Check kinds 51 52 Array_Index_Check, 53 Divide_By_Zero_Check, 54 Tag_Check, 55 Discriminant_Check, 56 Range_Check, 57 Overflow_Check, 58 Assertion_Check, 59 60 -- Warning kinds 61 62 Suspicious_Range_Precondition_Warning, 63 Suspicious_First_Precondition_Warning, 64 Suspicious_Input_Warning, 65 Suspicious_Constant_Operation_Warning, 66 Unread_In_Out_Parameter_Warning, 67 Unassigned_In_Out_Parameter_Warning, 68 Non_Analyzed_Call_Warning, 69 Procedure_Does_Not_Return_Warning, 70 Check_Fails_On_Every_Call_Warning, 71 Unknown_Call_Warning, 72 Dead_Store_Warning, 73 Dead_Outparam_Store_Warning, 74 Potentially_Dead_Store_Warning, 75 Same_Value_Dead_Store_Warning, 76 Dead_Block_Warning, 77 Infinite_Loop_Warning, 78 Dead_Edge_Warning, 79 Plain_Dead_Edge_Warning, 80 True_Dead_Edge_Warning, 81 False_Dead_Edge_Warning, 82 True_Condition_Dead_Edge_Warning, 83 False_Condition_Dead_Edge_Warning, 84 Unrepeatable_While_Loop_Warning, 85 Dead_Block_Continuation_Warning, 86 Local_Lock_Of_Global_Object_Warning, 87 Analyzed_Module_Warning, 88 Non_Analyzed_Module_Warning, 89 Non_Analyzed_Procedure_Warning, 90 Incompletely_Analyzed_Procedure_Warning); 91 92 -- Assertion_Check includes checks for user-defined PPCs (both specific 93 -- and class-wide), Assert pragma checks, subtype predicate checks, 94 -- type invariant checks (specific and class-wide), and checks for 95 -- implementation-defined assertions such as Assert_And_Cut, Assume, 96 -- Contract_Cases, Default_Initial_Condition, Initial_Condition, 97 -- Loop_Invariant, Loop_Variant, and Refined_Post. 98 -- 99 -- TBD: it might be nice to distinguish these different kinds of assertions 100 -- as is done in SPARK's VC_Kind enumeration type, but any distinction 101 -- which isn't already present in CP's BE_Message_Subkind enumeration type 102 -- would require more work on the CP side. 103 -- 104 -- The warning kinds are pretty much a copy of the set of 105 -- Be_Message_Subkind values for which CP's Is_Warning predicate returns 106 -- True; see descriptive comment for each in CP's message_kinds.ads . 107 108 subtype Check_Kind is Message_Kind 109 range Array_Index_Check .. Assertion_Check; 110 subtype Warning_Kind is Message_Kind 111 range Message_Kind'Succ (Check_Kind'Last) .. Message_Kind'Last; 112 113 -- Possible outcomes of the static analysis of a runtime check 114 -- 115 -- Not_Statically_Known_With_Low_Severity could be used instead of of 116 -- Not_Statically_Known if there is some reason to believe that (although 117 -- the tool couldn't prove it) the check is likely to always pass (in CP 118 -- terms, if the corresponding CP message has severity Low as opposed to 119 -- Medium). It's not clear yet whether SPARK will care about this 120 -- distinction. 121 122 type SA_Check_Result is 123 (Statically_Known_Success, 124 Not_Statically_Known_With_Low_Severity, 125 Not_Statically_Known, 126 Statically_Known_Failure); 127 128 type SA_Message (Kind : Message_Kind := Message_Kind'Last) is record 129 case Kind is 130 when Check_Kind => 131 Check_Result : SA_Check_Result; 132 133 when Warning_Kind => 134 null; 135 end case; 136 end record; 137 138 type Source_Location_Or_Null (<>) is private; 139 Null_Location : constant Source_Location_Or_Null; 140 subtype Source_Location is Source_Location_Or_Null with 141 Dynamic_Predicate => Source_Location /= Null_Location; 142 143 type Line_Number is new Positive; 144 type Column_Number is new Positive; 145 146 function File_Name (Location : Source_Location) return String; 147 function File_Name (Location : Source_Location) return Unbounded_String; 148 function Line (Location : Source_Location) return Line_Number; 149 function Column (Location : Source_Location) return Column_Number; 150 151 type Iteration_Kind is (None, Initial, Subsequent, Numbered); 152 -- None is for the usual no-unrolling case. 153 -- Initial and Subsequent are for use in the case where only the first 154 -- iteration of a loop (or some part thereof, such as the termination 155 -- test of a while-loop) is unrolled. 156 -- Numbered is for use in the case where a for-loop with a statically 157 -- known number of iterations is fully unrolled. 158 159 subtype Iteration_Number is Integer range 1 .. 255; 160 subtype Iteration_Total is Integer range 2 .. 255; 161 162 type Iteration_Id (Kind : Iteration_Kind := None) is record 163 case Kind is 164 when Numbered => 165 Number : Iteration_Number; 166 Of_Total : Iteration_Total; 167 when others => 168 null; 169 end case; 170 end record; 171 172 function Iteration (Location : Source_Location) return Iteration_Id; 173 174 function Enclosing_Instance 175 (Location : Source_Location) return Source_Location_Or_Null; 176 -- For a source location occurring within the expansion of an instance of a 177 -- generic unit, the Line, Column, and File_Name selectors will indicate a 178 -- location within the generic; the Enclosing_Instance selector yields the 179 -- location of the declaration of the instance. 180 181 function Make 182 (File_Name : String; 183 Line : Line_Number; 184 Column : Column_Number; 185 Iteration : Iteration_Id; 186 Enclosing_Instance : Source_Location_Or_Null) return Source_Location; 187 -- Constructor 188 189 type Message_And_Location (<>) is private; 190 191 function Location (Item : Message_And_Location) return Source_Location; 192 function Message (Item : Message_And_Location) return SA_Message; 193 194 function Make_Msg_Loc 195 (Msg : SA_Message; 196 Loc : Source_Location) return Message_And_Location; 197 -- Selectors 198 199 function "<" (Left, Right : Message_And_Location) return Boolean; 200 function Hash (Key : Message_And_Location) return Hash_Type; 201 -- Actuals for container instances 202 203 File_Extension : constant String; -- ".json" (but could change in future) 204 -- Clients may wish to use File_Extension in constructing 205 -- File_Name parameters for calls to Open. 206 207 package Writing is 208 function Is_Open return Boolean; 209 210 procedure Open (File_Name : String) with 211 Precondition => not Is_Open, 212 Postcondition => Is_Open; 213 -- Behaves like Text_IO.Create with respect to error cases 214 215 procedure Write (Message : SA_Message; Location : Source_Location); 216 217 procedure Close with 218 Precondition => Is_Open, 219 Postcondition => not Is_Open; 220 -- Behaves like Text_IO.Close with respect to error cases 221 end Writing; 222 223 package Reading is 224 function Is_Open return Boolean; 225 226 procedure Open (File_Name : String; Full_Path : Boolean := True) with 227 Precondition => not Is_Open, 228 Postcondition => Is_Open; 229 -- Behaves like Text_IO.Open with respect to error cases 230 231 function Done return Boolean with 232 Precondition => Is_Open; 233 234 function Get return Message_And_Location with 235 Precondition => not Done; 236 237 procedure Close with 238 Precondition => Is_Open, 239 Postcondition => not Is_Open; 240 -- Behaves like Text_IO.Close with respect to error cases 241 end Reading; 242 243private 244 type Simple_Source_Location is record 245 File_Name : Unbounded_String := Null_Unbounded_String; 246 Line : Line_Number := Line_Number'Last; 247 Column : Column_Number := Column_Number'Last; 248 Iteration : Iteration_Id := (Kind => None); 249 end record; 250 251 type Source_Locations is 252 array (Natural range <>) of Simple_Source_Location; 253 254 type Source_Location_Or_Null (Count : Natural) is record 255 Locations : Source_Locations (1 .. Count); 256 end record; 257 258 Null_Location : constant Source_Location_Or_Null := 259 (Count => 0, Locations => (others => <>)); 260 261 type Message_And_Location (Count : Positive) is record 262 Message : SA_Message; 263 Location : Source_Location (Count => Count); 264 end record; 265 266 File_Extension : constant String := ".json"; 267end SA_Messages; 268