ext2: Adjust Extent_Block_Map() to ease proof
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index deb2d21..3d6c0eb 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -481,11 +481,15 @@
Cache_End : out Max_Block_Index;
Success : out Boolean)
with
- Pre => Logical_Off <= Logical,
- Post => (if Success then
- Next <= Dynamic_Max_Index and then
- Cache_End = Cache_Start + State.Static.Block_Size - 1 and then
- Extent_Logical (Cache (Cache_Start .. Cache_End), Next) <= Logical)
+ Pre =>
+ Logical_Off <= Logical and
+ Dynamic_Max_Index = State.Static.Block_Size / Extent_Header_Size - 1,
+ Post =>
+ State.Static = State.Static'Old and
+ (if Success then
+ Next <= Dynamic_Max_Index and then
+ Cache_End = Cache_Start + State.Static.Block_Size - 1 and then
+ Extent_Logical (Cache (Cache_Start .. Cache_End), Next) <= Logical)
is
begin
Cache_FSBlock
@@ -518,6 +522,7 @@
if not Success then
Next := 1;
else
+ pragma Assert (Cache_End - Cache_Start + 1 = State.Static.Block_Size);
Next := Bin_Search (Cache (Cache_Start .. Cache_End), Hdr_Entries);
end if;
end;
@@ -554,7 +559,8 @@
Logical_Off := Index_Logical (Inline_Extents, Idx);
loop
pragma Loop_Invariant
- (Depth > 0 and then
+ (State.Static = State.Static'Loop_Entry and then
+ Depth > 0 and then
Depth in Extent_Depth and then
Logical_Off <= Logical);
Depth := Depth - 1;
@@ -583,7 +589,8 @@
Success :=
Length > 0 and then
Logical_Off <= FSBlock_Logical'Last - Length and then
- Logical < Logical_Off + Length;
+ Logical < Logical_Off + Length and then
+ FSBlock_Offset (Logical - Logical_Off) <= FSBlock_Offset'Last - Physical;
if Success then
Physical := Physical + FSBlock_Offset (Logical - Logical_Off);
end if;