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 => "devread";
   
end FILO.Blockdev;