ext2: Finish round of proofs for inode version of Open()
Only things left that could possibly be shown with a predicate
on Mount_State.
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index a69730e..d7bd018 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -715,10 +715,12 @@
Cache_Start => Cache_Start,
Cache_End => Cache_End,
Success => Success);
+ Success := Success and then
+ -- TODO: Prove this using a predicate on Mount_State:
+ Cache_Start <= Cache_End - Group_In_Block_Offset - Static.Group_Desc_Size + 1;
if not Success then
return;
end if;
- pragma Assert_And_Cut (Cache_End = Cache_Start + Static.Block_Size - 1);
Parse_Group
(Static => Static,
@@ -729,7 +731,6 @@
if not Success then
return;
end if;
- pragma Assert_And_Cut (Boolean'(True));
declare
Inode_In_Group : constant Inode_In_Group_Index :=
@@ -745,7 +746,6 @@
Success := False;
return;
end if;
- pragma Assert_And_Cut (First_Table_Block + Inode_Block in FSBlock_Offset);
Cache_FSBlock
(Static => Static,
@@ -755,6 +755,9 @@
Cache_Start => Cache_Start,
Cache_End => Cache_End,
Success => Success);
+ Success := Success and then
+ -- TODO: Prove this using a predicate on Mount_State:
+ Cache_Start <= Cache_End - Inode_In_Block_Offset - Static.Inode_Size + 1;
if not Success then
return;
end if;