File : sa_messages.ads
1 ------------------------------------------------------------------------------
2 -- C O D E P E E R / S P A R K --
3 -- --
4 -- Copyright (C) 2015-2016, 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
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,
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
163 record
164 case Kind is
165 when Numbered =>
166 Number : Iteration_Number;
167 Of_Total : Iteration_Total;
168 when others =>
169 null;
170 end case;
171 end record;
172
173 function Iteration (Location : Source_Location) return Iteration_Id;
174
175 function Enclosing_Instance
176 (Location : Source_Location) return Source_Location_Or_Null;
177 -- For a source location occurring within the expansion of an instance of a
178 -- generic unit, the Line, Column, and File_Name selectors will indicate a
179 -- location within the generic; the Enclosing_Instance selector yields the
180 -- location of the declaration of the instance.
181
182 function Make
183 (File_Name : String;
184 Line : Line_Number;
185 Column : Column_Number;
186 Iteration : Iteration_Id;
187 Enclosing_Instance : Source_Location_Or_Null) return Source_Location;
188 -- Constructor
189
190 type Message_And_Location (<>) is private;
191
192 function Location (Item : Message_And_Location) return Source_Location;
193 function Message (Item : Message_And_Location) return SA_Message;
194
195 function Make_Msg_Loc
196 (Msg : SA_Message;
197 Loc : Source_Location) return Message_And_Location;
198 -- Selectors
199
200 function "<" (Left, Right : Message_And_Location) return Boolean;
201 function Hash (Key : Message_And_Location) return Hash_Type;
202 -- Actuals for container instances
203
204 File_Extension : constant String; -- ".json" (but could change in future)
205 -- Clients may wish to use File_Extension in constructing
206 -- File_Name parameters for calls to Open.
207
208 package Writing is
209 function Is_Open return Boolean;
210
211 procedure Open (File_Name : String) with
212 Precondition => not Is_Open,
213 Postcondition => Is_Open;
214 -- Behaves like Text_IO.Create with respect to error cases
215
216 procedure Write (Message : SA_Message; Location : Source_Location);
217
218 procedure Close with
219 Precondition => Is_Open,
220 Postcondition => not Is_Open;
221 -- Behaves like Text_IO.Close with respect to error cases
222 end Writing;
223
224 package Reading is
225 function Is_Open return Boolean;
226
227 procedure Open (File_Name : String; Full_Path : Boolean := True) with
228 Precondition => not Is_Open,
229 Postcondition => Is_Open;
230 -- Behaves like Text_IO.Open with respect to error cases
231
232 function Done return Boolean with
233 Precondition => Is_Open;
234
235 function Get return Message_And_Location with
236 Precondition => not Done;
237
238 procedure Close with
239 Precondition => Is_Open,
240 Postcondition => not Is_Open;
241 -- Behaves like Text_IO.Close with respect to error cases
242 end Reading;
243
244 private
245 type Simple_Source_Location is record
246 File_Name : Unbounded_String := Null_Unbounded_String;
247 Line : Line_Number := Line_Number'Last;
248 Column : Column_Number := Column_Number'Last;
249 Iteration : Iteration_Id := (Kind => None);
250 end record;
251
252 type Source_Locations is
253 array (Natural range <>) of Simple_Source_Location;
254
255 type Source_Location_Or_Null (Count : Natural) is record
256 Locations : Source_Locations (1 .. Count);
257 end record;
258
259 Null_Location : constant Source_Location_Or_Null :=
260 (Count => 0, Locations => (others => <>));
261
262 type Message_And_Location (Count : Positive) is record
263 Message : SA_Message;
264 Location : Source_Location (Count => Count);
265 end record;
266
267 File_Extension : constant String := ".json";
268 end SA_Messages;