]>
Commit | Line | Data |
---|---|---|
d40800cf PMR |
1 | ------------------------------------------------------------------------------ |
2 | -- C O D E P E E R / S P A R K -- | |
3 | -- -- | |
8d0d46f4 | 4 | -- Copyright (C) 2015-2021, AdaCore -- |
d40800cf PMR |
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 | ||
19 | pragma Ada_2012; | |
20 | ||
21 | with Ada.Containers; use Ada.Containers; | |
22 | with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; | |
23 | ||
24 | package 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, | |
ae8c5626 | 97 | -- Loop_Invariant, Loop_Variant, Refined_Post, and Subprogram_Variant. |
d40800cf | 98 | -- |
4463d6ee | 99 | -- It might be nice to distinguish these different kinds of assertions |
d40800cf PMR |
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 | ||
243 | private | |
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"; | |
267 | end SA_Messages; |