1 ------------------------------------------------------------------------------
2 -- C O D E P E E R / S P A R K --
4 -- Copyright (C) 2015-2018, AdaCore --
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 --
17 ------------------------------------------------------------------------------
21 with Ada
.Containers
; use Ada
.Containers
;
22 with Ada
.Strings
.Unbounded
; use Ada
.Strings
.Unbounded
;
24 package SA_Messages
is
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.
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.
48 type Message_Kind
is (
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
,
73 Dead_Outparam_Store_Warning
,
74 Potentially_Dead_Store_Warning
,
75 Same_Value_Dead_Store_Warning
,
77 Infinite_Loop_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
);
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.
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.
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 .
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;
113 -- Possible outcomes of the static analysis of a runtime check
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
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
);
128 type SA_Message
(Kind
: Message_Kind
:= Message_Kind
'Last) is record
131 Check_Result
: SA_Check_Result
;
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
;
143 type Line_Number
is new Positive;
144 type Column_Number
is new Positive;
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
;
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.
159 subtype Iteration_Number
is Integer range 1 .. 255;
160 subtype Iteration_Total
is Integer range 2 .. 255;
162 type Iteration_Id
(Kind
: Iteration_Kind
:= None
) is record
165 Number
: Iteration_Number
;
166 Of_Total
: Iteration_Total
;
172 function Iteration
(Location
: Source_Location
) return Iteration_Id
;
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.
184 Column
: Column_Number
;
185 Iteration
: Iteration_Id
;
186 Enclosing_Instance
: Source_Location_Or_Null
) return Source_Location
;
189 type Message_And_Location
(<>) is private;
191 function Location
(Item
: Message_And_Location
) return Source_Location
;
192 function Message
(Item
: Message_And_Location
) return SA_Message
;
194 function Make_Msg_Loc
196 Loc
: Source_Location
) return Message_And_Location
;
199 function "<" (Left
, Right
: Message_And_Location
) return Boolean;
200 function Hash
(Key
: Message_And_Location
) return Hash_Type
;
201 -- Actuals for container instances
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.
208 function Is_Open
return Boolean;
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
215 procedure Write
(Message
: SA_Message
; Location
: Source_Location
);
218 Precondition
=> Is_Open
,
219 Postcondition
=> not Is_Open
;
220 -- Behaves like Text_IO.Close with respect to error cases
224 function Is_Open
return Boolean;
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
231 function Done
return Boolean with
232 Precondition
=> Is_Open
;
234 function Get
return Message_And_Location
with
235 Precondition
=> not Done
;
238 Precondition
=> Is_Open
,
239 Postcondition
=> not Is_Open
;
240 -- Behaves like Text_IO.Close with respect to error cases
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
);
251 type Source_Locations
is
252 array (Natural range <>) of Simple_Source_Location
;
254 type Source_Location_Or_Null
(Count
: Natural) is record
255 Locations
: Source_Locations
(1 .. Count
);
258 Null_Location
: constant Source_Location_Or_Null
:=
259 (Count
=> 0, Locations
=> (others => <>));
261 type Message_And_Location
(Count
: Positive) is record
262 Message
: SA_Message
;
263 Location
: Source_Location
(Count
=> Count
);
266 File_Extension
: constant String := ".json";