Extract Str_Buf_Equal() from ext2 driver
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index bab0c69..903820b 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -779,19 +779,6 @@
File_Name_Max : constant := 255;
Root_Inode : constant := 2;
- function Str_Buf_Equal (Str : String; Buf : Buffer_Type) return Boolean
- with
- Pre => Str'Length <= Buf'Length
- is
- begin
- for I in Str'Range loop
- if Character'Pos (Str (I)) /= Buf (Buf'First + (I - Str'First)) then
- return False;
- end if;
- end loop;
- return True;
- end Str_Buf_Equal;
-
File_Inode : Inode_Index;
File_Pos : File_Length;
begin
@@ -829,7 +816,7 @@
declare
Dir_Entry_Header_Length : constant := 4 + 2 + 1 + 1;
Dir_Entry_Header : Buffer_Type (0 .. Dir_Entry_Header_Length - 1);
- Dir_Entry_Name : Buffer_Type (0 .. File_Name_Max - 1);
+ Dir_Entry_Name : Buffer_Type (0 .. File_Name'Length - 1);
Entry_File_Pos : File_Offset := File_Pos;
Dir_Entry_Length : File_Length;
Inode : Inode_0_Index;
@@ -858,11 +845,11 @@
Buf => Dir_Entry_Name,
Len => Len);
pragma Warnings (GNATprove, On, """Entry_File_Pos"" is set*but not used");
- if Len < File_Name'Length then
+ if Len /= File_Name'Length then
return;
end if;
- Success := Str_Buf_Equal (File_Name, Dir_Entry_Name);
+ Success := Equal (File_Name, Dir_Entry_Name);
if Success then
File_Inode := Inode;
exit;