ext2: Help proof of extent lookup
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 3cdeca5..4dcde30 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -377,6 +377,7 @@
subtype Extent_Off is Natural range 0 .. Extent_Header_Size;
subtype Extent_Idx is Natural range 1 .. (Max_Block_Index'Last + 1) / Extent_Header_Size - 1;
Dynamic_Max_Index : constant Extent_Idx := State.Block_Size / Extent_Header_Size - 1;
+ subtype Extent_Depth is Natural range 0 .. 32;
function Extent_Byte_Offset (Idx : Extent_Idx; Off : Extent_Off) return Natural
is
@@ -466,7 +467,7 @@
procedure Next_Ref
(Current : in FSBlock_Offset;
Logical_Off : in FSBlock_Logical;
- Depth : in Natural;
+ Depth : in Extent_Depth;
Next : out Extent_Idx;
Cache_Start : out Max_Block_Index;
Cache_End : out Max_Block_Index;
@@ -474,6 +475,7 @@
with
Pre => Logical_Off <= Logical,
Post => (if Success then
+ Next <= Dynamic_Max_Index and then
Cache_End = Cache_Start + State.Block_Size - 1 and then
Extent_Logical (State.Block_Cache (Cache_Start .. Cache_End), Next) <= Logical)
is
@@ -504,6 +506,7 @@
Success := Success and then
Hdr_Magic = Extent_Header_Magic and then
Hdr_Depth = Depth and then
+ Hdr_Entries in Extent_Idx and then
Hdr_Entries <= Dynamic_Max_Index and then
First_Logical = Logical_Off;
if not Success then
@@ -528,7 +531,8 @@
Inode_Magic = Extent_Header_Magic and then
Inode_Entries > 0 and then
Inode_Entries < Inline_Extents'Length / Extent_Header_Size and then
- First_Logical <= Logical;
+ First_Logical <= Logical and then
+ Depth in Extent_Depth;
if not Success then
Physical := 0;
return;
@@ -543,6 +547,10 @@
Physical := Index_Physical (Inline_Extents, Idx);
Logical_Off := Index_Logical (Inline_Extents, Idx);
loop
+ pragma Loop_Invariant
+ (Depth > 0 and then
+ Depth in Extent_Depth and then
+ Logical_Off <= Logical);
Depth := Depth - 1;
Next_Ref
(Current => Physical,