Introduce Blockdev_Length/_Offset
diff --git a/src/filo-blockdev.adb b/src/filo-blockdev.adb
index 28747e7..ba7bc6d 100644
--- a/src/filo-blockdev.adb
+++ b/src/filo-blockdev.adb
@@ -2,7 +2,7 @@
procedure Read
(Buffer : in out Buffer_Type;
- Offset : in Natural;
+ Offset : in Blockdev_Offset;
Success : out Boolean)
is
use Interfaces.C;
diff --git a/src/filo-blockdev.ads b/src/filo-blockdev.ads
index d35eef3..2fde36a 100644
--- a/src/filo-blockdev.ads
+++ b/src/filo-blockdev.ads
@@ -5,8 +5,10 @@
Procedure Read
(Buffer : in out Buffer_Type;
- Offset : in Natural;
- Success : out Boolean);
+ Offset : in Blockdev_Offset;
+ Success : out Boolean)
+ with
+ Pre => Offset <= Blockdev_Length'Last - Buffer'Length;
private
diff --git a/src/filo.ads b/src/filo.ads
index c0a7e3d..93985b1 100644
--- a/src/filo.ads
+++ b/src/filo.ads
@@ -4,8 +4,10 @@
package FILO is
- type Partition_Length is range 0 .. Interfaces.Unsigned_64'Last;
- subtype Partition_Offset is Partition_Length range 0 .. Partition_Length'Last - 1;
+ type Blockdev_Length is range 0 .. Interfaces.Unsigned_64'Last;
+ subtype Blockdev_Offset is Blockdev_Length range 0 .. Blockdev_Length'Last - 1;
+ subtype Partition_Length is Blockdev_Length;
+ subtype Partition_Offset is Blockdev_Offset;
BLOCK_SIZE : constant := 512;
type Block_Offset is range 0 .. Partition_Offset'Last / BLOCK_SIZE;