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
|
-------------------------------------------------------------------------------
-- (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.
--
--=============================================================================
separate (Sem)
procedure Wf_Subprogram_Annotation
(Node : in STree.SyntaxNode;
Current_Scope : in Dictionary.Scopes;
Subprog_Sym : in Dictionary.Symbol;
First_Seen : in Boolean;
The_Heap : in out Heap.HeapRecord)
is
-- look up table: if First_Seen then we are dealing with Abstract spec else Refined
type Which_Abstractions is array (Boolean) of Dictionary.Abstractions;
Which_Abstraction : constant Which_Abstractions :=
Which_Abstractions'(False => Dictionary.IsRefined,
True => Dictionary.IsAbstract);
Glob_Def_Err : Boolean := False;
Global_Has_Errors : Boolean := False;
Report_Node_Pos : LexTokenManager.Token_Position;
Global_Node : STree.SyntaxNode;
Dependency_Node : STree.SyntaxNode;
Declare_Node : STree.SyntaxNode;
Constraint_Node : STree.SyntaxNode;
begin
--# accept Flow, 10, Constraint_Node, "Expected ineffective assignment";
Get_Subprogram_Anno_Key_Nodes
(Node => Node,
Global_Node => Global_Node,
Dependency_Node => Dependency_Node,
Declare_Node => Declare_Node,
Constraint_Node => Constraint_Node);
--# end accept;
Report_Node_Pos := Node_Position (Node => Parent_Node (Current_Node => Node));
if Syntax_Node_Type (Node => Node) = SP_Symbols.procedure_annotation
and then not First_Seen
and then Global_Node = STree.NullNode then
Global_Has_Errors := True;
ErrorHandler.Semantic_Error
(Err_Num => 87,
Reference => ErrorHandler.No_Reference,
Position => Report_Node_Pos,
Id_Str => Dictionary.GetSimpleName (Subprog_Sym));
end if;
if Syntax_Node_Type (Node => Global_Node) = SP_Symbols.moded_global_definition then
-- ASSUME Global_Node = moded_global_definition
Report_Node_Pos := Node_Position (Node => Global_Node);
if Dictionary.Is_Generic_Subprogram (The_Symbol => Subprog_Sym) then
ErrorHandler.Semantic_Error
(Err_Num => 638,
Reference => ErrorHandler.No_Reference,
Position => Report_Node_Pos,
Id_Str => LexTokenManager.Null_String);
Global_Has_Errors := True;
else
Wf_Global_Definition
(Node => Global_Node,
Scope => Current_Scope,
Subprog_Sym => Subprog_Sym,
First_Seen => First_Seen,
Sem_Err_Found => Glob_Def_Err);
Global_Has_Errors := Global_Has_Errors or else Glob_Def_Err;
end if;
end if;
if Syntax_Node_Type (Node => Dependency_Node) = SP_Symbols.dependency_relation then
-- ASSUME Dependency_Node = dependency_relation
Report_Node_Pos := Node_Position (Node => Dependency_Node);
Dependency_Relation.Wf_Dependency_Relation
(Node => Dependency_Node,
Scope => Current_Scope,
Subprog_Sym => Subprog_Sym,
First_Seen => First_Seen,
Glob_Def_Err => Glob_Def_Err,
The_Heap => The_Heap);
end if;
if Syntax_Node_Type (Node => Declare_Node) = SP_Symbols.declare_annotation then
-- ASSUME Declare_Node = declare_annotation
Wf_Declare_Annotation
(Node => Declare_Node,
Scope => Current_Scope,
Task_Or_Proc => Subprog_Sym,
First_Seen => First_Seen,
The_Heap => The_Heap);
end if;
if Syntax_Node_Type (Node => Node) = SP_Symbols.procedure_annotation then
Add_Derives_Stream_Effects
(Node_Pos => Node_Position (Node => Node),
Subprog_Sym => Subprog_Sym,
Abstraction => Which_Abstraction (First_Seen));
end if;
-- mark subprogram as having incorrect signature if necessary
if Global_Has_Errors then
Dictionary.SetSubprogramSignatureNotWellformed (Which_Abstraction (First_Seen), Subprog_Sym);
end if;
-- Raise error 501 (dependency relation expected) if:
-- 1. flow=info and there was no derives, or
-- 2. flow=auto, global is refined and there was a derives on the spec,
-- 3. flow=data, language=83 and there was no derives.
-- Generally, if flow=data (and lang /= 83) or flow=auto a derives is not required because
-- there will be a moded global annotation if one is necessary. However, if flow=auto and there
-- are refined own variables in the annotation, and there was a dependency annotation on the
-- spec then one is expected on the body (case 2 in the list above).
if Syntax_Node_Type (Node => Node) = SP_Symbols.procedure_annotation then
if Dependency_Node = STree.NullNode then -- no derives on body
if CommandLineData.Content.Flow_Option = CommandLineData.Info_Flow -- 1
or else (CommandLineData.Content.Flow_Option = CommandLineData.Auto_Flow
and then not First_Seen
and then Dictionary.GetHasDerivesAnnotation (Subprog_Sym)) --2
or else (CommandLineData.Content.Flow_Option = CommandLineData.Data_Flow
and then CommandLineData.Content.Language_Profile = CommandLineData.SPARK83) then --3
-- Here we definitely know that the derives annotation is missing
if Global_Node = STree.NullNode and then Declare_Node = STree.NullNode then
Dictionary.SetSubprogramSignatureNotWellformed (Dictionary.IsAbstract, Subprog_Sym);
ErrorHandler.Semantic_Error
(Err_Num => 154,
Reference => ErrorHandler.No_Reference,
Position => Report_Node_Pos,
Id_Str => Dictionary.GetSimpleName (Subprog_Sym));
else
Dictionary.SetSubprogramSignatureNotWellformed (Which_Abstraction (First_Seen), Subprog_Sym);
ErrorHandler.Semantic_Error
(Err_Num => 501,
Reference => ErrorHandler.No_Reference,
Position => Report_Node_Pos,
Id_Str => LexTokenManager.Null_String);
end if;
end if;
else -- there was a derives on the body
-- Similarly, if there was a dependency found, and flow=auto, and there was no dependency on the spec,
-- and the annotation is in terms of refined variables, then raise semantic error 509.
if CommandLineData.Content.Flow_Option = CommandLineData.Auto_Flow
and then not First_Seen
and then not Dictionary.GetHasDerivesAnnotation (Subprog_Sym) then
Dictionary.SetSubprogramSignatureNotWellformed (Which_Abstraction (First_Seen), Subprog_Sym);
ErrorHandler.Semantic_Error
(Err_Num => 509,
Reference => ErrorHandler.No_Reference,
Position => Report_Node_Pos,
Id_Str => LexTokenManager.Null_String);
end if;
end if;
end if;
--# accept Flow, 33, Constraint_Node, "Expected to be neither referenced nor exported";
end Wf_Subprogram_Annotation;
|
