iso9660: Fix small bugs and proofs
diff --git a/src/filo-fs-iso9660.adb b/src/filo-fs-iso9660.adb
index c542ee0..a4af392 100644
--- a/src/filo-fs-iso9660.adb
+++ b/src/filo-fs-iso9660.adb
@@ -109,7 +109,9 @@
Dir_Rec_Len : in FSBlock_Length;
Searched_Sig : in SUSP_Signature)
with
- Pre => FSBlock_Index (Dir_Rec_Pos mod FSBlock_Size) <= FSBlock_Size - Dir_Rec_Len
+ Pre =>
+ Dir_Rec_Pos mod FSBlock_Size <= File_Offset (FSBlock_Size - Dir_Rec_Len) and
+ FSBlock_Count (Dir_Rec_Pos / FSBlock_Size) < State.Inode.Extents (0).Count
is
subtype Signature_Buf is Buffer_Type (0 .. 1);
function Signature (Str : SUSP_Signature) return Signature_Buf
@@ -121,7 +123,7 @@
Offset => FSBlock_Index (Dir_Rec_Pos mod FSBlock_Size),
Size => Dir_Rec_Len);
- Continuation : FS_Record := (others => <>);
+ Continuation : FS_Record := (Size => 0, others => <>);
SUSP_Head : Buffer_Type (0 .. 3);
@@ -138,7 +140,7 @@
for I in 1 .. 2**16 loop -- arbitrary limit to avoid endless loop
if Cur.Size < SUSP_Head'Length then
- if Continuation.Size = 0 then
+ if Continuation.Size < SUSP_Head'Length then
return;
else
Cur := Continuation;
@@ -175,14 +177,15 @@
CE_Offset : constant Unsigned_32 := Read_LE32 (SUSP_CE, 12);
CE_Size : constant Unsigned_32 := Read_LE32 (SUSP_CE, 20);
begin
- if (CE_Offset > FSBlock_Size or CE_Size > FSBlock_Size) or else
- CE_Offset > FSBlock_Size - CE_Size
+ if CE_Extent > Unsigned_32 (FSBlock'Last) or else
+ (CE_Offset > FSBlock_Size or CE_Size > FSBlock_Size) or else
+ FSBlock_Length (CE_Size) > FSBlock_Size - FSBlock_Length (CE_Offset)
then
return;
end if;
Continuation :=
(Block => FSBlock (CE_Extent),
- Offset => FSBlock_Index (CE_Offset),
+ Offset => FSBlock_Length (CE_Offset),
Size => FSBlock_Length (CE_Size));
end;
end if;
@@ -233,10 +236,17 @@
else
Inode.Mode := Regular;
end if;
+
Inode.Size := Inode_Length (Read_LE32 (Dir_Rec, 10));
+ if FSBlock (D_Extent) > FSBlock_Count'Last - FSBlock_Count (Inode.Size / FSBlock_Size)
+ then
+ Success := False;
+ return;
+ end if;
+
Inode.Extents (0) :=
(Start => FSBlock (D_Extent),
- Count => FSBlock_Count (Inode.Size / Inode_Length (FSBlock_Size)));
+ Count => FSBlock_Count (Inode.Size / FSBlock_Size));
State.S := File_Opened;
end;
end Open;
@@ -252,11 +262,12 @@
File_Name_Max : constant := 255;
procedure Match_ISO_Name
- (ISO_Name_Length : in Natural;
+ (ISO_Name_Length : in Positive;
Record_Dir_Pos : in File_Offset;
Success : in out Boolean)
with
- Post => State.Static = State.Static'Old
+ Pre => Is_Open (State) and File_Name'Length <= Natural'Last - 3,
+ Post => Is_Open (State)
is
function Upper_Case_Equal (Str : String; Buf : Buffer_Type) return Boolean
with
@@ -304,23 +315,23 @@
end if;
pragma Warnings (GNATprove, On, """Dir_Pos"" is set*but not used");
- if (Name_Len = 1 and ISO_Name (0) = 16#00# and File_Name = ".") or
- (Name_Len = 1 and ISO_Name (0) = 16#01# and File_Name = "..")
+ if (Name_Len = 1 and then (ISO_Name (0) = 16#00# and File_Name = ".")) or
+ (Name_Len = 1 and then (ISO_Name (0) = 16#01# and File_Name = ".."))
then
Success := True;
return;
end if;
-- Ignore file version `;1'
- if Name_Len >= File_Name'Length + 2 and
- ISO_Name (Name_Len - 2) = Character'Pos (';') and
- ISO_Name (Name_Len - 1) = Character'Pos ('1')
+ if Name_Len >= File_Name'Length + 2 and then
+ (ISO_Name (Name_Len - 2) = Character'Pos (';') and
+ ISO_Name (Name_Len - 1) = Character'Pos ('1'))
then
Name_Len := Name_Len - 2;
end if;
-- Ignore trailing `.'
- if Name_Len >= File_Name'Length + 1 and
+ if Name_Len >= File_Name'Length + 1 and then
ISO_Name (Name_Len - 1) = Character'Pos ('.')
then
Name_Len := Name_Len - 1;
@@ -332,15 +343,18 @@
procedure Match_Rock_Ridge_Name
(Pos : in File_Offset;
- Len : in Natural;
- Success : in out Boolean)
+ Len : in FSBlock_Length;
+ Success : out Boolean)
with
+ Pre =>
+ Pos mod FSBlock_Size <= File_Offset (FSBlock_Size - Len) and
+ FSBlock_Count (Pos / FSBlock_Size) < State.Inode.Extents (0).Count,
Post => State = State'Old
is
Name_Rec : FS_Record;
begin
Find_SUSP_Record (State, Name_Rec, Pos, Len, "NM");
- if Name_Rec.Size /= File_Name'Length + 5 then
+ if Name_Rec.Size - 5 /= File_Name'Length then
Success := False;
return;
end if;
@@ -415,7 +429,7 @@
if Dir_Rec_Length /= 0 then
if Unsigned_64 (Dir_Pos) > Unsigned_64 (State.Inode.Size) - Unsigned_64 (Dir_Rec_Length) or
- Dir_Rec_Name_Length > Dir_Rec_Length - Dir_Rec_Head'Length
+ Dir_Rec_Name_Length not in 1 .. Dir_Rec_Length - Dir_Rec_Head'Length
then
return;
end if;