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
|
-------------------------------------------------------------------------------
-- (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.
--
--=============================================================================
-- Overview
-- Checks sub-program declarations from node subprogram_declaration. These
-- nodes occur only in package declarations therefore well formation of
-- function_ and procedure_specifications are handled here as a special case
-- rather than using the more complex and general-purpose
-- wf_subprogram_specification.
-- NOTE 11/6/02
-- Declarations also occur in protected types but this procedure can
-- deal with those as well
--------------------------------------------------------------------------------
separate (Sem)
procedure Wf_Subprogram_Declaration
(Node : in STree.SyntaxNode;
Inherit_Node : in STree.SyntaxNode;
Context_Node : in STree.SyntaxNode;
Generic_Formal_Part_Node : in STree.SyntaxNode;
Current_Scope : in Dictionary.Scopes;
Generic_Unit : in Dictionary.Symbol;
Component_Data : in out ComponentManager.ComponentData;
The_Heap : in out Heap.HeapRecord;
Subprog_Sym : out Dictionary.Symbol)
is
Spec_Node : STree.SyntaxNode;
Ident_Node : STree.SyntaxNode;
Anno_Node : STree.SyntaxNode;
Global_Node : STree.SyntaxNode;
Dependency_Node : STree.SyntaxNode;
Declare_Node : STree.SyntaxNode;
Constraint_Node : STree.SyntaxNode;
Is_Overriding : Boolean := False;
begin
-- Determine and record in the variable Overriding_Indicator
-- if the procedure overrides a parent.
-- In SPARK 2005 "not overriding Procedure ..." is equivalent
-- to "Procedure ...".
-- This differs from Ada 2005 where a procedure may override
-- a parent procedure when no overriding_indicator is present.
Spec_Node := Child_Node (Current_Node => Node);
-- ASSUME Spec_Node = overriding_indicator OR procedure_specification OR function_specification OR
-- proof_function_declaration OR entry_specification
if Syntax_Node_Type (Node => Spec_Node) = SP_Symbols.overriding_indicator then
-- ASSUME Spec_Node = overriding_indicator
-- ASSUME Child_Node (Current_Node => Spec_Node) = RWoverriding OR RWnot
if Syntax_Node_Type (Node => Child_Node (Current_Node => Spec_Node)) = SP_Symbols.RWoverriding then
-- ASSUME Child_Node (Current_Node => Spec_Node) = RWoverriding
Is_Overriding := True;
elsif Syntax_Node_Type (Node => Child_Node (Current_Node => Spec_Node)) /= SP_Symbols.RWnot then
SystemErrors.Fatal_Error
(Sys_Err => SystemErrors.Invalid_Syntax_Tree,
Msg => "Expect Child_Node (Current_Node => Spec_Node) = RWoverriding OR RWnot in Wf_Subprogram_Declaration");
end if;
Spec_Node := Next_Sibling (Current_Node => Spec_Node);
elsif Syntax_Node_Type (Node => Spec_Node) /= SP_Symbols.procedure_specification
and then Syntax_Node_Type (Node => Spec_Node) /= SP_Symbols.function_specification
and then Syntax_Node_Type (Node => Spec_Node) /= SP_Symbols.proof_function_declaration
and then Syntax_Node_Type (Node => Spec_Node) /= SP_Symbols.entry_specification then
SystemErrors.Fatal_Error
(Sys_Err => SystemErrors.Invalid_Syntax_Tree,
Msg => "Expect Spec_Node = overriding_indicator OR procedure_specification OR function_specification OR " &
"proof_function_declaration OR entry_specification in Wf_Subprogram_Declaration");
end if;
--# assert STree.Table = STree.Table~ and
--# (Syntax_Node_Type (Node, STree.Table) = SP_Symbols.subprogram_declaration or
--# Syntax_Node_Type (Node, STree.Table) = SP_Symbols.not_overriding_subprogram_declaration or
--# Syntax_Node_Type (Node, STree.Table) = SP_Symbols.entry_declaration) and
--# (Syntax_Node_Type (Context_Node, STree.Table) = SP_Symbols.context_clause or Context_Node = STree.NullNode) and
--# (Syntax_Node_Type (Inherit_Node, STree.Table) = SP_Symbols.inherit_clause or Inherit_Node = STree.NullNode) and
--# (Syntax_Node_Type (Generic_Formal_Part_Node, STree.Table) = SP_Symbols.generic_formal_part or
--# Generic_Formal_Part_Node = STree.NullNode);
-- ASSUME Spec_Node = procedure_specification OR function_specification OR proof_function_declaration OR entry_specification
if Syntax_Node_Type (Node => Spec_Node) = SP_Symbols.procedure_specification
or else Syntax_Node_Type (Node => Spec_Node) = SP_Symbols.function_specification
or else Syntax_Node_Type (Node => Spec_Node) = SP_Symbols.entry_specification then
-- ASSUME Spec_Node = procedure_specification OR function_specification OR entry_specification
Anno_Node := Next_Sibling (Current_Node => Spec_Node);
-- ASSUME Anno_Node = procedure_annotation OR function_annotation
SystemErrors.RT_Assert
(C => Syntax_Node_Type (Node => Anno_Node) = SP_Symbols.procedure_annotation
or else Syntax_Node_Type (Node => Anno_Node) = SP_Symbols.function_annotation,
Sys_Err => SystemErrors.Invalid_Syntax_Tree,
Msg => "Expect Anno_Node = procedure_annotation OR function_annotation in Wf_Subprogram_Declaration");
--# accept Flow, 10, Global_Node, "Expected ineffective assignment" &
--# Flow, 10, Dependency_Node, "Expected ineffective assignment" &
--# Flow, 10, Declare_Node, "Expected ineffective assignment";
Get_Subprogram_Anno_Key_Nodes
(Node => Anno_Node,
Global_Node => Global_Node,
Dependency_Node => Dependency_Node,
Declare_Node => Declare_Node,
Constraint_Node => Constraint_Node);
--# end accept;
elsif Syntax_Node_Type (Node => Spec_Node) = SP_Symbols.proof_function_declaration then
-- ASSUME Spec_Node = proof_function_declaration
Anno_Node := STree.NullNode;
Constraint_Node := Last_Sibling_Of (Start_Node => Child_Node (Current_Node => Spec_Node));
-- ASSUME Constraint_Node = function_constraint
SystemErrors.RT_Assert
(C => Syntax_Node_Type (Node => Constraint_Node) = SP_Symbols.function_constraint,
Sys_Err => SystemErrors.Invalid_Syntax_Tree,
Msg => "Expect Constraint_Node = function_constraint in Wf_Subprogram_Declaration");
else
Anno_Node := STree.NullNode;
Constraint_Node := STree.NullNode;
SystemErrors.Fatal_Error
(Sys_Err => SystemErrors.Invalid_Syntax_Tree,
Msg => "Expect Spec_Node = procedure_specification OR function_specification OR " &
"proof_function_declaration OR entry_specification in Wf_Subprogram_Declaration");
end if;
--# assert STree.Table = STree.Table~ and
--# (Syntax_Node_Type (Node, STree.Table) = SP_Symbols.subprogram_declaration or
--# Syntax_Node_Type (Node, STree.Table) = SP_Symbols.not_overriding_subprogram_declaration or
--# Syntax_Node_Type (Node, STree.Table) = SP_Symbols.entry_declaration) and
--# (Syntax_Node_Type (Spec_Node, STree.Table) = SP_Symbols.procedure_specification or
--# Syntax_Node_Type (Spec_Node, STree.Table) = SP_Symbols.function_specification or
--# Syntax_Node_Type (Spec_Node, STree.Table) = SP_Symbols.proof_function_declaration or
--# Syntax_Node_Type (Spec_Node, STree.Table) = SP_Symbols.entry_specification) and
--# (Syntax_Node_Type (Anno_Node, STree.Table) = SP_Symbols.procedure_annotation or
--# Syntax_Node_Type (Anno_Node, STree.Table) = SP_Symbols.function_annotation or
--# Anno_Node = STree.NullNode) and
--# (Syntax_Node_Type (Constraint_Node, STree.Table) = SP_Symbols.function_constraint or
--# Syntax_Node_Type (Constraint_Node, STree.Table) = SP_Symbols.procedure_constraint) and
--# (Syntax_Node_Type (Context_Node, STree.Table) = SP_Symbols.context_clause or Context_Node = STree.NullNode) and
--# (Syntax_Node_Type (Inherit_Node, STree.Table) = SP_Symbols.inherit_clause or Inherit_Node = STree.NullNode) and
--# (Syntax_Node_Type (Generic_Formal_Part_Node, STree.Table) = SP_Symbols.generic_formal_part or
--# Generic_Formal_Part_Node = STree.NullNode);
if Syntax_Node_Type (Node => Spec_Node) = SP_Symbols.procedure_specification
or else Syntax_Node_Type (Node => Spec_Node) = SP_Symbols.function_specification
or else Syntax_Node_Type (Node => Spec_Node) = SP_Symbols.entry_specification then
-- ASSUME Spec_Node = procedure_specification OR function_specification OR entry_specification
Subprogram_Specification.Wf_Subprogram_Specification
(Spec_Node => Spec_Node,
Anno_Node => Anno_Node,
Constraint_Node => Constraint_Node,
Inherit_Node => Inherit_Node,
Context_Node => Context_Node,
Generic_Formal_Part_Node => Generic_Formal_Part_Node,
Current_Scope => Current_Scope,
Generic_Unit => Generic_Unit,
Current_Context => Dictionary.ProgramContext,
Component_Data => Component_Data,
The_Heap => The_Heap,
Subprog_Sym => Subprog_Sym);
Ident_Node := Child_Node (Current_Node => Child_Node (Current_Node => Spec_Node));
-- ASSUME Ident_Node = identifier
SystemErrors.RT_Assert
(C => Syntax_Node_Type (Node => Ident_Node) = SP_Symbols.identifier,
Sys_Err => SystemErrors.Invalid_Syntax_Tree,
Msg => "Expect Result = identifier in Wf_Subprogram_Declaration");
Check_No_Overloading_From_Tagged_Ops
(Ident_Node => Ident_Node,
Subprog_Sym => Subprog_Sym,
Scope => Current_Scope,
Abstraction => Dictionary.IsAbstract,
Is_Overriding => Is_Overriding);
elsif Syntax_Node_Type (Node => Spec_Node) = SP_Symbols.proof_function_declaration then
-- ASSUME Spec_Node = proof_function_declaration
Spec_Node := Child_Node (Current_Node => Spec_Node);
-- ASSUME Spec_Node = function_specification
SystemErrors.RT_Assert
(C => Syntax_Node_Type (Node => Spec_Node) = SP_Symbols.function_specification,
Sys_Err => SystemErrors.Invalid_Syntax_Tree,
Msg => "Expect Spec_Node = function_specification in Wf_Subprogram_Declaration");
Subprogram_Specification.Wf_Subprogram_Specification
(Spec_Node => Spec_Node,
Anno_Node => Anno_Node,
Constraint_Node => Constraint_Node,
Inherit_Node => Inherit_Node,
Context_Node => Context_Node,
Generic_Formal_Part_Node => Generic_Formal_Part_Node,
Current_Scope => Current_Scope,
Generic_Unit => Generic_Unit,
Current_Context => Dictionary.ProofContext,
Component_Data => Component_Data,
The_Heap => The_Heap,
Subprog_Sym => Subprog_Sym);
else
Subprog_Sym := Dictionary.NullSymbol;
end if;
--# accept Flow, 33, Global_Node, "Expected to be neither referenced nor exported" &
--# Flow, 33, Dependency_Node, "Expected to be neither referenced nor exported" &
--# Flow, 33, Declare_Node, "Expected to be neither referenced nor exported";
end Wf_Subprogram_Declaration;
|
