ext2: Fix binary extent search and help proof
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 3dbbb2b..3cdeca5 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -433,12 +433,15 @@
function Bin_Search (Buf : Buffer_Type; Refs : Extent_Idx) return Extent_Idx
with
- Pre => Refs in 1 .. Extent_Idx (Buf'Length / Extent_Header_Size - 1) and
- Extent_Logical (Buf, 1) <= Logical,
- Post => Bin_Search'Result in 1 .. Refs and
- Extent_Logical (Buf, Bin_Search'Result) <= Logical
+ Pre =>
+ Buf'Length in 2 * Extent_Header_Size .. Max_Block_Index'Last and then
+ Refs in 1 .. Extent_Idx (Buf'Length / Extent_Header_Size - 1) and then
+ Extent_Logical (Buf, 1) <= Logical,
+ Post =>
+ Bin_Search'Result in 1 .. Refs and
+ Extent_Logical (Buf, Bin_Search'Result) <= Logical
is
- Left : Extent_Idx := 1;
+ Left : Positive := 2;
Right : Extent_Idx := Refs;
begin
while Left <= Right loop
@@ -451,6 +454,10 @@
else
Left := Mid + 1;
end if;
+ pragma Loop_Invariant
+ (Right <= Refs and then
+ Left in 2 .. Refs + 1 and then
+ Extent_Logical (Buf, Left - 1) <= Logical);
end;
end loop;
return Left - 1;