1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
|
------------------------------------------------------------------------------
-- C O D E P E E R --
-- --
-- Copyright (C) 2008-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. --
-- --
-- The CodePeer technology was originally developed by SofCheck, Inc. --
------------------------------------------------------------------------------
-- This package isolates the enumeration of message_kinds produced by the
-- the backend and potential other checkers.
-- IMPORTANT Note: do NOT add any with clause in this package, so that
-- Message_Kinds can be used as a standalone package, with no dependencies.
package Message_Kinds is
type Message_Subkind is
-- Each Checker_Message_Kind has a Subkind field, which tells whether it's
-- an annotation or an error, and which kind of annotation or error.
-- There is exactly one Module_Annotation/Procedure_Annotation per SCIL
-- module/procedure; these aren't really "messages", but just
-- placeholders to hold the name and source position.
-- The Module_Annotation comes before all Procedure_Annotations
-- for procedures in that module.
-- The Procedure_Annotation comes before all other messages
-- for that procedure.
-- Note: avoid deleting message kinds so that old messages stay valid.
-- Note: adding a new message subkind may require adding a corresponding
-- new element to the enumeration type
-- BE.SCIL.Auxiliary_Types.Annotation_Check_Kind.
-- For details, see lengthy comment in
-- BE.PVP.Mess.User_Review_For_Message.Kinds_Matching_Table_Is_Ok
-- When adding a new kind, please also consider updating the various
-- Is_xxx functions below, in particular Is_Documented_Kind.
(Module_Annotation,
Procedure_Annotation,
End_Module_Annotation, -- TBD: Not sure of exact rules for these.
End_Procedure_Annotation, -- TBD.
Input_Annotation,
Output_Annotation,
New_Obj_Annotation,
Precondition_Annotation,
Presumption_Annotation,
Postcondition_Annotation,
-- another annotation:
Unknown_Call_Annotation,
-- another annotation:
Test_Vector_Annotation,
-- Implicit warnings
Non_Analyzed_Call_Warning, -- We are making a call that is
-- "too_complex"
Suspicious_Precondition_Warning, -- NOTE: No longer used
Suspicious_Range_Precondition_Warning, -- Precondition looks fishy
Suspicious_First_Precondition_Warning, -- Precondition looks fishy
Suspicious_Input_Warning, -- Out param read before assigned
Suspicious_Constant_Operation_Warning, -- Operation computes a constant
Unread_In_Out_Parameter_Warning, -- Mode in out could be mode out
Unassigned_In_Out_Parameter_Warning, -- In out param never assigned
-- Implicit checks. See the documentation of Check_Stm in
-- SCIL.Statements for the semantics of these.
Precondition_Check, -- Must be first check so subranges work
Postcondition_Check,
User_Precondition_Check,
Invalid_Check,
Invalid_Or_Null_Check,
Freed_Check, -- Invalid access value due to unchecked_deallocation
Divide_By_Zero_Check,
Boolean_Check,
Non_Neg_Check,
Negative_Exponent_Check,
User_Assign_Stm_Check,
Pre_Assign_Stm_Check, -- Implicitly generated pre-call assignments
Post_Assign_Stm_Check, -- ...post-call...
Aliasing_Check, -- For checking parameter aliasing
-- Explicit checks (corresponding to Check_Stm/Check_Exp).
Raise_Check, -- Unconditional explicit raise/throw
Conditional_Raise_Check, -- Conditional raise/throw (presuming FE
-- recognizes user-written "if ... then raise")
Array_Indexing_Check, -- Array bounds or length check
Assertion_Check, -- Assert statement/pragma
Numeric_Overflow_Check, -- Check against physical bounds of type
Numeric_Range_Check, -- Check against declared range
Floating_Point_Underflow_Check,
Type_Variant_Check, -- Variant record check
Tag_Check, -- Type tag check
Procedure_Does_Not_Return_Error, -- Procedure never returns
Check_Fails_On_Every_Call_Error, -- Procedure fails a check
Unlocked_Reentrant_Update_Error,
Unlocked_Shared_Daemon_Update_Error,
Mismatched_Locked_Update_Error,
Unknown_Call_Warning, -- We are making a call on an unknown proc
Dead_Store_Warning,
Dead_Outparam_Store_Warning, -- assign into outparam
Potentially_Dead_Store_Warning, -- assign into dmod
Same_Value_Dead_Store_Warning,
Dead_Block_Warning, -- "Interesting" Basic block is dead
Infinite_Loop_Warning, -- Infinite loop
Dead_Edge_Warning, -- unused, replaced with the following warnings
Plain_Dead_Edge_Warning, -- Test leading to interesting Basic Block
-- always goes the same way
True_Dead_Edge_Warning, -- A test is always "true", so that the other
-- edge is dead
False_Dead_Edge_Warning, -- A test is always "false", so that the other
-- edge is dead
True_Condition_Dead_Edge_Warning, -- A condition is always "true", so
-- that the other edge is dead
False_Condition_Dead_Edge_Warning, -- A condition is always "false", so
-- that the other edge is dead
Unrepeatable_While_Loop_Warning,
-- A while-loop's body will never execute more than once
-- used to represent the obj_ids that have been modified but not used
-- locally (do not appear in the listing)
Locally_Unused_Store_Annotation,
Dead_Block_Continuation_Warning, -- Block that is dead because
-- its predecessors are dead.
Local_Lock_Of_Global_Object, -- message detected during race_condition
-- limitation warnings
Analyzed_Module_Warning, -- info
Non_Analyzed_Module_Warning, -- module was poisoned
Non_Analyzed_Procedure_Warning, -- procedure was poisoned
Incompletely_Analyzed_Procedure_Warning, -- incomplete analysis
-- Two security-related checks
SQL_Injection_Check, -- using tainted data in an SQL command
XSS_Check, -- Cross-site scripting; using tainted data in HTML output
-- GNAT Warning messages
GNAT_Warning,
-- GNATcheck messages
GNATcheck);
subtype BE_Message_Subkind is Message_Subkind range
Module_Annotation .. XSS_Check;
subtype External_Message_Subkind is Message_Subkind range
GNAT_Warning .. GNATcheck;
-- NOTE: These subranges are generally *not* to be used
-- to distinguish, e.g., "informational" from "warning" messages,
-- because we no longer guarantee that all messages of the
-- same category will get contiguous enumeration literals
-- (because we want to avoid invalidating existing databases).
-- Use functions Is_Warning, Is_Warning_Or_Check,
-- Is_Informational, etc. for that purpose (see functions below).
-- Those functions will make use of these subranges as appropriate.
subtype Place_Holder_Subkind is BE_Message_Subkind range
Module_Annotation .. End_Procedure_Annotation;
subtype Annotation_Subkind is BE_Message_Subkind range
Module_Annotation .. Postcondition_Annotation;
subtype Method_Annotation_Subkind is BE_Message_Subkind range
Input_Annotation .. Postcondition_Annotation;
subtype Pre_Post_Annotation_Subkind is BE_Message_Subkind range
Precondition_Annotation .. Postcondition_Annotation;
subtype In_Out_Annotation_Subkind is BE_Message_Subkind range
Input_Annotation .. Output_Annotation;
-- cannot have this subtype as the range is no longer contiguous
-- subtype Warning_Subkind is BE_Message_Subkind
-- range Unknown_Call_Warning .. Suspicious_Precondition_Warning;
subtype Suspicious_Precondition_Subkind is BE_Message_Subkind range
Suspicious_Precondition_Warning ..
Suspicious_First_Precondition_Warning;
subtype Pre_Or_Post_Check is BE_Message_Subkind range
Precondition_Check .. Postcondition_Check;
subtype Error_Subkind is BE_Message_Subkind range
Precondition_Check .. Mismatched_Locked_Update_Error;
subtype Warning_Or_Error_Subkind is BE_Message_Subkind range
Non_Analyzed_Call_Warning .. Unrepeatable_While_Loop_Warning;
subtype Check_Kind_Enum is Error_Subkind range
Precondition_Check .. Tag_Check;
subtype Local_Check is Check_Kind_Enum
-- all but Precondition_Check and Postcondition_Check
range
Check_Kind_Enum'Succ (Postcondition_Check) .. Check_Kind_Enum'Last;
subtype Assign_Stm_Check is Check_Kind_Enum range
User_Assign_Stm_Check .. Post_Assign_Stm_Check;
subtype Race_Condition_Subkind is BE_Message_Subkind range
Unlocked_Reentrant_Update_Error .. Mismatched_Locked_Update_Error;
-- Note: do not include the Local_Lock_Of_Global_Object
subtype Dead_Store_Subkind is BE_Message_Subkind range
Dead_Store_Warning .. Same_Value_Dead_Store_Warning;
subtype Dead_Control_Flow_Subkind is BE_Message_Subkind range
Dead_Block_Warning .. Unrepeatable_While_Loop_Warning;
subtype Condition_Dead_Edge_Subkind is BE_Message_Subkind range
True_Condition_Dead_Edge_Warning .. Unrepeatable_While_Loop_Warning;
subtype Decision_Dead_Edge_Subkind is BE_Message_Subkind range
Dead_Edge_Warning .. False_Dead_Edge_Warning;
subtype Dead_Edge_Subkind is BE_Message_Subkind range
Dead_Edge_Warning .. Unrepeatable_While_Loop_Warning;
subtype Security_Check_Subkind is BE_Message_Subkind range
SQL_Injection_Check .. XSS_Check;
subtype All_Checks_Subkind is BE_Message_Subkind range
Check_Kind_Enum'First .. Security_Check_Subkind'Last;
-- This subrange is meant to cover *all* "checks" though
-- it might not be contiguous
subtype Non_Checks_Subkind is All_Checks_Subkind range
All_Checks_Subkind'Succ (Check_Kind_Enum'Last) ..
All_Checks_Subkind'Pred (Security_Check_Subkind'First);
-- This subrange covers the "hole" in All_Checks_Subkind
subtype All_Checks_With_External_Subkinds is Message_Subkind range
All_Checks_Subkind'First .. Message_Subkind'Last;
type Check_Kinds_Array is array (Check_Kind_Enum) of Boolean;
pragma Pack (Check_Kinds_Array);
Check_Kinds_Array_Default : constant Check_Kinds_Array :=
(others => False);
Check_Kinds_String_Default : constant String := "";
function Is_Documented_Kind (M : Message_Subkind) return Boolean is
(case M is
when Non_Analyzed_Call_Warning
| Suspicious_First_Precondition_Warning .. Invalid_Or_Null_Check
| Divide_By_Zero_Check
| Aliasing_Check .. Numeric_Range_Check
| Type_Variant_Check .. Infinite_Loop_Warning
| Plain_Dead_Edge_Warning .. True_Condition_Dead_Edge_Warning
| Dead_Block_Continuation_Warning
| Analyzed_Module_Warning ..
Incompletely_Analyzed_Procedure_Warning => True,
when others => False);
-- Lists all warning/checks/info messages that should be documented
function CWE_Ids
(Kind : Message_Subkind;
Msg : String := "") return String;
-- Return the set of applicate CWE ids for Kind, or """ if none.
-- Msg if not null is the message string associated with the message
-- which can be used to e.g. differentiate between precondition messages.
function Is_Security_Relevant
(Kind : BE_Message_Subkind;
Msg : String;
Runtime_Check : Boolean) return Boolean;
-- Return True if the given Kind/Msg is relevant for security.
-- Runtime_Check tells whether runtime checks (e.g. range/overflow/index)
-- should be considered as security relevant or not.
function Primary_Original_Checks
(Original_Checks : Check_Kinds_Array) return Check_Kinds_Array;
-- Returns a subset of Original_Checks with only the check_kinds
-- with the highest precedence (which add the strictest constraints)
function Improve_Number_Readability_In_Messages
(S : String;
For_HTML_Output : Boolean := True)
return String;
-- Make various improvements to numbers, such as
-- replacing near powers-of-2 by 2<sup>X +/- n, or
-- Integer_xx'First/Last +/- n.
-- If For_HTML_Output is True, will use HTML (e.g. "2<sup>X"), otherwise
-- Text (e.g. "2**X").
function Is_Annotation (Subkind : Message_Subkind) return Boolean;
function Is_Method_Annotation (Subkind : Message_Subkind) return Boolean;
-- true if subkind is in annotation subkinds, or locally_unused_assignment
function Is_Stored_In_DB_Method_Annotation
(Subkind : Message_Subkind)
return Boolean;
-- same as above, but only keep certain messages (no input/output)
function Is_Warning (Subkind : Message_Subkind) return Boolean;
-- Return True if message is not considered a check, which
-- means there is no reason to add "check that ..." in front
-- of the text of the message. Also, these messages are
-- *not* counted as one of the "check-related" messages.
function Is_Check (Subkind : Message_Subkind) return Boolean;
-- Returns True if message is a check.
function Is_Warning_Or_Check (Subkind : Message_Subkind) return Boolean;
-- Return True if message is to be counted in the count of
-- all messages. This includes race condition messages,
-- dead stores, external checkers, GNAT warnings etc.
function Is_Informational (Subkind : Message_Subkind) return Boolean;
-- Return True if "Subkind" is an informational message.
-- An informational message is NOT counted in the error counts,
-- nor is it part of the next/prev chain in the message-window.
-- However, it is "printable", and if you click on it, in the
-- source window, an informational message will be printed in the
-- message window.
end Message_Kinds;
|
