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
|
-------------------------------------------------------------------------------
-- (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 (ErrorHandler.Conversions.ToString)
procedure UsageError (Err_Num : in Error_Types.NumericError;
With_Explanation : in Boolean;
E_Str : in out E_Strings.T) is
Err_Type : ErrorHandler.Usage_Err_Type;
procedure UsageErrorExpl (E_Str : in out E_Strings.T)
--# global in Err_Type;
--# derives E_Str from *,
--# Err_Type;
is separate;
-- Note that the parameter names for this subunit are chosen to make it as easy as
-- possible to auto-generate the subunit from this, its parent, file. The
-- generation requires copying the case statement below, stripping out the
-- current Append'Thing' statements and adding an Append_String for the
-- explanatory text that is delineated by --! comments.
procedure Append_Explanation
--# global in Err_Type;
--# in With_Explanation;
--# in out E_Str;
--# derives E_Str from *,
--# Err_Type,
--# With_Explanation;
is
Explanation_String : E_Strings.T := E_Strings.Empty_String;
begin
if With_Explanation then
-- we need to at least look for an explanation
UsageErrorExpl (E_Str => Explanation_String);
if E_Strings.Get_Length (E_Str => Explanation_String) > 0 then
-- there actually is one
E_Strings.Append_String (E_Str => E_Str,
Str => ErrorHandler.Explanation_Prefix);
E_Strings.Append_Examiner_String (E_Str1 => E_Str,
E_Str2 => Explanation_String);
E_Strings.Append_String (E_Str => E_Str,
Str => ErrorHandler.Explanation_Postfix);
end if;
end if;
end Append_Explanation;
begin
Err_Type := ErrorHandler.Usage_Err_Type'Val (Err_Num.ErrorNum - Error_Types.UsageErrOffset);
case Err_Type is
-- HTML Directives
--! <NameFormat> <"flow-"><Name>
--! <ErrorFormat> <"!!! Flow Error : "><Name><" : "><Error>
when ErrorHandler.Unused_Import =>
--! <Name> 30
E_Strings.Append_String (E_Str => E_Str,
Str => "The variable ");
Append_Name (E_Str => E_Str,
Name => Err_Num.Name1,
Scope => Err_Num.Scope);
E_Strings.Append_String (E_Str => E_Str,
Str => " is imported but neither referenced nor exported");
when ErrorHandler.Undefined_Export =>
--! <Name> 31
if Err_Num.Name1 = Error_Types.NoName then
E_Strings.Append_String (E_Str => E_Str,
Str => "The returned function value is not defined");
else
E_Strings.Append_String (E_Str => E_Str,
Str => "The variable ");
Append_Name (E_Str => E_Str,
Name => Err_Num.Name1,
Scope => Err_Num.Scope);
E_Strings.Append_String (E_Str => E_Str,
Str => " is exported but not (internally) defined");
end if;
--! <Error> The variable XXX is exported but not (internally) defined.
when ErrorHandler.Undefined_Var =>
--! <Name> 32
E_Strings.Append_String (E_Str => E_Str,
Str => "The variable ");
Append_Name (E_Str => E_Str,
Name => Err_Num.Name1,
Scope => Err_Num.Scope);
E_Strings.Append_String (E_Str => E_Str,
Str => " is neither imported nor defined");
when ErrorHandler.Unreferenced_Var =>
--! <Name> 33
E_Strings.Append_String (E_Str => E_Str,
Str => "The variable ");
Append_Name (E_Str => E_Str,
Name => Err_Num.Name1,
Scope => Err_Num.Scope);
E_Strings.Append_String (E_Str => E_Str,
Str => " is neither referenced nor exported");
when ErrorHandler.Redefined_Import =>
--! <Name> 34
E_Strings.Append_String (E_Str => E_Str,
Str => "The imported, non-exported variable ");
Append_Name (E_Str => E_Str,
Name => Err_Num.Name1,
Scope => Err_Num.Scope);
E_Strings.Append_String (E_Str => E_Str,
Str => " may be redefined");
--! The updating of imported-only variables is forbidden under all
--! circumstances.
when ErrorHandler.Ineffective_Import =>
--! <Name> 35
E_Strings.Append_String (E_Str => E_Str,
Str => "Importation of the initial value of variable ");
Append_Name (E_Str => E_Str,
Name => Err_Num.Name1,
Scope => Err_Num.Scope);
E_Strings.Append_String (E_Str => E_Str,
Str => " is ineffective");
--! The meaning of this message is explained in Section 4.2 of Appendix A
when ErrorHandler.Referenced_But_Not_In_Partition =>
--! <Name> 36
E_Strings.Append_String (E_Str => E_Str,
Str => "The referencing of variable ");
Append_Name (E_Str => E_Str,
Name => Err_Num.Name1,
Scope => Err_Num.Scope);
E_Strings.Append_String
(E_Str => E_Str,
Str => " by a task or interrupt handler has been omitted from the partition annotation");
--! This message is only issued when processing the partition annotation. The partition annotation
--! must describe all the actions of the tasks and interrupt handlers making up the program. Therefore,
--! if a variable is imported somewhere in the program by a task or interrupt handler, then it must
--! also be an import at the partition level. As well as the omission of explicit imports, this message is also
--! generated if the implicit imports of tasks and interrupt handlers are omitted. For tasks this means
--! any variable the task suspends on and for interrupt handlers it means the name of the protected
--! object containing the handler or, if given, the name of the interrupt stream associated with the
--! handler.
when ErrorHandler.Updated_But_Not_In_Partition =>
--! <Name> 37
E_Strings.Append_String (E_Str => E_Str,
Str => "The updating of variable ");
Append_Name (E_Str => E_Str,
Name => Err_Num.Name1,
Scope => Err_Num.Scope);
E_Strings.Append_String
(E_Str => E_Str,
Str => " by a task or interrupt handler has been omitted from the partition annotation");
--! This message is only issued when processing the partition annotation. The partition annotation
--! must describe all the actions of the tasks and interrupt handlers making up the program. Therefore,
--! if a variable is exported somewhere in the program by a task or interrupt handler, then it must
--! also be an export at the partition level.
when ErrorHandler.Uninitialized_Protected_Element =>
--! <Name> 38
E_Strings.Append_String (E_Str => E_Str,
Str => "The protected element ");
Append_Name (E_Str => E_Str,
Name => Err_Num.Name1,
Scope => Err_Num.Scope);
E_Strings.Append_String (E_Str => E_Str,
Str => " must be initialized at its point of declaration");
--! To avoid potential race conditions during program startup, all
--! elements of a protected type must be initialized with a constant value
--! at the point of declaration.
end case;
Append_Explanation;
E_Strings.Append_String (E_Str => E_Str,
Str => ".");
end UsageError;
|
