| with Interfaces.C; |
| with System; |
| |
| package FILO.Blockdev is |
| |
| Procedure Read |
| (Buffer : out Buffer_Type; |
| Offset : in Blockdev_Offset; |
| Success : out Boolean) |
| with |
| Pre => Offset <= Blockdev_Length'Last - Buffer'Length; |
| |
| private |
| |
| function C_devread |
| (sector : Interfaces.C.unsigned_long; |
| byte_offset : Interfaces.C.unsigned_long; |
| byte_len : Interfaces.C.unsigned_long; |
| buf : System.Address) |
| return Interfaces.C.int |
| with |
| SPARK_Mode => Off, |
| Import => True, |
| Convention => C, |
| External_Name => "devopen"; |
| |
| end FILO.Blockdev; |