-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================

with Ada.Characters.Handling;
with Ada.Characters.Latin_1;
with SPARK.Ada.Strings.Maps;
with SPARK.Ada.Strings.Unbounded.Not_SPARK;

package body E_Strings is

   function To_Unbounded_String (E_Str : T) return SPARK.Ada.Strings.Unbounded.Unbounded_String is
   begin
      return E_Str.Content;
   end To_Unbounded_String;

   -- Case (in)sensitive comparison.  Returns true if and only if the strings
   -- are equal, given the specified lengths.
   function Eq_String_Local
     (Str1 : SPARK.Ada.Strings.Unbounded.Unbounded_String;
      Str2 : SPARK.Ada.Strings.Unbounded.Unbounded_String)
     return Boolean
   is
      Result : Boolean;
   begin
      if SPARK.Ada.Strings.Unbounded.Get_Length (Source => Str1) = SPARK.Ada.Strings.Unbounded.Get_Length (Source => Str2) then
         Result := True;
         for I in Positions range 1 .. SPARK.Ada.Strings.Unbounded.Get_Length (Source => Str1) loop
            --# assert SPARK.Ada.Strings.Unbounded.Get_Length (Str1) =
            --#   SPARK.Ada.Strings.Unbounded.Get_Length (Str1%) and
            --#   SPARK.Ada.Strings.Unbounded.Get_Length (Str1) in Lengths;
            Result := Ada.Characters.Handling.To_Lower (SPARK.Ada.Strings.Unbounded.Get_Element (Source => Str1,
                                                                                                 Index  => I)) =
              Ada.Characters.Handling.To_Lower (SPARK.Ada.Strings.Unbounded.Get_Element (Source => Str2,
                                                                                         Index  => I));
            exit when not Result;
         end loop;
      else
         Result := False;
      end if;
      return Result;
   end Eq_String_Local;

   -- Case INsensitive comparison.
   function Eq_String (E_Str1, E_Str2 : T) return Boolean is
   begin
      return Eq_String_Local (Str1 => E_Str1.Content,
                              Str2 => E_Str2.Content);
   end Eq_String;

   -- Case INsensitive comparison.
   function Eq1_String (E_Str : T;
                        Str   : String) return Boolean is
   begin
      return Eq_String_Local
        (Str1 => E_Str.Content,
         Str2 => SPARK.Ada.Strings.Unbounded.String_To_Unbounded_String (Source => Str));
   end Eq1_String;

   -- Case sensitive comparison.
   function Eq_CS_String (E_Str1, E_Str2 : T) return Boolean is
   begin
      return SPARK.Ada.Strings.Unbounded.Equal_Unbounded_String_Unbounded_String (Left  => E_Str1.Content,
                                                                                  Right => E_Str2.Content);
   end Eq_CS_String;

   function Is_Empty (E_Str : T) return Boolean is
   begin
      return E_Str = Empty_String;
   end Is_Empty;

   function Get_Length (E_Str : T) return Lengths is
   begin
      return SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content);
   end Get_Length;

   function Get_Empty_String return T is
   begin
      return Empty_String;
   end Get_Empty_String;

   function Get_Element (E_Str : T;
                         Pos   : Positions) return Character is
      Return_Value : Character;
   begin
      if Pos <= SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content) then
         Return_Value := SPARK.Ada.Strings.Unbounded.Get_Element (Source => E_Str.Content,
                                                                  Index  => Pos);
      else
         Return_Value := ' ';
      end if;
      return Return_Value;
   end Get_Element;

   function Copy_String (Str : String) return T is
   begin
      return T'(Content => SPARK.Ada.Strings.Unbounded.String_To_Unbounded_String (Source => Str));
   end Copy_String;

   procedure Append_String (E_Str : in out T;
                            Str   : in     String) is
   begin
      SPARK.Ada.Strings.Unbounded.Append_String (Source   => E_Str.Content,
                                                 New_Item => Str);
   end Append_String;

   procedure Append_Examiner_String (E_Str1 : in out T;
                                     E_Str2 : in     T) is
   begin
      SPARK.Ada.Strings.Unbounded.Append_Unbounded_String (Source   => E_Str1.Content,
                                                           New_Item => E_Str2.Content);
   end Append_Examiner_String;

   function Lower_Case (E_Str : T) return T is
      Temp   : Character;
      Result : T;
   begin
      Result := E_Str;
      for I in Natural range 1 .. SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content) loop
         --# assert SPARK.Ada.Strings.Unbounded.Get_Length (E_Str.Content) =
         --#   SPARK.Ada.Strings.Unbounded.Get_Length (E_Str%.Content) and
         --#   SPARK.Ada.Strings.Unbounded.Get_Length (E_Str.Content) in Lengths;
         Temp := SPARK.Ada.Strings.Unbounded.Get_Element (Source => E_Str.Content,
                                                          Index  => I);
         if Temp in 'A' .. 'Z' then
            SPARK.Ada.Strings.Unbounded.Replace_Element
              (Source => Result.Content,
               Index  => I,
               By     => Ada.Characters.Handling.To_Lower (Temp));
         end if;
      end loop;
      return Result;
   end Lower_Case;

   function Upper_Case (E_Str : T) return T is
      Temp   : Character;
      Result : T;
   begin
      Result := E_Str;
      for I in Natural range 1 .. SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content) loop
         --# assert SPARK.Ada.Strings.Unbounded.Get_Length (E_Str.Content) =
         --#   SPARK.Ada.Strings.Unbounded.Get_Length (E_Str%.Content) and
         --#   SPARK.Ada.Strings.Unbounded.Get_Length (E_Str.Content) in Lengths;
         Temp := SPARK.Ada.Strings.Unbounded.Get_Element (Source => E_Str.Content,
                                                          Index  => I);
         if Temp in 'a' .. 'z' then
            SPARK.Ada.Strings.Unbounded.Replace_Element
              (Source => Result.Content,
               Index  => I,
               By     => Ada.Characters.Handling.To_Upper (Temp));
         end if;
      end loop;
      return Result;
   end Upper_Case;

   function Lower_Case_Char (E_Str : T;
                             Pos   : Positions) return T is
      Result : T;
   begin
      Result := E_Str;
      SPARK.Ada.Strings.Unbounded.Replace_Element
        (Source => Result.Content,
         Index  => Pos,
         By     => Ada.Characters.Handling.To_Lower (SPARK.Ada.Strings.Unbounded.Get_Element (Source => Result.Content,
                                                                                              Index  => Pos)));
      return Result;
   end Lower_Case_Char;

   function Upper_Case_Char (E_Str : T;
                             Pos   : Positions) return T is
      Result : T;
   begin
      Result := E_Str;
      SPARK.Ada.Strings.Unbounded.Replace_Element
        (Source => Result.Content,
         Index  => Pos,
         By     => Ada.Characters.Handling.To_Upper (SPARK.Ada.Strings.Unbounded.Get_Element (Source => Result.Content,
                                                                                              Index  => Pos)));
      return Result;
   end Upper_Case_Char;

   function Translate
     (E_Str     : T;
      From_Char : Character;
      To_Char   : Character)
     return      T
   is
      Result : T;
   begin
      Result := E_Str;
      for I in Positions range 1 .. SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content) loop
         --# assert SPARK.Ada.Strings.Unbounded.Get_Length (E_Str.Content) =
         --#   SPARK.Ada.Strings.Unbounded.Get_Length (E_Str%.Content) and
         --#   SPARK.Ada.Strings.Unbounded.Get_Length (E_Str.Content) in Lengths;
         if SPARK.Ada.Strings.Unbounded.Get_Element (Source => E_Str.Content,
                                                     Index  => I) = From_Char then
            SPARK.Ada.Strings.Unbounded.Replace_Element (Source => Result.Content,
                                                         Index  => I,
                                                         By     => To_Char);
         end if;
      end loop;
      return Result;
   end Translate;

   procedure Append_Char (E_Str : in out T;
                          Ch    : in     Character) is
   begin
      SPARK.Ada.Strings.Unbounded.Append_Char (Source   => E_Str.Content,
                                               New_Item => Ch);
   end Append_Char;

   -------------------------------------------------------------------------
   -- Find_Sub_String_After: for use in summary tool
   -- find the specified SearchString, starting at the specified position in
   -- the given T
   -------------------------------------------------------------------------
   procedure Find_Sub_String_After
     (E_Str         : in     T;
      Search_Start  : in     Positions;
      Search_String : in     String;
      String_Found  :    out Boolean;
      String_Start  :    out Positions)
   is
      Result : Natural;
   begin
      Result :=
        SPARK.Ada.Strings.Unbounded.Index_Pattern_From
        (Source   => E_Str.Content,
         Pattern  => Search_String,
         Arg_From => Search_Start,
         Going    => SPARK.Ada.Strings.Direction_Forward,
         Mapping  => SPARK.Ada.Strings.Maps.Identity);
      if Result = 0 then
         String_Found := False;
         String_Start := 1;
      else
         String_Found := True;
         String_Start := Result;
      end if;
   end Find_Sub_String_After;

   --------------------------------------------------------------------------
   -- Find_Sub_String: for use in summary tool
   -- find specified SearchString in the given T
   --------------------------------------------------------------------------
   procedure Find_Sub_String
     (E_Str         : in     T;
      Search_String : in     String;
      String_Found  :    out Boolean;
      String_Start  :    out Positions)
   is
      Result : Natural;
   begin
      Result :=
        SPARK.Ada.Strings.Unbounded.Index_Pattern
        (Source  => E_Str.Content,
         Pattern => Search_String,
         Going   => SPARK.Ada.Strings.Direction_Forward,
         Mapping => SPARK.Ada.Strings.Maps.Identity);
      if Result = 0 then
         String_Found := False;
         String_Start := 1;
      else
         String_Found := True;
         String_Start := Result;
      end if;
   end Find_Sub_String;

   procedure Find_Examiner_Sub_String
     (E_Str         : in     T;
      Search_String : in     T;
      String_Found  :    out Boolean;
      String_Start  :    out Positions)
   is
      --# hide Find_Examiner_Sub_String;
      Result : Natural;
   begin
      Result :=
        SPARK.Ada.Strings.Unbounded.Index_Pattern
        (Source  => E_Str.Content,
         Pattern => SPARK.Ada.Strings.Unbounded.Not_SPARK.To_String (Source => Search_String.Content),
         Going   => SPARK.Ada.Strings.Direction_Forward,
         Mapping => SPARK.Ada.Strings.Maps.Identity);
      if Result = 0 then
         String_Found := False;
         String_Start := 1;
      else
         String_Found := True;
         String_Start := Result;
      end if;
   end Find_Examiner_Sub_String;

   procedure Pop_Char (E_Str : in out T;
                       Char  :    out Character) is
   begin
      if SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content) = 0 then
         Char := ' ';
      else
         Char := SPARK.Ada.Strings.Unbounded.Get_Element (Source => E_Str.Content,
                                                          Index  => Positions'First);
         SPARK.Ada.Strings.Unbounded.Procedure_Delete (Source   => E_Str.Content,
                                                       Arg_From => Positions'First,
                                                       Through  => 1);
      end if;
   end Pop_Char;

   procedure Find_Char_After
     (E_Str        : in     T;
      Search_Start : in     Positions;
      Search_Char  : in     Character;
      Char_Found   :    out Boolean;
      Char_Pos     :    out Positions)
   is
      Result : Natural;
   begin
      Result :=
        SPARK.Ada.Strings.Unbounded.Index_Set_From
        (Source   => E_Str.Content,
         Arg_Set  => SPARK.Ada.Strings.Maps.Singleton_To_Set (Singleton => Search_Char),
         Arg_From => Search_Start,
         Test     => SPARK.Ada.Strings.Membership_Inside,
         Going    => SPARK.Ada.Strings.Direction_Forward);
      if Result = 0 then
         Char_Found := False;
         Char_Pos   := 1;
      else
         Char_Found := True;
         Char_Pos   := Result;
      end if;
   end Find_Char_After;

   procedure Find_Char
     (E_Str       : in     T;
      Search_Char : in     Character;
      Char_Found  :    out Boolean;
      Char_Pos    :    out Positions)
   is
      Result : Natural;
   begin
      Result :=
        SPARK.Ada.Strings.Unbounded.Index_Set
        (Source  => E_Str.Content,
         Arg_Set => SPARK.Ada.Strings.Maps.Singleton_To_Set (Singleton => Search_Char),
         Test    => SPARK.Ada.Strings.Membership_Inside,
         Going   => SPARK.Ada.Strings.Direction_Forward);
      if Result = 0 then
         Char_Found := False;
         Char_Pos   := 1;
      else
         Char_Found := True;
         Char_Pos   := Result;
      end if;
   end Find_Char;

   function Lex_Order (First_Name, Second_Name : T) return Order_Types is
      Result : Order_Types;
   begin
      if SPARK.Ada.Strings.Unbounded.Equal_Unbounded_String_Unbounded_String
        (Left  => First_Name.Content,
         Right => Second_Name.Content) then
         Result := Neither_First;
      elsif SPARK.Ada.Strings.Unbounded.Less_Unbounded_String_Unbounded_String
        (Left  => First_Name.Content,
         Right => Second_Name.Content) then
         Result := First_One_First;
      else
         Result := Second_One_First;
      end if;
      return Result;
   end Lex_Order;

   function Section
     (E_Str     : T;
      Start_Pos : Positions;
      Length    : Lengths)
     return      T
   is
      Result : T := Empty_String;
   begin
      --  Using an 'and then' here will confuse the simplifier, so we
      --  stick to a simple nested if.
      if Start_Pos - 1 <= Lengths'Last - Length then
         if Start_Pos + (Length - 1) <= SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content) then
            Result.Content :=
              SPARK.Ada.Strings.Unbounded.Function_Unbounded_Slice
              (Source => E_Str.Content,
               Low    => Start_Pos,
               High   => Start_Pos + (Length - 1));
         end if;
      end if;
      return Result;
   end Section;

   function Trim (E_Str : T) return T is
      subtype String_Length is Integer range 1 .. 4;
      subtype String_4 is String (String_Length);
      White_Space : String_4 := "    ";
   begin
      White_Space (1) := ' ';
      White_Space (2) := Ada.Characters.Latin_1.HT;
      White_Space (3) := Ada.Characters.Latin_1.LF;
      White_Space (4) := Ada.Characters.Latin_1.CR;
      return T'
        (Content => SPARK.Ada.Strings.Unbounded.Function_Trim_Character_Set
           (Source => E_Str.Content,
            Left   => SPARK.Ada.Strings.Maps.Character_Sequence_To_Set (Arg_Sequence => White_Space),
            Right  => SPARK.Ada.Strings.Maps.Character_Sequence_To_Set (Arg_Sequence => White_Space)));
   end Trim;

   procedure Get_Int_From_String
     (Source   : in     T;
      Item     :    out Integer;
      Start_Pt : in     Positions;
      Stop     :    out Natural)
   is
      --# hide Get_Int_From_String;
   begin
      SPARK_IO.Get_Int_From_String
        (Source    => SPARK.Ada.Strings.Unbounded.Not_SPARK.Slice
           (Source => Source.Content,
            Low    => Start_Pt,
            High   => SPARK.Ada.Strings.Unbounded.Get_Length (Source => Source.Content)),
         Item      => Item,
         Start_Pos => Start_Pt,
         Stop      => Stop);
   end Get_Int_From_String;

   procedure Put_Int_To_String
     (Dest     :    out T;
      Item     : in     Integer;
      Start_Pt : in     Positions;
      Base     : in     Valid_Base)
   is

      type Unsigned_Integer is range 0 .. 2 * (Integer'Last + 1);

      subtype Hex_Size is Unsigned_Integer range 0 .. 15;
      type Hex_T is array (Hex_Size) of Character;

      subtype String_Range is Positive range 1 .. 1;
      subtype String_1_T is String (String_Range);

      Hex : constant Hex_T :=
        Hex_T'
        (0  => '0',
         1  => '1',
         2  => '2',
         3  => '3',
         4  => '4',
         5  => '5',
         6  => '6',
         7  => '7',
         8  => '8',
         9  => '9',
         10 => 'A',
         11 => 'B',
         12 => 'C',
         13 => 'D',
         14 => 'E',
         15 => 'F');

      Local_Item  : Unsigned_Integer;
      Local_Base  : Unsigned_Integer;
      String_1    : String_1_T := String_1_T'(" ");
      Current_Pos : Positive;
   begin
      Dest       := Empty_String;
      Local_Base := Unsigned_Integer (Base);
      --# check Local_Base in Unsigned_Integer(Valid_Base'First) .. Unsigned_Integer(Valid_Base'Last);

      --  Pad with spaces
      for I in Positive range 2 .. Start_Pt loop
         --# assert Local_Base in Unsigned_Integer(Valid_Base'First) .. Unsigned_Integer(Valid_Base'Last) and
         --#   Start_Pt < Lengths'Last - (3 + 1 + 31);
         SPARK.Ada.Strings.Unbounded.Append_Char (Source   => Dest.Content,
                                                  New_Item => ' ');
      end loop;

      --# assert Local_Base in Unsigned_Integer(Valid_Base'First) .. Unsigned_Integer(Valid_Base'Last) and
      --#   Start_Pt < Lengths'Last - (3 + 1 + 31);

      --  Indicate the base if it is not 10
      Current_Pos := Start_Pt;
      if Local_Base /= 10 then
         if Local_Base > 10 then
            SPARK.Ada.Strings.Unbounded.Append_Char (Source   => Dest.Content,
                                                     New_Item => '1');
            Current_Pos := Current_Pos + 1;
         end if;
         SPARK.Ada.Strings.Unbounded.Append_Char (Source   => Dest.Content,
                                                  New_Item => Hex (Local_Base mod 10));
         SPARK.Ada.Strings.Unbounded.Append_Char (Source   => Dest.Content,
                                                  New_Item => '#');
         Current_Pos := Current_Pos + 2;
      end if;

      --# assert Local_Base in Unsigned_Integer(Valid_Base'First) .. Unsigned_Integer(Valid_Base'Last) and
      --#   Start_Pt < Lengths'Last - (3 + 1 + 31) and
      --#   Current_Pos >= Start_Pt and Current_Pos <= Start_Pt + 3;

      --  Obtain the absolute value of Item and indicate the sign in
      --  the generated string.
      if Item < 0 then
         Local_Item := Unsigned_Integer (-Long_Long_Integer (Item));
         SPARK.Ada.Strings.Unbounded.Append_Char (Source   => Dest.Content,
                                                  New_Item => '-');
         Current_Pos := Current_Pos + 1;
      else
         Local_Item := Unsigned_Integer (Item);
      end if;

      --# assert Local_Base in Unsigned_Integer(Valid_Base'First) .. Unsigned_Integer(Valid_Base'Last) and
      --#   Start_Pt < Lengths'Last - (3 + 1 + 31) and
      --#   Current_Pos >= Start_Pt and Current_Pos <= Start_Pt + 3 + 1 and
      --#   Local_Item mod Local_Base in 0 .. 15;

      --  Convert Local_Item and output to the string. We insert into
      --  the generated string at Current_Pos.
      while Local_Item >= Local_Base loop
         --# assert Local_Base in Unsigned_Integer(Valid_Base'First) .. Unsigned_Integer(Valid_Base'Last) and
         --#   Start_Pt < Lengths'Last - (3 + 1 + 31) and
         --#   Current_Pos >= Start_Pt and Current_Pos <= Start_Pt + 3 + 1 and
         --#   Local_Item mod Local_Base in 0 .. 15;
         String_1 (1) := Hex (Local_Item mod Local_Base);
         SPARK.Ada.Strings.Unbounded.Procedure_Insert (Source   => Dest.Content,
                                                       Before   => Current_Pos,
                                                       New_Item => String_1);
         Local_Item := Local_Item / Local_Base;
      end loop;
      String_1 (1) := Hex (Local_Item);
      SPARK.Ada.Strings.Unbounded.Procedure_Insert (Source   => Dest.Content,
                                                    Before   => Current_Pos,
                                                    New_Item => String_1);

      --  Insert the final base marking if necessary
      if Local_Base /= 10 then
         SPARK.Ada.Strings.Unbounded.Append_Char (Source   => Dest.Content,
                                                  New_Item => '#');
      end if;
   end Put_Int_To_String;

   function Get_Dotted_Common_Prefix_Length (E_Str_A, E_Str_B : T) return Lengths is
      Equal         : Boolean := False;
      Min_Length    : Lengths;
      Common_Prefix : Lengths := 0;
   begin
      Min_Length := Lengths'Min (Get_Length (E_Str_A), Get_Length (E_Str_B));
      --# assert Min_Length <= Get_Length (E_Str_A) and
      --#   Min_Length <= Get_Length (E_Str_B);

      if Min_Length >= 1 then
         for I in Positions range 1 .. Min_Length loop
            Equal := Get_Element (E_Str_A, I) = Get_Element (E_Str_B, I);
            exit when not Equal;
            if Get_Element (E_Str_A, I) = '.' then
               Common_Prefix := I - 1;
            end if;
         end loop;
         if Equal then
            if Get_Length (E_Str_A) = Get_Length (E_Str_B) then
               Common_Prefix := Get_Length (E_Str_A);
            elsif Get_Length (E_Str_A) > Get_Length (E_Str_B) then
               if Get_Element (E_Str_A, Get_Length (E_Str_B) + 1) = '.' then
                  Common_Prefix := Get_Length (E_Str_B);
               end if;
            else
               if Get_Element (E_Str_B, Get_Length (E_Str_A) + 1) = '.' then
                  Common_Prefix := Get_Length (E_Str_A);
               end if;
            end if;
         end if;
      end if;

      return Common_Prefix;
   end Get_Dotted_Common_Prefix_Length;

   function Starts_With (E_Str : T;
                         Str   : String) return Boolean is
      Result : Boolean;
   begin
      if Get_Length (E_Str) >= Str'Length then
         Result := Eq1_String (Section (E_Str     => E_Str,
                                        Start_Pos => Positions'First,
                                        Length    => Str'Length), Str);
      else
         Result := False;
      end if;
      return Result;
   end Starts_With;

   procedure Create
     (File         : in out SPARK_IO.File_Type;
      Name_Of_File : in     T;
      Form_Of_File : in     String;
      Status       :    out SPARK_IO.File_Status)
   is
      --# hide Create;
   begin
      SPARK_IO.Create
        (File         => File,
         Name_Length  => SPARK.Ada.Strings.Unbounded.Get_Length (Source => Name_Of_File.Content),
         Name_Of_File => SPARK.Ada.Strings.Unbounded.Not_SPARK.To_String (Source => Name_Of_File.Content),
         Form_Of_File => Form_Of_File,
         Status       => Status);
   end Create;

   procedure Open
     (File         : in out SPARK_IO.File_Type;
      Mode_Of_File : in     SPARK_IO.File_Mode;
      Name_Of_File : in     T;
      Form_Of_File : in     String;
      Status       :    out SPARK_IO.File_Status)
   is
      --# hide Open;
   begin
      SPARK_IO.Open
        (File         => File,
         Mode_Of_File => Mode_Of_File,
         Name_Length  => SPARK.Ada.Strings.Unbounded.Get_Length (Source => Name_Of_File.Content),
         Name_Of_File => SPARK.Ada.Strings.Unbounded.Not_SPARK.To_String (Source => Name_Of_File.Content),
         Form_Of_File => Form_Of_File,
         Status       => Status);
   end Open;

   procedure Put_String (File  : in SPARK_IO.File_Type;
                         E_Str : in T) is
      --# hide Put_String;
   begin
      if SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content) /= 0 then
         SPARK_IO.Put_String
           (File => File,
            Item => SPARK.Ada.Strings.Unbounded.Not_SPARK.To_String (Source => E_Str.Content),
            Stop => SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content));
      end if;
   end Put_String;

   procedure Put_Line (File  : in SPARK_IO.File_Type;
                       E_Str : in T) is
      --# hide Put_Line;
   begin
      if SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content) = 0 then
         SPARK_IO.New_Line (File    => File,
                            Spacing => 1);
      else
         SPARK_IO.Put_Line
           (File => File,
            Item => SPARK.Ada.Strings.Unbounded.Not_SPARK.To_String (Source => E_Str.Content),
            Stop => SPARK.Ada.Strings.Unbounded.Get_Length (Source => E_Str.Content));
      end if;
   end Put_Line;

   procedure Get_Line (File  : in     SPARK_IO.File_Type;
                       E_Str :    out T) is
      subtype String_Length is Integer range 1 .. 4096;
      subtype Long_String is String (String_Length);
      Item : Long_String;
      Stop : Natural;
   begin
      SPARK_IO.Get_Line (File => File,
                         Item => Item,
                         Stop => Stop);
      E_Str.Content := SPARK.Ada.Strings.Unbounded.String_To_Unbounded_String (Source => Item);
      E_Str.Content :=
        SPARK.Ada.Strings.Unbounded.Function_Unbounded_Slice (Source => E_Str.Content,
                                                              Low    => Positions'First,
                                                              High   => Stop);
   end Get_Line;

end E_Strings;