ext2: Adapt to satisfy some checks
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 5f28c83..3dbbb2b 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -89,9 +89,7 @@
declare
S_Inode_Size : constant Unsigned_16 := Read_LE16 (Super_Block, 22 * 4);
begin
- if S_Inode_Size in
- Unsigned_16 (Inode_Size'First) .. Unsigned_16 (Inode_Size'Last)
- then
+ if Natural (S_Inode_Size) in Inode_Size then
State.Inode_Size := Inode_Size (S_Inode_Size);
else
Success := False;
@@ -222,7 +220,7 @@
Double_Indirect : Unsigned_32;
Triple_Indirect : Unsigned_32;
end record
- with Size => Inode_Extents'Length * 8;
+ with Object_Size => Inode_Extents'Length * 8;
function I_Blocks is new Ada.Unchecked_Conversion (Inode_Extents, Inode_Blocks);
function I_Blocks (State : T) return Inode_Blocks is (I_Blocks (State.Inode.Inline));
@@ -239,7 +237,9 @@
Next_Physical : out FSBlock_Offset;
Success : out Boolean)
with
- Pre => FSBlock_Logical (Addr_In_Block) < Addr_Per_Block
+ Pre =>
+ Addr_Per_Block = FSBlock_Logical (State.Block_Size / 4) and
+ FSBlock_Logical (Addr_In_Block) < Addr_Per_Block
is
Cache_Start, Cache_End : Max_Block_Index;
begin
@@ -257,6 +257,8 @@
end Indirect_Block_Lookup;
Logical_Rest : FSBlock_Logical := Logical;
+
+ pragma Assert (Addr_Per_Block <= 2 ** 14);
begin
if Logical_Rest < Direct_Blocks then
Physical := FSBlock_Offset (I_Blocks (State).Direct_Blocks (Natural (Logical)));
@@ -280,7 +282,7 @@
if Logical_Rest < Addr_Per_Block ** 2 then
Indirect_Block_Lookup
(Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Double_Indirect),
- Addr_In_Block => Addr_In_Block_Range (Logical_Rest / Addr_Per_Block),
+ Addr_In_Block => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block) mod Addr_Per_Block),
Level => 1,
Logical_Off => Logical - Logical_Rest,
Next_Physical => Physical,
@@ -303,7 +305,7 @@
if Logical_Rest < Addr_Per_Block ** 3 then
Indirect_Block_Lookup
(Indirect_Block_Phys => FSBlock_Offset (I_Blocks (State).Triple_Indirect),
- Addr_In_Block => Addr_In_Block_Range (Logical_Rest / Addr_Per_Block ** 2),
+ Addr_In_Block => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block ** 2) mod Addr_Per_Block),
Level => 2,
Logical_Off => Logical - Logical_Rest,
Next_Physical => Physical,
@@ -314,7 +316,7 @@
Indirect_Block_Lookup
(Indirect_Block_Phys => Physical,
- Addr_In_Block => Addr_In_Block_Range (Logical_Rest / Addr_Per_Block mod Addr_Per_Block),
+ Addr_In_Block => Addr_In_Block_Range ((Logical_Rest / Addr_Per_Block) mod Addr_Per_Block),
Level => 1,
Logical_Off => Logical - (Logical_Rest mod Addr_Per_Block ** 2),
Next_Physical => Physical,
@@ -334,6 +336,7 @@
end if;
-- Logical address was just too high.
+ Physical := 0;
Success := False;
end Ext2_Block_Map;
diff --git a/src/filo-fs-ext2.ads b/src/filo-fs-ext2.ads
index ba47aef..a13b153 100644
--- a/src/filo-fs-ext2.ads
+++ b/src/filo-fs-ext2.ads
@@ -48,9 +48,10 @@
subtype Block_Size is Natural range 2 ** Log_Block_Size'First .. 2 ** Log_Block_Size'Last;
subtype Max_Block_Index is Index_Type range 0 .. 2 ** Log_Block_Size'Last - 1;
- -- Minimum ext2 block size is 1KiB (two 512B blocks)
- type FSBlock_Offset is new Block_Offset range 0 .. Block_Offset'Last / 2;
- type FSBlock_Logical is new Block_Offset range 0 .. Block_Offset'Last / 2;
+ -- Extent physical addresses are 48 bits.
+ type FSBlock_Offset is new Block_Offset range 0 .. 2 ** 48 - 1;
+ -- Logical block addresses are 32 bits.
+ type FSBlock_Logical is new Block_Offset range 0 .. 2 ** 32 - 1;
-- We use a 64KiB cache which fits at least one ext2 block. If a lower
-- block size is encountered (likely), we partition the cache into up
@@ -65,7 +66,9 @@
-- Same as the 12 direct + 3 indirect blocks times 4B:
subtype Inode_Extents_Index is Natural range 0 .. 59;
- subtype Inode_Extents is Buffer_Type (Inode_Extents_Index);
+ subtype Inode_Extents is Buffer_Type (Inode_Extents_Index)
+ with
+ Object_Size => (Inode_Extents_Index'Last + 1) * 8;
type Inode_Index is new Unsigned_32 range 2 .. Unsigned_32'Last;
subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last);
@@ -79,7 +82,7 @@
Mode : Inode_Type := Inode_Type'First;
Size : Inode_Length := 0;
Use_Extents : Boolean := False;
- Inline : Buffer_Type (Inode_Extents_Index) := (others => 16#00#);
+ Inline : Inode_Extents := (others => 16#00#);
end record;
type T is record