ext2: Further split our state record
To assist proving that the metadata doesn't change.
diff --git a/src/filo-fs-ext2.ads b/src/filo-fs-ext2.ads
index a13b153..7c1e467 100644
--- a/src/filo-fs-ext2.ads
+++ b/src/filo-fs-ext2.ads
@@ -63,6 +63,7 @@
subtype Block_Cache_Index is Natural range 0 .. 63;
type Cache_Label_Logical is array (Block_Cache_Index) of Boolean;
type Cache_Label_Array is array (Block_Cache_Index) of Cache_Label;
+ subtype Cache_Buffer is Buffer_Type (Max_Block_Index);
-- Same as the 12 direct + 3 indirect blocks times 4B:
subtype Inode_Extents_Index is Natural range 0 .. 59;
@@ -85,8 +86,7 @@
Inline : Inode_Extents := (others => 16#00#);
end record;
- type T is record
- S : State;
+ type Mount_State is record
Part_Len : Partition_Length := 0;
First_Data_Block : FSBlock_Offset := 0;
Block_Size_Bits : Log_Block_Size := Log_Block_Size'First;
@@ -96,11 +96,20 @@
Desc_Size : Ext2.Desc_Size := Ext2.Desc_Size'First;
Feature_Extents : Boolean := False;
Feature_64Bit : Boolean := False;
- Inode : Inode_Info := (others => <>);
- Cur_Dir : Inode_Index := Inode_Index'First;
- Block_Cache_Logical : Cache_Label_Logical := (others => False);
- Block_Cache_Label : Cache_Label_Array := (others => 0);
- Block_Cache : Buffer_Type (Max_Block_Index) := (others => 16#00#);
+ end record;
+
+ type Block_Cache is record
+ Logical : Cache_Label_Logical := (others => False);
+ Label : Cache_Label_Array := (others => 0);
+ Buffer : Cache_Buffer := (others => 16#00#);
+ end record;
+
+ type T is record
+ Static : Mount_State := (others => <>);
+ S : State;
+ Inode : Inode_Info := (others => <>);
+ Cur_Dir : Inode_Index := Inode_Index'First;
+ Cache : Block_Cache := (others => <>);
end record;
end FILO.FS.Ext2;