package body FILO.Blockdev is

   procedure Read
      (Buffer  :    out Buffer_Type;
       Offset  : in     Blockdev_Offset;
       Success :    out Boolean)
   with
      SPARK_Mode => Off
   is
      use Interfaces.C;

      Sector      : constant unsigned_long  := unsigned_long (Offset / BLOCK_SIZE);
      Byte_Offset : constant unsigned_long  := unsigned_long (Offset rem BLOCK_SIZE);
      Byte_Len    : constant unsigned_long  := unsigned_long (Buffer'Length);
      Buf         : constant System.Address := Buffer'Address;

      -- NOTE: C_devread returns 1 on success
      function To_Success (Item : Interfaces.C.int) return Boolean is
         (if Item = 1 then True else False);

   begin
      -- With 32-bit longs, the current C interface
      -- can't access more than 512 * 2 ** 32:
      pragma Warnings (GNAT, Off, "condition can only be True if");
      pragma Warnings (GNAT, Off, "condition is always False");
      if Unsigned_64 (Offset / BLOCK_SIZE) > Unsigned_64 (unsigned_long'last) then
         Success := False;
         return;
      end if;
      Success := To_Success (C_devread (Sector, Byte_Offset, Byte_Len, Buf));
   end Read;

end FILO.Blockdev;