commit 5a042fd263a56df4cf12cc637e76599d71bb525b
author Nico Huber <nico.huber@secunet.com> Mon Jan 08 15:54:57 2024 +0100
committer Nico Huber <nico.huber@secunet.com> Mon Jan 08 15:59:01 2024 +0100
tree a79a99b2adebbf159fe7090d85649ea8888e44db
parent 700a411afa61504be84c9b64bfe45b491ccd3780

ext2: Adapt to satisfy some checks

src/filo-fs-ext2.adb

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;