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