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
|
separate (ErrorHandler.Conversions.ToString.WarningWithoutPosition)
procedure WarningWithoutPositionExpl (E_Str : in out E_Strings.T)
is
begin
case Err_Num.ErrorNum is
when 9 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "Issued when a --# hide XXX annotation is used to hide a user-defined exception handler. (warning control file" &
" keyword: handler_parts)");
when 10 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "Issued when a --# hide XXX annotation is used. (warning control file keyword: hidden_parts)");
when 400 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "Issued when a variable declared in a subprogram is neither" &
" referenced, nor updated." &
" (warning control file keyword: unused_variables)");
when 402 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "In order to prove properties of code containing loops, the" &
" loop must be ""cut"" with" &
" a suitable assertion statement. When generating run-time checks," &
" the Examiner" &
" inserts a simple assertion to cut any loops which do not have one" &
" supplied" &
" by the user. The assertion is placed at the point where this" &
" warning appears in" &
" the listing file. The default assertion asserts that the" &
" subprogram's precondition" &
" (if any) is satisfied, that all imports to it are in their" &
" subtypes and that any for" &
" loop counter is in its subtype. In many cases this provides" &
" sufficient information" &
" to complete a proof of absence of run-time errors. If more" &
" information is required," &
" then the user can supply an assertion and the Examiner will" &
" append the above information" &
" to it. (warning control file keyword: default_loop_assertions)");
when 403 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "XXX is a variable which was initialized at declaration but" &
" whose value is only ever" &
" read not updated; it could therefore have been declared as" &
" a constant. (warning control" &
" file keyword: constant_variables)");
when 405 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "The Examiner generates VCs associated with" &
" real numbers using perfect arithmetic rather than the machine" &
" approximations used on the" &
" target platform. It is possible that rounding errors might" &
" cause a Constraint_Error even" &
" if these run-time check proofs are completed satisfactorily." &
" (warning control file keyword: real_rtcs)");
when 406 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "This message is echoed to the screen if the Examiner is unable" &
" to create output files for the VCs being generated" &
" (for instance, if the user does not have write" &
" permission for the output directory).");
when 407 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "Issued where SPARK own variable and initialization annotations" &
" make it clear that a" &
" package requires a body but where no Ada requirement for a body" &
" exists.");
when 408 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "Semantic errors prevent VC Generation, so a single False VC" &
" is produced. This will be detected and reported by POGS.");
when 409 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "A subprogram which has excessive complexity of data structure" &
" or number of paths may cause the VC Generator to exceed its capacity." &
" A single False VC is generated in this case to make sure this" &
" error is detected in subsequent proof and analysis with POGS");
when 410 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "Partition-wide flow analysis is performed by checking all" &
" packages withed by the main program for" &
" tasks and interrupt handlers and constructing an overall flow" &
" relation that captures their cumulative" &
" effect. It is for this reason that SPARK requires task and" &
" protected types to be declared in package" &
" specifications. If a task or protected type which contains" &
" an interrupt handler, is hidden from the" &
" Examiner (in a hidden package private part) or contains errors" &
" in it specification, the partition-wide" &
" flow analysis cannot be" &
" constructed correctly and is therefore suppressed. Correct the" &
" specification of the affected tasks" &
" and (temporarily if desired) make them visible to the Examiner.");
when 411 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "The Examiner checks that there is no potential sharing of" &
" unprotected data between tasks. If a task type" &
" is hidden from the Examiner in a hidden package private" &
" part, then it is not possible to check whether that" &
" task may share unprotected data.");
when 412 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "The Examiner checks that no more than one task can suspend on" &
" a single object. If a task" &
" is hidden from the Examiner in a hidden package private part," &
" then it is not possible to check whether that" &
" task may suspend on the same object as another task.");
when 413 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "The Examiner checks that no more than one task can suspend on a" &
" single object and that there is no" &
" potential sharing of unprotected data between tasks. These checks" &
" depend on the accuracy of the annotations" &
" on the task types withed by the main program. If these annotations" &
" contain errors, then any reported" &
" violations of the shared variable and max-one-in-a-queue checks will" &
" be correct; however, the check" &
" may be incomplete. The errors in the task annotations should be corrected.");
when 414 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "Raised if an output file name is longer than the" &
" limit imposed by the operating system and has been truncated." &
" Section 4.7 of the Examiner User Manual describes how the output file names" &
" are constructed. If this message is seen there is a possibility" &
" that the output from two" &
" or more subprograms will be written to the same file name," &
" if they have a sufficiently large number of characters in common.");
when 420 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "In release 7.5 of the Examiner, a flaw in the VC generation" &
" was fixed such that subcomponents of records and elements of" &
" arrays when used as ""out"" or ""in out""" &
" parameters will now generate an" &
" additional VC to verify absence of run-time errors. This warning" &
" flags an instance of this occurrence. Please read the release" &
" note and/or seek advice for assistance with this issue.");
when 425 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "A code generator language profile such as KCG is in use" &
" and so conditional flow errors may be present in the subprogram." &
" Therefore the -vcg switch must be used to generate VCs and the VCs" &
" related to definedness discharged using the proof tools.");
when 426 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "A code generator language profile such as KCG allows a package body to" &
" with its own public child which is not normally permitted in SPARK." &
" The removal of this restriction means that the Examiner will not" &
" detect mutual recursion between subprograms declared in the visible" &
" parts of the package and its child. The code generator is expected" &
" to guarantee the absence of recursion.");
when 495 =>
E_Strings.Append_String
(E_Str => E_Str,
Str => "There is little that can be done to work around this as this" &
" is a fundamental limitation of Windows. You could try one of the" &
" following: Perform analysis higher up in the directory tree (i.e." &
" in C:\a instead of C:\project_name\spark\analysis). You could try" &
" remapping a directory to a new drive to do the same (google for subst)." &
" You could try renaming or restructuring your program to flatten the" &
" structure a bit. And finally you can perform analysis on a UNIX system" &
" such as Mac OSX or GNU/Linux as they do not suffer from this problem.");
when others => null;
end case;
end WarningWithoutPositionExpl;
|
