Make VFS wrapper state aware
diff --git a/src/fs-filo-vfs.ads b/src/fs-filo-vfs.ads
index 6115554..2b6dd52 100644
--- a/src/fs-filo-vfs.ads
+++ b/src/fs-filo-vfs.ads
@@ -6,19 +6,53 @@
generic
- with procedure Mount (Success : out Boolean);
+ type T (<>) is private;
- with procedure Open (File_Path : String; Success : out Boolean);
- with procedure Close with Convention => C;
+ with function Is_Mounted (State : T) return Boolean;
+ with function Is_Open (State : T) return Boolean
+ with
+ Post => (if Is_Open'Result then Is_Mounted (State));
- with procedure Read (Buf : out Buffer_Type; Len : out Natural);
+ Initial : T;
+
+ with procedure Mount
+ (State : in out T;
+ Part_Len : in Partition_Length;
+ Success : out Boolean)
+ with
+ Pre => not Is_Mounted (State),
+ Post => Success = Is_Mounted (State);
+
+ with procedure Open
+ (State : in out T;
+ File_Len : out File_Length;
+ File_Path : in String;
+ Success : out Boolean)
+ with
+ Pre => Is_Mounted (State) and not Is_Open (State),
+ Post => Success = Is_Open (State);
+
+ with procedure Close (State : in out T)
+ with
+ Pre => Is_Open (State),
+ Post => Is_Mounted (State);
+
+ with 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);
package FS.FILO.VFS is
function C_Mount return int;
function C_Open (File_Path : Strings.chars_ptr) return int;
- procedure C_Close renames Close;
+ procedure C_Close;
function C_Read (Buf : System.Address; Len : int) return int;