isofs: Assist proofs
diff --git a/src/filo-fs-iso9660.adb b/src/filo-fs-iso9660.adb
index 8c1b441..03f1abb 100644
--- a/src/filo-fs-iso9660.adb
+++ b/src/filo-fs-iso9660.adb
@@ -22,7 +22,7 @@
--------------------------------------------------------------------------
procedure Read
- (Buf : in out Buffer_Type;
+ (Buf : out Buffer_Type;
Block : in FSBlock;
Offset : in FSBlock_Index;
FS_Len : in Partition_Length;
@@ -35,6 +35,7 @@
Max_Block_Offset : constant Integer_64 := Integer_64 (FS_Len) / FSBlock_Size - 1;
begin
if Block_64 > Max_Block_Offset then
+ Buf := (others => 16#00#);
Success := False;
return;
end if;
@@ -59,18 +60,19 @@
Static : Mount_State renames State.Static;
- Volume_Descriptor : Buffer_Type (0 .. 190 - 1);
+ Volume_Descriptor : Buffer_Type (0 .. D_Ver);
Block : FSBlock := 32;
begin
loop
pragma Loop_Invariant (Block < 1024);
+ pragma Loop_Invariant (not Is_Mounted (State));
if Part_Len < Partition_Length (Block + 1) * FSBlock_Size then
Success := False;
return;
end if;
- Read (Volume_Descriptor (0 .. D_Ver), Block, 0, Part_Len, Success);
+ Read (Volume_Descriptor, Block, 0, Part_Len, Success);
if not Success then
return;
end if;
@@ -79,6 +81,7 @@
Volume_Descriptor (D_Id .. D_Ver - 1) /= CD001 or
Volume_Descriptor (D_Type) = D_Type_Terminator
then
+ Success := False;
return;
end if;
@@ -86,6 +89,7 @@
Block := Block + 1;
if Block >= 1024 then
+ Success := False;
return;
end if;
end loop;
@@ -109,6 +113,8 @@
Dir_Rec : Directory_Record;
begin
+ State.S := Mounted;
+
Inode := (I, others => <>);
Read (Dir_Rec, I.Block, I.Offset, Static.Part_Len, Success);
@@ -120,11 +126,17 @@
D_Flag_Dir : constant := 16#02#;
D_Flag_Cont : constant := 16#80#;
D_Flags : constant Unsigned_8 := Dir_Rec (25);
+ D_Extent : constant Unsigned_32 := Read_LE32 (Dir_Rec, 2);
begin
+ if D_Extent > Unsigned_32 (FSBlock'Last) then
+ Success := False;
+ return;
+ end if;
if (D_Flags and D_Flag_Cont) /= 0 then
Success := False;
return;
end if;
+
if (D_Flags and D_Flag_Dir) /= 0 then
Inode.Mode := Dir;
else
@@ -132,7 +144,7 @@
end if;
Inode.Size := Inode_Length (Read_LE32 (Dir_Rec, 10));
Inode.Extents (0) :=
- (Start => FSBlock (Read_LE32 (Dir_Rec, 2)),
+ (Start => FSBlock (D_Extent),
Count => FSBlock_Count (Inode.Size / Inode_Length (FSBlock_Size)));
State.S := File_Opened;
end;
@@ -199,6 +211,9 @@
Success := False;
loop
pragma Loop_Invariant (Is_Open (State) and not Success);
+ pragma Loop_Invariant
+ (FSBlock_Index (Dir_Pos mod FSBlock_Size) <= Directory_Record_Offset'Last);
+
declare
Dir_Rec : Directory_Record;
Dir_Rec_Name : Buffer_Type (0 .. File_Name_Max - 1);
@@ -241,8 +256,10 @@
end if;
Dir_Rec_Length := File_Length (Dir_Rec (0));
- if Dir_Rec_Length = 0 or
- Dir_Pos > File_Length'Last - Dir_Rec_Length or
+ if Dir_Rec_Length = 0 or else
+ Dir_Pos > File_Length'Last - Dir_Rec_Length or else
+ (Dir_Pos + Dir_Rec_Length) mod FSBlock_Size
+ > File_Length (Directory_Record_Offset'Last) or else
Unsigned_64 (Dir_Pos) >= Unsigned_64 (State.Inode.Size) - Unsigned_64 (Dir_Rec_Length)
then
return;
@@ -261,7 +278,7 @@
State.Cur_Dir := Found_Inode;
end if;
- --Success := State.Inode.Size <= Inode_Length (File_Length'Last);
+ Success := State.Inode.Size <= Inode_Length (File_Length'Last);
if Success then
File_Len := File_Length (State.Inode.Size);
File_Type := State.Inode.Mode;
@@ -291,6 +308,7 @@
File_Pos < File_Offset'Last and
Inode_Length (File_Pos) < State.Inode.Size
loop
+ pragma Loop_Invariant (for all I in Buf'First .. Pos - 1 => Buf (I)'Initialized);
pragma Loop_Invariant (Is_Open (State));
declare
In_Block : constant FSBlock_Index := Natural (File_Pos mod FSBlock_Size);
diff --git a/src/filo-fs-iso9660.ads b/src/filo-fs-iso9660.ads
index dd82d74..0a28cc2 100644
--- a/src/filo-fs-iso9660.ads
+++ b/src/filo-fs-iso9660.ads
@@ -31,14 +31,19 @@
Pre => Is_Open (State),
Post => Is_Mounted (State);
+ pragma Warnings
+ (GNATprove, Off, """State"" is not modified*",
+ Reason => "It's `in out' to fulfill common interface.");
procedure Read
(State : in out T;
File_Pos : in out File_Offset;
Buf : out Buffer_Type;
Len : out Natural)
with
+ Relaxed_Initialization => Buf,
Pre => Is_Open (State) and Buf'Length > 0,
- Post => Is_Open (State);
+ Post => Is_Open (State) and Buf'Initialized;
+ pragma Warnings (GNATprove, On, """State"" is not modified*");
private
type State is (Unmounted, Mounted, File_Opened);
@@ -52,11 +57,13 @@
subtype Directory_Record_Range is Index_Type range 0 .. 32;
subtype Directory_Record is Buffer_Type (Directory_Record_Range);
+ subtype Directory_Record_Offset is FSBlock_Index
+ range 0 .. FSBlock_Size - Directory_Record'Length;
-- We'll use the absolute position of the dir record
type Inode_Index is record
Block : FSBlock := 0;
- Offset : FSBlock_Index := 0;
+ Offset : Directory_Record_Offset := 0;
end record;
type Inode_Length is range 0 .. FSBlock_Count'Last * FSBlock_Size;