gnatprove_11.2.3_f7ece6d3/share/examples/spark/tokeneer/floppy.adb

  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;