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
|
-------------------------------------------------------------------------------
-- (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 StabilityError (Err_Num : in Error_Types.NumericError;
With_Explanation : in Boolean;
E_Str : in out E_Strings.T) is
Stab_Index : ErrorHandler.Index_Type;
Stab_Typ : ErrorHandler.Stability_Err_Type;
procedure StabilityErrorExpl (E_Str : in out E_Strings.T)
--# global in Stab_Typ;
--# derives E_Str from *,
--# Stab_Typ;
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 Stab_Typ;
--# in With_Explanation;
--# in out E_Str;
--# derives E_Str from *,
--# Stab_Typ,
--# 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
StabilityErrorExpl (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
Stab_Index := ErrorHandler.Index_Type'Val (Err_Num.Name1.Pos);
Stab_Typ := ErrorHandler.Stability_Err_Type'Val (Err_Num.ErrorNum - Error_Types.StabilityErrOffset);
case Stab_Typ is
-- HTML Directives
--! <NameFormat> <"flow-"><Name>
--! <ErrorFormat> <"!!! Flow Error : "><Name><" : "><Error>
when ErrorHandler.Stable_Exit_Cond =>
--! <Name> 40
E_Strings.Append_String (E_Str => E_Str,
Str => "Exit condition is stable, of index");
--! <Error> Exit condition is stable, of index 0
--! <Error2> Exit condition is stable, of index 1
--! <Error3> Exit condition is stable, of index greater than 1
--! In these cases the (loop) exit condition occurs in an iteration scheme,
--! an exit statement, or an if-statement whose (unique) sequence of
--! statements ends with an unconditional exit statement - see the SPARK
--! Definition. The concept of loop stability is explained in Section
--! 4.4 of Appendix A. A loop exit condition which is stable of index 0
--! takes the same value at every iteration around the loop, and with a
--! stability index of 1, it always takes the same value after the first
--! iteration. Stability with indices greater
--! than 0 does not necessarily indicate a program error, but the
--! conditions for loop termination require careful consideration
when ErrorHandler.Stable_Fork_Cond =>
--! <Name> 41
E_Strings.Append_String (E_Str => E_Str,
Str => "Expression is stable, of index");
--! <Error> Expression is stable, of index 0
--! <Error2> Expression is stable, of index 1
--! <Error3> Expression is stable, of index greater than 1
--! The expression, occurring within a loop, is either a case expression
--! or a condition (Boolean-valued expression) associated with an
--! if-statement, whose value determines the path taken through the body
--! of the loop, but does not (directly) cause loop termination.
--! Information flow analysis shows that the expression does not vary
--! as the loop is executed, so the same branch of the case or if statement will
--! be taken on every loop iteration. An Index of 0 means that the expression is
--! immediately stable, 1 means it becomes stable after the first pass through the loop and so on.
--! The stability index is given with reference to the loop most
--! closely-containing the expression. Stable conditionals are not necessarily
--! an error but do require careful evaluation; they can often be removed by lifting them
--! outside the loop.
end case;
case Stab_Index is
when ErrorHandler.Index_Zero =>
E_Strings.Append_String (E_Str => E_Str,
Str => " 0");
when ErrorHandler.Index_One =>
E_Strings.Append_String (E_Str => E_Str,
Str => " 1");
when ErrorHandler.Larger_Index =>
E_Strings.Append_String (E_Str => E_Str,
Str => " greater than 1");
end case;
Append_Explanation;
E_Strings.Append_String (E_Str => E_Str,
Str => ".");
end StabilityError;
|
