ext2: Use unnecessarily big range type to ease proving
diff --git a/src/filo-fs-ext2.ads b/src/filo-fs-ext2.ads
index 5e6b641..c48ee93 100644
--- a/src/filo-fs-ext2.ads
+++ b/src/filo-fs-ext2.ads
@@ -71,7 +71,8 @@
with
Object_Size => (Inode_Extents_Index'Last + 1) * 8;
- type Inode_0_Index is new Unsigned_32;
+ -- TODO: Could use modular Unsigned_32 if GNATprove wouldn't stumble as much:
+ type Inode_0_Index is new Integer_64 range 0 .. Integer_64 (Unsigned_32'Last);
subtype Inode_Index is Inode_0_Index range 2 .. Inode_0_Index'Last;
subtype Inode_Size is Positive range 128 .. Positive (Unsigned_16'Last);
subtype Group_Desc_Size is Positive range 32 .. 2 ** 15; -- power-of-2 that fits in 16 bits