package FS.FILO.Ext2 is | |
Sane_And_Mounted : Boolean with Ghost; -- TODO: track what FS type is mounted in FS.FILO | |
procedure Mount (Success : out Boolean) | |
with | |
Post => (if Success then Sane_And_Mounted); | |
procedure Open (File_Path : String; Success : out Boolean) | |
with | |
Pre => Sane_And_Mounted; | |
procedure Close | |
with | |
Convention => C, | |
Pre => Sane_And_Mounted; | |
procedure Read (Buf : out Buffer_Type; Len : out Natural) | |
with | |
Pre => Sane_And_Mounted; | |
end FS.FILO.Ext2; |