File tree 1 file changed +9
-6
lines changed
1 file changed +9
-6
lines changed Original file line number Diff line number Diff line change
1
+ with Ada.Containers.Formal_Vectors ;
1
2
with Ada.Text_IO ;
2
3
3
- with Coord ;
4
-
5
4
procedure Repro
6
5
with SPARK_Mode => On
7
6
is
8
7
8
+ package Points is new Ada.Containers.Formal_Vectors
9
+ (Element_Type => Natural,
10
+ Index_Type => Natural);
11
+
9
12
-- Instantiate Vec_2 to have a Capacity of 200.
10
- Vec_2 : Coord. Points.Vector (200 );
13
+ Vec_2 : Points.Vector (200 );
11
14
12
15
Pos : constant Natural := 12345 ;
13
16
14
17
begin
15
18
16
19
-- Fails SPARK analysis, but we knew that was going to happen...
17
20
for J in Positive range 1 .. 40005 loop
18
- Coord. Points.Append(Vec_2, Pos);
19
- Ada.Text_IO.Put_Line (" Vector Append" & Coord. Points.Length(Vec_2)'Image);
21
+ Points.Append(Vec_2, Pos);
22
+ Ada.Text_IO.Put_Line (" Vector Append" & Points.Length(Vec_2)'Image);
20
23
end loop ;
21
24
22
25
Ada.Text_IO.Put_Line
23
- (" Vector Finished" & Coord. Points.Length(Vec_2)'Image);
26
+ (" Vector Finished" & Points.Length(Vec_2)'Image);
24
27
25
28
end Repro ;
You can’t perform that action at this time.
0 commit comments