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
|
-------------------------------------------------------------------------------
-- (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.
--
--=============================================================================
--------------------------------------------------------------------------------
-- This package implements files of Error Entries either using the standard --
-- mechanisms of SPARK_IO (as in Examiners up to and including release 5) --
-- or building them entirely in-memory as an option for future Examiners on --
-- hosts where sufficient memory (or insufficient file handles) are available --
-- --
-- The "In_Memory" implementation assumes the host compiler is GNAT, and uses --
-- the GNAT.Dynamic_Tables package --
-- --
-- Following Examiner 7.6, we assume the host compiler is always GNAT and --
-- that error files will always be built in memory, so the "On_Disk" --
-- implementation has been removed. As such, this file no longer needs to --
-- be passed through GNATPREP --
--------------------------------------------------------------------------------
with GNAT.Dynamic_Tables;
package body Error_IO is
--# hide Error_IO;
package NumericError_Tables is new GNAT.Dynamic_Tables (
Error_Types.NumericError,
Positive,
Positive'First,
100, -- elements
100); -- % increase when reallocated
type File_Descriptor is record
T : NumericError_Tables.Instance;
Top : Natural; -- Length of file in records
Ptr : Positive; -- Current file pointer
end record;
procedure Close (File : in out File_Type;
Status : out SPARK_IO.File_Status) is
begin
Status := SPARK_IO.Ok;
NumericError_Tables.Set_Last (File.T, Positive'First);
NumericError_Tables.Release (File.T);
File.Top := 0;
File.Ptr := 1;
exception
when others =>
Status := SPARK_IO.Device_Error;
end Close;
------------
-- Create --
------------
procedure Create (File : in out File_Type;
Status : out SPARK_IO.File_Status) is
begin
Status := SPARK_IO.Ok;
File := new File_Descriptor;
NumericError_Tables.Init (File.T);
File.Top := 0;
File.Ptr := 1;
exception
when others =>
Status := SPARK_IO.Device_Error;
end Create;
---------------------
-- Get_Numeric_Error --
---------------------
procedure Get_Numeric_Error (File : in File_Type;
Item : out Error_Types.NumericError) is
begin
if File.Ptr <= File.Top then
Item := File.T.Table (File.Ptr);
File.Ptr := File.Ptr + 1;
else
Item := Error_Types.Empty_NumericError;
end if;
end Get_Numeric_Error;
---------------------
-- Put_Numeric_Error --
---------------------
procedure Put_Numeric_Error (File : in File_Type;
Item : in Error_Types.NumericError) is
begin
NumericError_Tables.Allocate (File.T, 1);
File.T.Table (File.Ptr) := Item;
File.Ptr := File.Ptr + 1;
File.Top := File.Top + 1;
end Put_Numeric_Error;
-----------
-- Reset --
-----------
procedure Reset (File : in out File_Type;
Mode_Of_File : in SPARK_IO.File_Mode;
Status : out SPARK_IO.File_Status) is
pragma Unreferenced (Mode_Of_File);
begin
Status := SPARK_IO.Ok;
if File /= Null_File then
File.Ptr := 1;
end if;
end Reset;
end Error_IO;
|
