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 | ------------------------------------------------------------------
-- Tokeneer ID Station Core Software
--
-- Copyright (2003) United States Government, as represented
-- by the Director, National Security Agency. All rights reserved.
--
-- This material was originally developed by Praxis High Integrity
-- Systems Ltd. under contract to the National Security Agency.
------------------------------------------------------------------
------------------------------------------------------------------
-- Floppy
--
-- Implementation Notes:
-- Uses WIN32 so is not SPARK.
--
------------------------------------------------------------------
with Ada.Text_IO;
with System;
with Interfaces.C;
use type System.Address;
use type Interfaces.C.Size_T;
package body Floppy
with SPARK_Mode => Off
is
OFS_MAXPATHNAME : constant := 4096;
subtype FilePathNameT is
Interfaces.C.Char_Array( 0 .. OFS_MAXPATHNAME + 1);
subtype FileNameStringT is String (1 .. 256);
------------------------------------------------------------------
-- State
--
------------------------------------------------------------------
CurrentFile : File.T := File.NullFile;
WrittenFile : File.T := File.NullFile;
TempDir : constant String := "Temp";
FloppyDrive : String( 1 .. 2) := "A:";
CurrentName : String := "current.txt";
WrittenName : String := "written.log";
------------------------------------------------------------------
-- FileAndPathName
--
-- Description:
-- Prepends a path to a file name.
--
-- Implementation Notes:
-- None.
------------------------------------------------------------------
function FilePathAndName(Path : in String;
Name : in String) return Interfaces.C.Char_Array
is
FullName : String := Path & "\" & Name;
begin
return Interfaces.C.To_C(FullName);
end FilePathAndName;
------------------------------------------------------------------
-- IsPresent
--
-- Implementation Notes:
-- None.
------------------------------------------------------------------
function IsPresent return Boolean is (True);
------------------------------------------------------------------
-- Write
--
-- Implementation Notes:
-- None.
------------------------------------------------------------------
procedure Write (TheFile : in File.T)
is
begin
null;
end Write;
------------------------------------------------------------------
-- Read
--
-- Implementation Notes:
-- None.
------------------------------------------------------------------
procedure Read
is
begin
null;
end Read;
------------------------------------------------------------------
-- CheckWrite
--
-- Implementation Notes:
-- None.
------------------------------------------------------------------
procedure CheckWrite (WriteOK : out Boolean)
is
begin
WriteOK := True;
end CheckWrite;
------------------------------------------------------------------
-- CurrentFloppy
--
-- Implementation Notes:
-- None.
------------------------------------------------------------------
function CurrentFloppy return File.T is (CurrentFile);
------------------------------------------------------------------
-- Init
--
-- Implementation Notes:
-- Creates the Temp Directory if it doesn't exist.
------------------------------------------------------------------
procedure Init
is
---------------------------------------------------------
-- begin Init
---------------------------------------------------------
begin
null;
end Init;
end Floppy;
|