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
|
-------------------------------------------------------------------------------
-- (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)
package body Conversions
--# own State is Explanation_Table,
--# Source_Used;
is
-------------------------------------------------------------------
type Sources is (
Nul,
LRM,
SR95,
SR83,
UM,
Proof_UM,
JB);
type Sources_Used is array (Sources) of Boolean;
No_Source_Used : constant Sources_Used := Sources_Used'(Sources => False);
Source_Used : Sources_Used := No_Source_Used;
-- construct table of flags used to note when an error explanation of a particular
-- kind, number and destination has been given.
type Purpose_Array is array (Error_Types.ConversionRequestSource) of Boolean;
Empty_Purpose_Array : constant Purpose_Array := Purpose_Array'(False, False, False, False);
type Error_Number_Array is array (Error_Types.ErrNumRange) of Purpose_Array;
Empty_Error_Number_Array : constant Error_Number_Array := Error_Number_Array'(Error_Types.ErrNumRange => Empty_Purpose_Array);
type Explanation_Classes is (
Flow_Errors,
Dependency_Errs,
Semantic_Errs,
Dep_Semantic_Errs,
Warnings,
Notes,
Control_Flows,
Ineffective_Statements);
type Explanation_Tables is array (Explanation_Classes) of Error_Number_Array;
Empty_Explanation_Table : constant Explanation_Tables := Explanation_Tables'(Explanation_Classes => Empty_Error_Number_Array);
-- giving us the actual table (and refinement constituent)
Explanation_Table : Explanation_Tables := Empty_Explanation_Table;
--------------------------------------------------------------------------
procedure ToString
(Err_Num : in Error_Types.NumericError;
Purpose : in Error_Types.ConversionRequestSource;
Err_Str : out Error_Types.StringError)
--# global in CommandLineData.Content;
--# in Dictionary.Dict;
--# in LexTokenManager.State;
--# in out Explanation_Table;
--# in out Source_Used;
--# derives Err_Str from CommandLineData.Content,
--# Dictionary.Dict,
--# Err_Num,
--# Explanation_Table,
--# LexTokenManager.State,
--# Purpose &
--# Explanation_Table from *,
--# CommandLineData.Content,
--# Err_Num,
--# Purpose &
--# Source_Used from *,
--# CommandLineData.Content,
--# Err_Num;
is separate;
--------------------------------------------------------------------------
procedure Output_Reference_List (To_File : in SPARK_IO.File_Type)
--# global in CommandLineData.Content;
--# in Source_Used;
--# in out SPARK_IO.File_Sys;
--# derives SPARK_IO.File_Sys from *,
--# CommandLineData.Content,
--# Source_Used,
--# To_File;
is
procedure Output_A_Reference (Source : in Sources;
To_File : in SPARK_IO.File_Type)
--# global in CommandLineData.Content;
--# in out SPARK_IO.File_Sys;
--# derives SPARK_IO.File_Sys from *,
--# CommandLineData.Content,
--# Source,
--# To_File;
is
begin
case Source is
when LRM =>
case CommandLineData.Content.Language_Profile is
when CommandLineData.SPARK83 =>
SPARK_IO.Put_Line (To_File, "Ada LRM: Ada Reference Manual (ANSI/MIL-STD-1815A-1983)", 0);
when CommandLineData.SPARK95 =>
SPARK_IO.Put_Line (To_File, "Ada LRM: Ada Reference Manual (ISO/IEC 8652:1995)", 0);
when CommandLineData.SPARK2005_Profiles =>
SPARK_IO.Put_Line (To_File, "Ada LRM: Ada 2005 Reference Manual (ISO/IEC 8652:1995/AMD.1:2007)", 0);
end case;
when SR83 =>
SPARK_IO.Put_Line (To_File, "SR: SPARK - The SPADE Ada83 Kernel", 0);
when SR95 =>
SPARK_IO.Put_Line (To_File, "SR: SPARK95 - The SPADE Ada Kernel (including RavenSPARK)", 0);
when UM =>
SPARK_IO.Put_Line (To_File, "User Manual: Examiner User Manual", 0);
when Proof_UM =>
SPARK_IO.Put_Line (To_File, "SPARK Proof Manual", 0);
when JB =>
SPARK_IO.Put_Line (To_File, "Barnes: High Integrity Software - The SPARK Approach", 0);
when others =>
SPARK_IO.Put_Line (To_File, "Unexpected reference table entry", 0);
end case;
end Output_A_Reference;
---------------------
begin --Output_Reference_List
for I in Sources range LRM .. Sources'Last loop
if Source_Used (I) then
SPARK_IO.New_Line (To_File, 2);
SPARK_IO.Put_Line (To_File, "References used:", 0);
for J in Sources range LRM .. Sources'Last loop
if Source_Used (J) then
Output_A_Reference (Source => J,
To_File => To_File);
end if;
end loop;
exit;
end if;
end loop;
end Output_Reference_List;
-- state initialized at declaration
end Conversions;
|
