Nico Huber | 8ec45a1 | 2023-12-04 17:11:08 +0100 | [diff] [blame^] | 1 | with System; |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 2 | with Interfaces; |
Nico Huber | 8ec45a1 | 2023-12-04 17:11:08 +0100 | [diff] [blame^] | 3 | with Interfaces.C; |
| 4 | with Interfaces.C.Strings; |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 5 | |
| 6 | with FS.FILO.Dev; |
Nico Huber | 8ec45a1 | 2023-12-04 17:11:08 +0100 | [diff] [blame^] | 7 | with FS.FILO.VFS; |
| 8 | |
| 9 | use Interfaces.C; |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 10 | |
| 11 | package body FS.FILO.Ext2 is |
| 12 | |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 13 | function Is_Mounted (State : T) return Boolean is (State.S >= Mounted); |
| 14 | function Is_Open (State : T) return Boolean is (State.S = File_Opened); |
| 15 | |
| 16 | procedure Mount |
| 17 | (State : in out T; |
| 18 | Part_Len : in Partition_Length; |
| 19 | Success : out Boolean) |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 20 | is |
| 21 | begin |
| 22 | Success := False; |
| 23 | end Mount; |
| 24 | |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 25 | procedure Open |
| 26 | (State : in out T; |
| 27 | File_Len : out File_Length; |
| 28 | File_Path : in String; |
| 29 | Success : out Boolean) |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 30 | is |
| 31 | begin |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 32 | File_Len := 0; |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 33 | Success := False; |
| 34 | end Open; |
| 35 | |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 36 | procedure Close (State : in out T) is |
| 37 | begin |
| 38 | State.S := Mounted; |
| 39 | end Close; |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 40 | |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 41 | procedure Read |
| 42 | (State : in out T; |
| 43 | File_Len : in File_Length; |
| 44 | File_Pos : in out File_Offset; |
| 45 | Buf : out Buffer_Type; |
| 46 | Len : out Natural) |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 47 | is |
| 48 | begin |
Nico Huber | 57d3a85 | 2023-12-04 15:42:40 +0100 | [diff] [blame] | 49 | Buf := (others => 0); |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 50 | Len := 0; |
| 51 | end Read; |
| 52 | |
Nico Huber | 8ec45a1 | 2023-12-04 17:11:08 +0100 | [diff] [blame^] | 53 | package C is new VFS (T => T, Initial => (S => Unmounted)); |
| 54 | |
| 55 | function C_Mount return int |
| 56 | with |
| 57 | Export, |
| 58 | Convention => C, |
| 59 | External_Name => "ext2fs_mount"; |
| 60 | function C_Mount return int |
| 61 | with |
| 62 | SPARK_Mode => Off |
| 63 | is |
| 64 | begin |
| 65 | return C.C_Mount; |
| 66 | end C_Mount; |
| 67 | |
| 68 | function C_Open (File_Path : Strings.chars_ptr) return int |
| 69 | with |
| 70 | Export, |
| 71 | Convention => C, |
| 72 | External_Name => "ext2fs_dir"; |
| 73 | function C_Open (File_Path : Strings.chars_ptr) return int |
| 74 | with |
| 75 | SPARK_Mode => Off |
| 76 | is |
| 77 | begin |
| 78 | return C.C_Open (File_Path); |
| 79 | end C_Open; |
| 80 | |
| 81 | function C_Read (Buf : System.Address; Len : int) return int |
| 82 | with |
| 83 | Export, |
| 84 | Convention => C, |
| 85 | External_Name => "ext2fs_read"; |
| 86 | function C_Read (Buf : System.Address; Len : int) return int |
| 87 | with |
| 88 | SPARK_Mode => Off |
| 89 | is |
| 90 | begin |
| 91 | return C.C_Read (Buf, Len); |
| 92 | end C_Read; |
| 93 | |
Nico Huber | 1d7727f | 2023-11-30 15:58:46 +0100 | [diff] [blame] | 94 | end FS.FILO.Ext2; |