PR c/79855: add full stop to store merging param descriptions
[official-gcc.git] / gcc / ada / a-cfinve.ads
blobe76ae8d89268b774f5f00e4675cb1a200dcd3183
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT LIBRARY COMPONENTS --
4 -- --
5 -- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
10 -- --
11 -- This specification is derived from the Ada Reference Manual for use with --
12 -- GNAT. The copyright notice above, and the license provisions that follow --
13 -- apply solely to the contents of the part following the private keyword. --
14 -- --
15 -- GNAT is free software; you can redistribute it and/or modify it under --
16 -- terms of the GNU General Public License as published by the Free Soft- --
17 -- ware Foundation; either version 3, or (at your option) any later ver- --
18 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
19 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
20 -- or FITNESS FOR A PARTICULAR PURPOSE. --
21 -- --
22 -- As a special exception under Section 7 of GPL version 3, you are granted --
23 -- additional permissions described in the GCC Runtime Library Exception, --
24 -- version 3.1, as published by the Free Software Foundation. --
25 -- --
26 -- You should have received a copy of the GNU General Public License and --
27 -- a copy of the GCC Runtime Library Exception along with this program; --
28 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
29 -- <http://www.gnu.org/licenses/>. --
30 ------------------------------------------------------------------------------
32 -- Similar to Ada.Containers.Formal_Vectors. The main difference is that
33 -- Element_Type may be indefinite (but not an unconstrained array). In
34 -- addition, this is simplified by removing less-used functionality.
36 with Ada.Containers.Bounded_Holders;
37 with Ada.Containers.Formal_Vectors;
39 generic
40 type Index_Type is range <>;
41 type Element_Type (<>) is private;
42 Max_Size_In_Storage_Elements : Natural :=
43 Element_Type'Max_Size_In_Storage_Elements;
44 -- Maximum size of Vector elements in bytes. This has the same meaning as
45 -- in Ada.Containers.Bounded_Holders, with the same restrictions. Note that
46 -- setting this too small can lead to erroneous execution; see comments in
47 -- Ada.Containers.Bounded_Holders. If Element_Type is class-wide, it is the
48 -- responsibility of clients to calculate the maximum size of all types in
49 -- the class.
51 with function "=" (Left, Right : Element_Type) return Boolean is <>;
53 Bounded : Boolean := True;
54 -- If True, the containers are bounded; the initial capacity is the maximum
55 -- size, and heap allocation will be avoided. If False, the containers can
56 -- grow via heap allocation.
58 package Ada.Containers.Formal_Indefinite_Vectors with
59 SPARK_Mode => On
61 pragma Annotate (GNATprove, External_Axiomatization);
62 pragma Annotate (CodePeer, Skip_Analysis);
64 subtype Extended_Index is Index_Type'Base
65 range Index_Type'First - 1 ..
66 Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
68 No_Index : constant Extended_Index := Extended_Index'First;
70 subtype Capacity_Range is
71 Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
73 type Vector (Capacity : Capacity_Range) is limited private with
74 Default_Initial_Condition;
76 function Empty_Vector return Vector;
78 function "=" (Left, Right : Vector) return Boolean with
79 Global => null;
81 function To_Vector
82 (New_Item : Element_Type;
83 Length : Capacity_Range) return Vector
84 with
85 Global => null;
87 function Capacity (Container : Vector) return Capacity_Range with
88 Global => null,
89 Post => Capacity'Result >= Container.Capacity;
91 procedure Reserve_Capacity
92 (Container : in out Vector;
93 Capacity : Capacity_Range)
94 with
95 Global => null,
96 Pre => (if Bounded then Capacity <= Container.Capacity);
98 function Length (Container : Vector) return Capacity_Range with
99 Global => null;
101 function Is_Empty (Container : Vector) return Boolean with
102 Global => null;
104 procedure Clear (Container : in out Vector) with
105 Global => null;
106 -- Note that this reclaims storage in the unbounded case. You need to call
107 -- this before a container goes out of scope in order to avoid storage
108 -- leaks.
110 procedure Assign (Target : in out Vector; Source : Vector) with
111 Global => null,
112 Pre => (if Bounded then Length (Source) <= Target.Capacity);
114 function Copy
115 (Source : Vector;
116 Capacity : Capacity_Range := 0) return Vector
117 with
118 Global => null,
119 Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity));
121 function Element
122 (Container : Vector;
123 Index : Index_Type) return Element_Type
124 with
125 Global => null,
126 Pre => Index in First_Index (Container) .. Last_Index (Container);
128 procedure Replace_Element
129 (Container : in out Vector;
130 Index : Index_Type;
131 New_Item : Element_Type)
132 with
133 Global => null,
134 Pre => Index in First_Index (Container) .. Last_Index (Container);
136 procedure Append
137 (Container : in out Vector;
138 New_Item : Vector)
139 with
140 Global => null,
141 Pre => (if Bounded
142 then Length (Container) + Length (New_Item) <=
143 Container.Capacity);
145 procedure Append
146 (Container : in out Vector;
147 New_Item : Element_Type)
148 with
149 Global => null,
150 Pre => (if Bounded
151 then Length (Container) < Container.Capacity);
153 procedure Delete_Last
154 (Container : in out Vector)
155 with
156 Global => null;
158 procedure Reverse_Elements (Container : in out Vector) with
159 Global => null;
161 procedure Swap (Container : in out Vector; I, J : Index_Type) with
162 Global => null,
163 Pre => I in First_Index (Container) .. Last_Index (Container)
164 and then J in First_Index (Container) .. Last_Index (Container);
166 function First_Index (Container : Vector) return Index_Type with
167 Global => null;
169 function First_Element (Container : Vector) return Element_Type with
170 Global => null,
171 Pre => not Is_Empty (Container);
173 function Last_Index (Container : Vector) return Extended_Index with
174 Global => null;
176 function Last_Element (Container : Vector) return Element_Type with
177 Global => null,
178 Pre => not Is_Empty (Container);
180 function Find_Index
181 (Container : Vector;
182 Item : Element_Type;
183 Index : Index_Type := Index_Type'First) return Extended_Index
184 with
185 Global => null;
187 function Reverse_Find_Index
188 (Container : Vector;
189 Item : Element_Type;
190 Index : Index_Type := Index_Type'Last) return Extended_Index
191 with
192 Global => null;
194 function Contains
195 (Container : Vector;
196 Item : Element_Type) return Boolean
197 with
198 Global => null;
200 function Has_Element
201 (Container : Vector; Position : Extended_Index) return Boolean with
202 Global => null;
204 generic
205 with function "<" (Left, Right : Element_Type) return Boolean is <>;
206 package Generic_Sorting with SPARK_Mode is
208 function Is_Sorted (Container : Vector) return Boolean with
209 Global => null;
211 procedure Sort (Container : in out Vector) with
212 Global => null;
214 end Generic_Sorting;
216 function First_To_Previous
217 (Container : Vector;
218 Current : Index_Type) return Vector
219 with
220 Ghost,
221 Global => null;
223 function Current_To_Last
224 (Container : Vector;
225 Current : Index_Type) return Vector
226 with
227 Ghost,
228 Global => null;
230 private
231 pragma SPARK_Mode (Off);
233 pragma Inline (First_Index);
234 pragma Inline (Last_Index);
235 pragma Inline (Element);
236 pragma Inline (First_Element);
237 pragma Inline (Last_Element);
238 pragma Inline (Replace_Element);
239 pragma Inline (Contains);
241 -- The implementation method is to instantiate Bounded_Holders to get a
242 -- definite type for Element_Type, and then use that Holder type to
243 -- instantiate Formal_Vectors. All the operations are just wrappers.
245 package Holders is new Bounded_Holders
246 (Element_Type, Max_Size_In_Storage_Elements, "=");
247 use Holders;
249 package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded);
250 use Def;
252 -- ????Assert that Def subtypes have the same range
254 type Vector (Capacity : Capacity_Range) is limited record
255 V : Def.Vector (Capacity);
256 end record;
258 function Empty_Vector return Vector is
259 ((Capacity => 0, V => Def.Empty_Vector));
261 end Ada.Containers.Formal_Indefinite_Vectors;