| Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 1 | package FS.FILO.Ext2 is |
| 2 | |
| 3 | Sane_And_Mounted : Boolean with Ghost; -- TODO: track what FS type is mounted in FS.FILO |
| 4 | |
| 5 | procedure Mount (Success : out Boolean) |
| 6 | with |
| 7 | Post => (if Success then Sane_And_Mounted); |
| 8 | |
| 9 | procedure Open (File_Path : String; Success : out Boolean) |
| 10 | with |
| 11 | Pre => Sane_And_Mounted; |
| 12 | procedure Close |
| 13 | with |
| 14 | Convention => C, |
| 15 | Pre => Sane_And_Mounted; |
| 16 | |
| 17 | procedure Read (Buf : out Buffer_Type; Len : out Natural) |
| 18 | with |
| 19 | Pre => Sane_And_Mounted; |
| 20 | |
| 21 | end FS.FILO.Ext2; |