Thomas Heijligen | a6d6315 | 2024-01-29 13:43:40 +0000 | [diff] [blame] | 1 | with FILO.Blockdev; |
| 2 | |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 3 | package body FILO.FS.NullFS is |
| 4 | |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 5 | function To_Int (Success : Boolean) return Interfaces.C.int is |
| 6 | (if Success then 1 else 0); |
| 7 | |
Thomas Heijligen | a6d6315 | 2024-01-29 13:43:40 +0000 | [diff] [blame] | 8 | function C_Mount return Interfaces.C.int is |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 9 | begin |
Thomas Heijligen | a6d6315 | 2024-01-29 13:43:40 +0000 | [diff] [blame] | 10 | return To_Int (True); |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 11 | end C_Mount; |
| 12 | |
| 13 | function C_Read |
| 14 | (buf : System.Address; |
| 15 | len : Interfaces.C.int) |
| 16 | return Interfaces.C.int |
| 17 | with SPARK_Mode => Off |
| 18 | is |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 19 | Buffer : Buffer_Type (0 .. Integer(len) - 1) with Address => buf; |
Thomas Heijligen | a6d6315 | 2024-01-29 13:43:40 +0000 | [diff] [blame] | 20 | Offset : constant Blockdev_Offset := Blockdev_Offset(File_Pos); |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 21 | Success : Boolean; |
| 22 | begin |
Thomas Heijligen | a6d6315 | 2024-01-29 13:43:40 +0000 | [diff] [blame] | 23 | FILO.Blockdev.Read (Buffer, Offset, Success); |
| 24 | return To_Int (Success); |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 25 | end C_Read; |
| 26 | |
Thomas Heijligen | a6d6315 | 2024-01-29 13:43:40 +0000 | [diff] [blame] | 27 | |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 28 | function C_Dir |
Thomas Heijligen | a6d6315 | 2024-01-29 13:43:40 +0000 | [diff] [blame] | 29 | (Path : System.Address) |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 30 | return Interfaces.C.int |
| 31 | with SPARK_Mode => Off |
| 32 | is |
Thomas Heijligen | a6d6315 | 2024-01-29 13:43:40 +0000 | [diff] [blame] | 33 | First_Byte : Unsigned_8 with Address => Path; |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 34 | begin |
Thomas Heijligen | a6d6315 | 2024-01-29 13:43:40 +0000 | [diff] [blame] | 35 | if First_Byte = 0 then |
| 36 | return To_Int (True); |
| 37 | end if; |
| 38 | return To_Int (False); |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 39 | end C_Dir; |
| 40 | |
Thomas Heijligen | 5182037 | 2023-12-11 15:29:17 +0000 | [diff] [blame] | 41 | end FILO.FS.NullFS; |