ext2: Somewhat finish proofs
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 3276cdd..96328dd 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -71,7 +71,7 @@
return;
end if;
end;
- pragma Assert_And_Cut (Success);
+ pragma Assert_And_Cut (Success and not Is_Mounted (State));
declare
S_Inodes_Per_Group : constant Unsigned_32 := Read_LE32 (Super_Block, 10 * 4);
@@ -83,7 +83,6 @@
return;
end if;
end;
- pragma Assert_And_Cut (Success);
declare
S_Rev_Level : constant Unsigned_32 := Read_LE32 (Super_Block, 19 * 4);
@@ -107,7 +106,7 @@
end if;
Static.Inodes_Per_Block := Inode_In_Block_Count (Static.Block_Size / Static.Inode_Size);
end;
- pragma Assert_And_Cut (Success);
+ pragma Assert_And_Cut (Success and not Is_Mounted (State));
declare
S_Feature_Incompat : constant Unsigned_32 := Read_LE32 (Super_Block, 24 * 4);
@@ -135,7 +134,6 @@
end if;
Static.Group_Desc_Per_Block := Group_In_Block_Count (Static.Block_Size / Static.Group_Desc_Size);
end;
- pragma Assert_And_Cut (Success);
State.S := Mounted;
end Mount;
@@ -224,6 +222,8 @@
Logical : in FSBlock_Logical;
Physical : out FSBlock_Offset;
Success : out Boolean)
+ with
+ Post => State.Static = State.Static'Old and State.S = State.S'Old
is
Static : constant Mount_State := State.Static;
@@ -254,7 +254,8 @@
with
Pre =>
Addr_Per_Block = FSBlock_Logical (Static.Block_Size / 4) and
- FSBlock_Logical (Addr_In_Block) < Addr_Per_Block
+ FSBlock_Logical (Addr_In_Block) < Addr_Per_Block,
+ Post => State.Static = State.Static'Old and State.S = State.S'Old
is
Cache_Start, Cache_End : Max_Block_Index;
begin
@@ -361,6 +362,8 @@
Logical : in FSBlock_Logical;
Physical : out FSBlock_Offset;
Success : out Boolean)
+ with
+ Post => State.Static = State.Static'Old and State.S = State.S'Old
is
Cache : Cache_Buffer renames State.Cache.Buffer;
@@ -495,7 +498,7 @@
Logical_Off <= Logical and
Dynamic_Max_Index = State.Static.Block_Size / Extent_Header_Size - 1,
Post =>
- State.Static = State.Static'Old and
+ State.Static = State.Static'Old and State.S = State.S'Old and
(if Success then
Next <= Dynamic_Max_Index and then
Cache_End = Cache_Start + State.Static.Block_Size - 1 and then
@@ -570,6 +573,7 @@
loop
pragma Loop_Invariant
(State.Static = State.Static'Loop_Entry and then
+ State.S = State.S'Loop_Entry and then
Depth > 0 and then
Depth in Extent_Depth and then
Logical_Off <= Logical);
@@ -692,7 +696,7 @@
Success : out Boolean)
with
Pre => Is_Mounted (State),
- Post => Success = Is_Open (State)
+ Post => Is_Mounted (State) and (Success = Is_Open (State))
is
Static : Mount_State renames State.Static;
Cache : Cache_Buffer renames State.Cache.Buffer;
@@ -926,7 +930,7 @@
Static : Mount_State renames State.Static;
Cache : Cache_Buffer renames State.Cache.Buffer;
- Pos : Natural;
+ Pos : Natural range Buf'First .. Buf'Last + 1;
begin
if State.Inode.Mode = Fast_Link then
if State.Inode.Size > Inode_Length (State.Inode.Inline'Length) or
@@ -944,22 +948,30 @@
Len := 0;
Pos := Buf'First;
- while Pos <= Buf'Last and Inode_Length (File_Pos) < State.Inode.Size loop
+ while Pos <= Buf'Last and
+ File_Pos < File_Offset'Last and
+ Inode_Length (File_Pos) < State.Inode.Size
+ loop
+ pragma Loop_Invariant (Is_Open (State));
declare
In_Block : constant Max_Block_Index := Natural (File_Pos) mod Static.Block_Size;
- Logical : constant FSBlock_Logical := FSBlock_Logical (File_Pos / File_Offset (Static.Block_Size));
- In_Block_Space : constant Natural := Natural (Static.Block_Size) - In_Block;
+ Logical : constant FSBlock_Logical :=
+ FSBlock_Logical (File_Pos / File_Offset (Static.Block_Size));
+ In_Block_Space : constant Positive := Static.Block_Size - In_Block;
In_File_Space : constant Inode_Length := State.Inode.Size - Inode_Length (File_Pos);
- In_Buf_Space : constant Natural := Buf'Last - Pos + 1;
- Len_Here : Natural;
+ In_Buf_Space : constant Positive := Buf'Last - Pos + 1;
+ Len_Here : Positive;
begin
Len_Here := In_Block_Space;
if In_File_Space < Inode_Length (Len_Here) then
- Len_Here := Natural (In_File_Space);
+ Len_Here := Positive (In_File_Space);
end if;
if In_Buf_Space < Len_Here then
Len_Here := In_Buf_Space;
end if;
+ if File_Offset'Last - File_Pos < File_Length (Len_Here) then
+ Len_Here := Positive (File_Offset'Last - File_Pos);
+ end if;
declare
Last : constant Index_Type := Pos + Len_Here - 1;
@@ -972,23 +984,24 @@
else
Ext2_Block_Map (State, Logical, Physical, Success);
end if;
- if Success then
- Cache_FSBlock
- (Static => Static,
- Cache => State.Cache,
- Phys => Physical,
- Level => Block_Cache_Index'Last,
- Cache_Start => Cache_Start,
- Cache_End => Cache_End,
- Success => Success);
- end if;
+ exit when not Success;
+
+ Cache_FSBlock
+ (Static => Static,
+ Cache => State.Cache,
+ Phys => Physical,
+ Level => Block_Cache_Index'Last,
+ Cache_Start => Cache_Start,
+ Cache_End => Cache_End,
+ Success => Success);
+ pragma Assert (Cache_Start <= Cache_End - (In_Block + Len_Here - 1));
exit when not Success;
Buf (Pos .. Last) := Cache (
Cache_Start + In_Block .. Cache_Start + In_Block + Len_Here - 1);
File_Pos := File_Pos + File_Length (Len_Here);
Pos := Pos + Len_Here;
- Len := Len + Len_Here;
+ Len := Pos - Buf'First;
end;
end;
end loop;
diff --git a/src/filo-fs-ext2.ads b/src/filo-fs-ext2.ads
index c48ee93..1757da8 100644
--- a/src/filo-fs-ext2.ads
+++ b/src/filo-fs-ext2.ads
@@ -24,7 +24,7 @@
Success : out Boolean)
with
Pre => Is_Mounted (State),
- Post => Success = Is_Open (State);
+ Post => (if Success then Is_Open (State) else Is_Mounted (State));
procedure Close (State : in out T)
with
@@ -37,7 +37,7 @@
Buf : out Buffer_Type;
Len : out Natural)
with
- Pre => Is_Open (State),
+ Pre => Is_Open (State) and Buf'Length > 0,
Post => Is_Open (State);
private
diff --git a/src/filo-fs-vfs.adb b/src/filo-fs-vfs.adb
index a43edf6..02e4c52 100644
--- a/src/filo-fs-vfs.adb
+++ b/src/filo-fs-vfs.adb
@@ -107,7 +107,7 @@
(Path : in out Path_String;
Rest_First : in Path_Index_Plus;
Rest_Last : in Path_Index;
- Link_Len : in Natural;
+ Link_Len : in Positive;
Success : out Boolean)
with
Pre =>
@@ -127,11 +127,15 @@
return;
end if;
+ pragma Warnings
+ (GNATprove, Off, """File_Pos"" is set*but not used",
+ Reason => "We only read the link at once, during path walks.");
Read
(State => State,
File_Pos => File_Pos,
Buf => Path_Buf (1 .. Link_Len),
Len => Read_Len);
+ pragma Warnings (GNATprove, On, """File_Pos"" is set*but not used");
Success := Read_Len = Link_Len;
if Success then
@@ -209,14 +213,14 @@
return;
end if;
when Link =>
- if File_Len > Path_Max then
+ if File_Len = 0 or File_Len > Path_Max then
Success := False;
else
Read_Link
(Path => Path,
Rest_First => Comp_Last + 1,
Rest_Last => Path_Last,
- Link_Len => Natural (File_Len),
+ Link_Len => Positive (File_Len),
Success => Success);
end if;
Close (State);