1--  { dg-do compile }
2--  { dg-options "-gnatd.F -gnatws" }
3
4package body Iter2
5   with SPARK_Mode
6is
7   function To_String (Name : String) return String
8   is
9      procedure Append (Result : in out String;
10                        Data   :        String)
11        with Inline_Always;
12      procedure Append (Result : in out String;
13                        Data   :        String)
14      is
15      begin
16         for C of Data
17         loop
18            Result (1) := C;
19         end loop;
20      end Append;
21
22      Result : String (1 .. 3);
23   begin
24      Append (Result, "</" & Name & ">");
25      return Result;
26   end To_String;
27
28end Iter2;
29