FS.FILO.Ext2: Update stubs
diff --git a/src/fs-filo-ext2.adb b/src/fs-filo-ext2.adb
index df8525f..730cd11 100644
--- a/src/fs-filo-ext2.adb
+++ b/src/fs-filo-ext2.adb
@@ -4,24 +4,43 @@
package body FS.FILO.Ext2 is
- procedure Mount (Success : out Boolean)
+ function Is_Mounted (State : T) return Boolean is (State.S >= Mounted);
+ function Is_Open (State : T) return Boolean is (State.S = File_Opened);
+
+ procedure Mount
+ (State : in out T;
+ Part_Len : in Partition_Length;
+ Success : out Boolean)
is
begin
Success := False;
end Mount;
- procedure Open (File_Path : String; Success : out Boolean)
+ procedure Open
+ (State : in out T;
+ File_Len : out File_Length;
+ File_Path : in String;
+ Success : out Boolean)
is
begin
+ File_Len := 0;
Success := False;
end Open;
- procedure Close is null;
+ procedure Close (State : in out T) is
+ begin
+ State.S := Mounted;
+ end Close;
- procedure Read (Buf : out Buffer_Type; Len : out Natural)
+ procedure Read
+ (State : in out T;
+ File_Len : in File_Length;
+ File_Pos : in out File_Offset;
+ Buf : out Buffer_Type;
+ Len : out Natural)
is
begin
- Buf := (others => 16#00#);
+ Buf := (others => 0);
Len := 0;
end Read;
diff --git a/src/fs-filo-ext2.ads b/src/fs-filo-ext2.ads
index d19a00f..d8cc7e9 100644
--- a/src/fs-filo-ext2.ads
+++ b/src/fs-filo-ext2.ads
@@ -1,21 +1,49 @@
package FS.FILO.Ext2 is
- Sane_And_Mounted : Boolean with Ghost; -- TODO: track what FS type is mounted in FS.FILO
+ type T is private;
- procedure Mount (Success : out Boolean)
+ function Is_Mounted (State : T) return Boolean;
+ function Is_Open (State : T) return Boolean
with
- Post => (if Success then Sane_And_Mounted);
+ Post => (if Is_Open'Result then Is_Mounted (State));
- procedure Open (File_Path : String; Success : out Boolean)
+ procedure Mount
+ (State : in out T;
+ Part_Len : in Partition_Length;
+ Success : out Boolean)
with
- Pre => Sane_And_Mounted;
- procedure Close
- with
- Convention => C,
- Pre => Sane_And_Mounted;
+ Pre => not Is_Mounted (State),
+ Post => Success = Is_Mounted (State);
- procedure Read (Buf : out Buffer_Type; Len : out Natural)
+ procedure Open
+ (State : in out T;
+ File_Len : out File_Length;
+ File_Path : in String;
+ Success : out Boolean)
with
- Pre => Sane_And_Mounted;
+ Pre => Is_Mounted (State) and not Is_Open (State),
+ Post => Success = Is_Open (State);
+
+ procedure Close (State : in out T)
+ with
+ Pre => Is_Open (State),
+ Post => Is_Mounted (State);
+
+ procedure Read
+ (State : in out T;
+ File_Len : in File_Length;
+ File_Pos : in out File_Offset;
+ Buf : out Buffer_Type;
+ Len : out Natural)
+ with
+ Pre => Is_Open (State),
+ Post => Is_Open (State);
+
+private
+ type State is (Unmounted, Mounted, File_Opened);
+
+ type T is record
+ S : State;
+ end record;
end FS.FILO.Ext2;