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
|
-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY 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 the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================
--------------------------------------------------------------------------------
--Synopsis: --
-- --
--Package providing a structure in which to store VC details. --
-- --
--To be used in tandem with the Heap data structure, hence the use of --
--Heap.Atom as the array range --
--------------------------------------------------------------------------------
with E_Strings;
with HeapIndex;
use type HeapIndex.IndexType;
--# inherit E_Strings,
--# HeapIndex;
package VCDetails is
type Terminal_Point_Type is (
Assert_Point,
Precondition_Check_Point,
Check_Statement_Point,
Runtime_Check_Point,
Refinement_VC_Point,
Inheritance_VC_Point,
Undetermined_Point);
-- These errors are the union of all possible errors types from
-- all possible analysis methods.
type Error_Type is (-- Missing VC files (NOT zombiescope)
Missing_SLG_File, -- SIV file, but no SLG file
Missing_VLG_File, -- VCT file, but no VLG file
-- Corrupt VC files (NOT zombiescope)
Corrupt_VCG_File, -- The VCG file itself has a problem
Corrupt_SIV_File, -- The SIV file was corrupted or malformed (simplifier)
Corrupt_SLG_File, -- The SLG file was corrupted or malformed (simplifier log)
Corrupt_VCT_File, -- The VCT file was corrupted or malformed (victor)
Corrupt_VLG_File, -- The VLG file was corrupted or malformed (victor log)
Corrupt_RSM_File, -- The RSM file was curripted or malformed (riposte summary)
Corrupt_PLG_File, -- The PLG file was corrupted or malformed (checker log)
Corrupt_PRV_File, -- The PLG file was corrupted or malformed (manual review)
-- Missing DPC files (zombiescope)
-- Corrupt DPC files (zombiescope)
Corrupt_DPC_File, -- The DPC file itself has a problem
Corrupt_SDP_File -- The SDP file was corrupted or malformed (zombiescope)
);
subtype Error_Type_Missing_VC_Files is Error_Type range Missing_SLG_File .. Missing_VLG_File;
subtype Error_Type_Corrupt_VC_Files is Error_Type range Corrupt_VCG_File .. Corrupt_PRV_File;
subtype Error_Type_Corrupt_DPC_Files is Error_Type range Corrupt_DPC_File .. Corrupt_SDP_File;
-- The possible states of a VC are:
-- * VC_Not_Present: There is no VC (the user has only generated dpc
-- files);
-- * VC_SIV_Not_Present: The Simplifier has not tried to discharge the VC.
-- * VC_Undischarged: The VC is undischarged - the Simplifier has failed to
-- discharge the VC;
-- * VC_Proved_By_Examiner: VC was discharged by the Examiner;
-- * VC_Proved_By_Inference: VC was dischaged by the Simplifier and the
-- proof is by inference;
-- * VC_Proved_By_Contradiction: VC was dischaged by the Simplifier
-- and the proof is by contradiction;
-- * VC_Proved_By_Checker: VC was discharged using the Checker;
-- * VC_Proved_By_Review: VC was discharged through a proof review file;
-- * VC_Proved_By_Using_Proof_Rules: VC was discharged using user proof
-- rules;
-- * VC_Proved_By_Victor: VC was discharged using Victor;
-- * VC_Proved_By_Riposte: VC was discharged using Riposte;
-- * VC_False: VC is false.
type VC_State_T is (
VC_Not_Present,
VC_SIV_Not_Present,
VC_Undischarged,
VC_Proved_By_Examiner,
VC_Proved_By_Inference,
VC_Proved_By_Contradiction,
VC_Proved_Using_User_Proof_Rules,
VC_Proved_By_Victor,
VC_Proved_By_Riposte,
VC_Proved_By_Checker,
VC_Proved_By_Review,
VC_False);
-- The possible states of a DPC are:
-- * DPC_Not_Present: There is no DPC (the user has only generated
-- VCG files).
-- * DPC_SIV_Not_Present: No SDP is present for DPC.
-- * DPC_Unchecked: The Examiner generated at DPC that does not required
-- ZombieScope to check for dead paths - e.g. RTCs
-- and asserts.
-- * DPC_Live: Path is not a dead path.
-- * DPC_Dead: Path is a dead path.
type DPC_State_T is (DPC_Not_Present, DPC_SDP_Not_Present, DPC_Unchecked, DPC_Live, DPC_Dead);
End_Type_Image_Length : constant := 12;
subtype End_Type_Image_Index is Positive range 1 .. End_Type_Image_Length;
subtype End_Type_Image_String is String (End_Type_Image_Index);
type End_Type_To_Image_Array is array (Terminal_Point_Type) of End_Type_Image_String;
End_Type_Image : constant End_Type_To_Image_Array :=
End_Type_To_Image_Array'
(Assert_Point => " assert @ ",
Precondition_Check_Point => "pre check @ ",
Check_Statement_Point => "check stm @ ",
Runtime_Check_Point => "rtc check @ ",
Refinement_VC_Point => "refinement ",
Inheritance_VC_Point => "inheritance ",
Undetermined_Point => " ");
type Data_Type is private;
procedure Add
(Details : in out Data_Type;
Index : out HeapIndex.IndexType;
Success : out Boolean;
Name : in E_Strings.T;
Path_Start : in E_Strings.T;
Path_End : in E_Strings.T;
End_Type : in Terminal_Point_Type;
VC_State : in VC_State_T;
DPC_State : in DPC_State_T);
--# derives Details from *,
--# DPC_State,
--# End_Type,
--# Name,
--# Path_End,
--# Path_Start,
--# VC_State &
--# Index,
--# Success from Details;
procedure Initialize (Details : out Data_Type);
--# derives Details from ;
procedure Raise_Error (Error_Kind : in Error_Type;
Details : in out Data_Type);
--# derives Details from *,
--# Error_Kind;
function Error_Raised (Error_Kind : in Error_Type;
Details : in Data_Type) return Boolean;
procedure Set_VC_State (Details : in out Data_Type;
Index : in HeapIndex.IndexType;
VC_State : in VC_State_T);
--# derives Details from *,
--# Index,
--# VC_State;
function Get_VC_State (Details : in Data_Type;
Index : in HeapIndex.IndexType) return VC_State_T;
procedure Set_DPC_State (Details : in out Data_Type;
Index : in HeapIndex.IndexType;
DPC_State : in DPC_State_T);
--# derives Details from *,
--# DPC_State,
--# Index;
function Get_DPC_State (Details : in Data_Type;
Index : in HeapIndex.IndexType) return DPC_State_T;
--------------------------------------------------------------------------
-- this compares the information given and returns
-- Result is as defined in section 5.4 of the specification
-- it works directly on values rather than on indices into the Details
-- structure so that information can be compared before insertion
-- NOTE : the procedure is successful iff neither Type is Invalid
--------------------------------------------------------------------------
procedure Order (First_Name : in E_Strings.T;
Second_Name : in E_Strings.T;
Result : out E_Strings.Order_Types);
--# derives Result from First_Name,
--# Second_Name;
procedure Retrieve
(Details : in Data_Type;
Index : in HeapIndex.IndexType;
Success : out Boolean;
Name : out E_Strings.T;
Path_Start : out E_Strings.T;
Path_End : out E_Strings.T;
End_Type : out Terminal_Point_Type;
VC_State : out VC_State_T;
DPC_State : out DPC_State_T);
--# derives DPC_State,
--# End_Type,
--# Name,
--# Path_End,
--# Path_Start,
--# Success,
--# VC_State from Details,
--# Index;
--------------------------------------------------------------------------
-- Path_End_To_Path_Type
--
-- Parses a Path End string to convert it into a Terminal Point Type
-- The basic patterns scanned for are:
-- ... to check ... -> check statement point
-- ... to run-time check ... -> run-time check point
-- ... to precondition check ... -> precondition check point
-- ... to assertion ... -> assertion point
-- ... refinement ... -> refinement VC point
-- ... inheritance ... -> inheritance VC point
-- ... anything else ... -> undetermined point
--------------------------------------------------------------------------
function Path_End_To_Path_Type (Line : E_Strings.T) return Terminal_Point_Type;
function End_Point_Type (Details : in Data_Type;
Index : in HeapIndex.IndexType) return Terminal_Point_Type;
private
type Details_Element is record
Name : E_Strings.T;
Path_Start : E_Strings.T;
Path_End : E_Strings.T;
End_Type : Terminal_Point_Type;
VC_State : VC_State_T;
DPC_State : DPC_State_T;
end record;
Null_Details_Element : constant Details_Element :=
Details_Element'
(Name => E_Strings.Empty_String,
Path_Start => E_Strings.Empty_String,
Path_End => E_Strings.Empty_String,
End_Type => Undetermined_Point,
VC_State => VC_Not_Present,
DPC_State => DPC_Not_Present);
type Elements_Array is array (HeapIndex.IndexType) of Details_Element;
-- Use an array to store the different error kinds that may be associated
-- with a subprogram. This construct may be extended by adding a new enumerated
-- type, without having to extend the subprogram interfaces.
type Error_Array is array (Error_Type) of Boolean;
-- High_Mark is the number of the highest allocated atom - zero if the
-- structure is empty
-- Error_Status records different kinds of errors that may be encountered
-- during analysis.
type Data_Type is record
Details : Elements_Array;
High_Mark : HeapIndex.IndexType;
Error_Status : Error_Array;
end record;
end VCDetails;
|
