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
|
-------------------------------------------------------------------------------
-- (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 combining Heap and VCDetails to give an ordered list of VC details. --
-- --
--This is implemented as an abstract state machine. This is possible as there --
--is only a single occurrence of the VCHeap in the program. It is necessary --
--to prevent unacceptable overheads of creating local copies of the embedded --
--Heap and VCDetails types to circumvent the entire variable rule. It would --
--also be possible to implement Heap and VCDetails as ASMs but not --
--necessarily desirable as this would affect the high level annotations of the--
--program. --
-- --
--------------------------------------------------------------------------------
with E_Strings;
with Heap;
with VCDetails;
use type Heap.Atom;
--# inherit E_Strings,
--# FatalErrors,
--# Heap,
--# HeapIndex,
--# VCDetails;
package VCHeap
--# own I_State;
--# State;
is
-- Start_Index is a point in the linked list at which to start the
-- search. This is used to start insertion at the first VC.
-- If the name table is full, a fatal error is produced and Add does not
-- return
procedure Add
(Start_Index : in Heap.Atom;
New_Name : in E_Strings.T;
Path_Start : in E_Strings.T;
Path_End : in E_Strings.T;
End_Type : in VCDetails.Terminal_Point_Type;
VC_State : in VCDetails.VC_State_T;
DPC_State : in VCDetails.DPC_State_T);
--# global in out FatalErrors.State;
--# in out I_State;
--# in out State;
--# derives FatalErrors.State,
--# State from *,
--# DPC_State,
--# End_Type,
--# New_Name,
--# Path_End,
--# Path_Start,
--# Start_Index,
--# State,
--# VC_State &
--# I_State from *,
--# New_Name,
--# Path_End,
--# Path_Start;
-- this procedure returns the VC details for the specified entry in the
-- linked list.
procedure Details
(List_Index : in Heap.Atom;
VC_Name : out E_Strings.T;
Path_Start : out E_Strings.T;
Path_End : out E_Strings.T;
End_Type : out VCDetails.Terminal_Point_Type;
VC_State : out VCDetails.VC_State_T;
DPC_State : out VCDetails.DPC_State_T);
--# global in State;
--# derives DPC_State,
--# End_Type,
--# Path_End,
--# Path_Start,
--# VC_Name,
--# VC_State from List_Index,
--# State;
function First_Entry return Heap.Atom;
--# global in State;
procedure Initialize;
--# global out I_State;
--# out State;
--# derives I_State,
--# State from ;
procedure Raise_Error (Error_Kind : in VCDetails.Error_Type);
--# global in out State;
--# derives State from *,
--# Error_Kind;
function Error_Raised (Error_Kind : in VCDetails.Error_Type) return Boolean;
--# global in State;
procedure Reinitialize
(First_Element : in E_Strings.T;
First_Path_Start : in E_Strings.T;
First_Path_End : in E_Strings.T;
First_End_Type : in VCDetails.Terminal_Point_Type);
--# global out I_State;
--# out State;
--# derives I_State from First_Element,
--# First_Path_End,
--# First_Path_Start &
--# State from First_Element,
--# First_End_Type,
--# First_Path_End,
--# First_Path_Start;
-- this procedure returns the 'Next_One' ordered element in VCH after
-- 'After_This'. It is successful if the Next_One is not a 'null' pointer
procedure Next (After_This : in Heap.Atom;
Success : out Boolean;
Next_One : out Heap.Atom);
--# global in State;
--# derives Next_One,
--# Success from After_This,
--# State;
procedure Set_VC_State (VC_Name : in E_Strings.T;
VC_State : in VCDetails.VC_State_T);
--# global in out FatalErrors.State;
--# in out State;
--# derives FatalErrors.State from *,
--# State,
--# VC_Name &
--# State from *,
--# VC_Name,
--# VC_State;
function Get_VC_State (VC_Name : in E_Strings.T) return VCDetails.VC_State_T;
--# global in State;
procedure Set_DPC_State (DPC_Name : in E_Strings.T;
DPC_State : in VCDetails.DPC_State_T);
--# global in out FatalErrors.State;
--# in out State;
--# derives FatalErrors.State from *,
--# DPC_Name,
--# State &
--# State from *,
--# DPC_Name,
--# DPC_State;
function Exists (VC_Name : E_Strings.T) return Boolean;
--# global in State;
procedure Get_VC_Name_End_Type (VC_Name : in E_Strings.T;
VC_Type : out VCDetails.Terminal_Point_Type);
--# global in State;
--# in out FatalErrors.State;
--# derives FatalErrors.State from *,
--# State,
--# VC_Name &
--# VC_Type from State,
--# VC_Name;
function Get_Longest_VC_Name_Length return Integer;
--# global in I_State;
function Get_Longest_VC_Start_Length return Integer;
--# global in I_State;
function Get_Longest_VC_End_Length return Integer;
--# global in I_State;
function Get_VC_Name_Prefix return E_Strings.T;
--# global in I_State;
end VCHeap;
|
