------------------------------------------------------------------------------
with Ada.Containers.Generic_Array_Sort;
-with Ada.Unchecked_Deallocation;
with System; use type System.Address;
SPARK_Mode => Off
is
- Growth_Factor : constant := 2;
- -- When growing a container, multiply current capacity by this. Doubling
- -- leads to amortized linear-time copying.
-
type Int is range System.Min_Int .. System.Max_Int;
- procedure Free is
- new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr);
-
- type Maximal_Array_Ptr is access all Elements_Array (Array_Index)
- with Storage_Size => 0;
- type Maximal_Array_Ptr_Const is access constant Elements_Array (Array_Index)
- with Storage_Size => 0;
-
- function Elems (Container : in out Vector) return Maximal_Array_Ptr;
- function Elemsc
- (Container : Vector) return Maximal_Array_Ptr_Const;
- -- Returns a pointer to the Elements array currently in use -- either
- -- Container.Elements_Ptr or a pointer to Container.Elements. We work with
- -- pointers to a bogus array subtype that is constrained with the maximum
- -- possible bounds. This means that the pointer is a thin pointer. This is
- -- necessary because 'Unrestricted_Access doesn't work when it produces
- -- access-to-unconstrained and is returned from a function.
- --
- -- Note that this is dangerous: make sure calls to this use an indexed
- -- component or slice that is within the bounds 1 .. Length (Container).
-
- function Get_Element
- (Container : Vector;
- Position : Capacity_Range) return Element_Type;
-
function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base;
- function Current_Capacity (Container : Vector) return Capacity_Range;
-
procedure Insert_Space
(Container : in out Vector;
Before : Extended_Index;
end if;
for J in 1 .. Length (Left) loop
- if Get_Element (Left, J) /= Get_Element (Right, J) then
+ if Left.Elements (J) /= Right.Elements (J) then
return False;
end if;
end loop;
return;
end if;
- if Bounded and then Target.Capacity < LS then
+ if Target.Capacity < LS then
raise Constraint_Error;
end if;
function Capacity (Container : Vector) return Capacity_Range is
begin
- return
- (if Bounded then
- Container.Capacity
- else
- Capacity_Range'Last);
+ return Container.Capacity;
end Capacity;
-----------
procedure Clear (Container : in out Vector) is
begin
Container.Last := No_Index;
-
- -- Free element, note that this is OK if Elements_Ptr is null
-
- Free (Container.Elements_Ptr);
end Clear;
--------------
end if;
return Target : Vector (C) do
- Elems (Target) (1 .. LS) := Elemsc (Source) (1 .. LS);
+ Target.Elements (1 .. LS) := Source.Elements (1 .. LS);
Target.Last := Source.Last;
end return;
end Copy;
- ----------------------
- -- Current_Capacity --
- ----------------------
-
- function Current_Capacity (Container : Vector) return Capacity_Range is
- begin
- return
- (if Container.Elements_Ptr = null then
- Container.Elements'Length
- else
- Container.Elements_Ptr.all'Length);
- end Current_Capacity;
-
------------
-- Delete --
------------
-- so we just slide down to Index the elements that weren't deleted.
declare
- EA : Maximal_Array_Ptr renames Elems (Container);
+ EA : Elements_Array renames Container.Elements;
Idx : constant Count_Type := EA'First + Off;
begin
EA (Idx .. Old_Len - Count) := EA (Idx + Count .. Old_Len);
II : constant Int'Base := Int (Index) - Int (No_Index);
I : constant Capacity_Range := Capacity_Range (II);
begin
- return Get_Element (Container, I);
+ return Container.Elements (I);
end;
end Element;
- -----------
- -- Elems --
- -----------
-
- function Elems (Container : in out Vector) return Maximal_Array_Ptr is
- begin
- return
- (if Container.Elements_Ptr = null then
- Container.Elements'Unrestricted_Access
- else
- Container.Elements_Ptr.all'Unrestricted_Access);
- end Elems;
-
- function Elemsc (Container : Vector) return Maximal_Array_Ptr_Const is
- begin
- return
- (if Container.Elements_Ptr = null then
- Container.Elements'Unrestricted_Access
- else
- Container.Elements_Ptr.all'Unrestricted_Access);
- end Elemsc;
-
----------------
-- Find_Index --
----------------
begin
K := Capacity_Range (Int (Index) - Int (No_Index));
for Indx in Index .. Last loop
- if Get_Element (Container, K) = Item then
+ if Container.Elements (K) = Item then
return Indx;
end if;
if Is_Empty (Container) then
raise Constraint_Error with "Container is empty";
else
- return Get_Element (Container, 1);
+ return Container.Elements (1);
end if;
end First_Element;
begin
for Position in 1 .. Length (Container) loop
- R := M.Add (R, Elemsc (Container) (Position));
+ R := M.Add (R, Container.Elements (Position));
end loop;
return R;
begin
for J in 1 .. L - 1 loop
- if Get_Element (Container, J + 1) <
- Get_Element (Container, J)
+ if Container.Elements (J + 1) <
+ Container.Elements (J)
then
return False;
end if;
if Container.Last <= Index_Type'First then
return;
else
- Sort (Elems (Container) (1 .. Len));
+ Sort (Container.Elements (1 .. Len));
end if;
end Sort;
New_Length : constant Count_Type := I + Length (Source);
begin
- if not Bounded
- and then Current_Capacity (Target) < Capacity_Range (New_Length)
- then
- Reserve_Capacity
- (Target,
- Capacity_Range'Max
- (Current_Capacity (Target) * Growth_Factor,
- Capacity_Range (New_Length)));
- end if;
-
if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
Target.Last := No_Index + Index_Type'Base (New_Length);
end;
declare
- TA : Maximal_Array_Ptr renames Elems (Target);
- SA : Maximal_Array_Ptr renames Elems (Source);
+ TA : Elements_Array renames Target.Elements;
+ SA : Elements_Array renames Source.Elements;
begin
J := Length (Target);
end Generic_Sorting;
- -----------------
- -- Get_Element --
- -----------------
-
- function Get_Element
- (Container : Vector;
- Position : Capacity_Range) return Element_Type
- is
- begin
- return Elemsc (Container) (Position);
- end Get_Element;
-
-----------------
-- Has_Element --
-----------------
J := To_Array_Index (Before);
- Elems (Container) (J .. J - 1 + Count) := (others => New_Item);
+ Container.Elements (J .. J - 1 + Count) := (others => New_Item);
end Insert;
procedure Insert
B := To_Array_Index (Before);
- Elems (Container) (B .. B + N - 1) := Elemsc (New_Item) (1 .. N);
+ Container.Elements (B .. B + N - 1) := New_Item.Elements (1 .. N);
end Insert;
------------------
J := To_Array_Index (Before);
- -- Increase the capacity of container if needed
-
- if not Bounded
- and then Current_Capacity (Container) < Capacity_Range (New_Length)
- then
- Reserve_Capacity
- (Container,
- Capacity_Range'Max (Current_Capacity (Container) * Growth_Factor,
- Capacity_Range (New_Length)));
- end if;
-
declare
- EA : Maximal_Array_Ptr renames Elems (Container);
+ EA : Elements_Array renames Container.Elements;
begin
if Before <= Container.Last then
if Is_Empty (Container) then
raise Constraint_Error with "Container is empty";
else
- return Get_Element (Container, Length (Container));
+ return Container.Elements (Length (Container));
end if;
end Last_Element;
return;
end if;
- if Bounded and then Target.Capacity < LS then
+ if Target.Capacity < LS then
raise Constraint_Error;
end if;
I : constant Capacity_Range := Capacity_Range (II);
begin
- Elems (Container) (I) := New_Item;
+ Container.Elements (I) := New_Item;
end;
end Replace_Element;
Capacity : Capacity_Range)
is
begin
- if Bounded then
- if Capacity > Container.Capacity then
- raise Constraint_Error with "Capacity is out of range";
- end if;
-
- else
- if Capacity > Formal_Vectors.Current_Capacity (Container) then
- declare
- New_Elements : constant Elements_Array_Ptr :=
- new Elements_Array (1 .. Capacity);
- L : constant Capacity_Range := Length (Container);
-
- begin
- New_Elements (1 .. L) := Elemsc (Container) (1 .. L);
- Free (Container.Elements_Ptr);
- Container.Elements_Ptr := New_Elements;
- end;
- end if;
+ if Capacity > Container.Capacity then
+ raise Constraint_Error with "Capacity is out of range";
end if;
end Reserve_Capacity;
declare
I, J : Capacity_Range;
E : Elements_Array renames
- Elems (Container) (1 .. Length (Container));
+ Container.Elements (1 .. Length (Container));
begin
I := 1;
K := Capacity_Range (Int (Last) - Int (No_Index));
for Indx in reverse Index_Type'First .. Last loop
- if Get_Element (Container, K) = Item then
+ if Container.Elements (K) = Item then
return Indx;
end if;
II : constant Int'Base := Int (I) - Int (No_Index);
JJ : constant Int'Base := Int (J) - Int (No_Index);
- EI : Element_Type renames Elems (Container) (Capacity_Range (II));
- EJ : Element_Type renames Elems (Container) (Capacity_Range (JJ));
+ EI : Element_Type renames Container.Elements (Capacity_Range (II));
+ EJ : Element_Type renames Container.Elements (Capacity_Range (JJ));
EI_Copy : constant Element_Type := EI;
Last := Index_Type (Last_As_Int);
return
- (Capacity => Length,
- Last => Last,
- Elements_Ptr => <>,
- Elements => (others => New_Item));
+ (Capacity => Length,
+ Last => Last,
+ Elements => (others => New_Item));
end;
end To_Vector;
generic
type Index_Type is range <>;
type Element_Type is private;
-
- Bounded : Boolean := True;
- -- If True, the containers are bounded; the initial capacity is the maximum
- -- size, and heap allocation will be avoided. If False, the containers can
- -- grow via heap allocation.
-
package Ada.Containers.Formal_Vectors with
SPARK_Mode
is
subtype Capacity_Range is Count_Type range 0 .. Last_Count;
- type Vector (Capacity : Capacity_Range) is limited private with
+ type Vector (Capacity : Capacity_Range) is private with
Default_Initial_Condition => Is_Empty (Vector);
- -- In the bounded case, Capacity is the capacity of the container, which
- -- never changes. In the unbounded case, Capacity is the initial capacity
- -- of the container, and operations such as Reserve_Capacity and Append can
- -- increase the capacity. The capacity never shrinks, except in the case of
- -- Clear.
- --
- -- Note that all objects of type Vector are constrained, including in the
- -- unbounded case; you can't assign from one object to another if the
- -- Capacity is different.
function Length (Container : Vector) return Capacity_Range with
Global => null,
function Capacity (Container : Vector) return Capacity_Range with
Global => null,
Post =>
- Capacity'Result =
- (if Bounded then
- Container.Capacity
- else
- Capacity_Range'Last);
+ Capacity'Result = Container.Capacity;
pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
procedure Reserve_Capacity
Capacity : Capacity_Range)
with
Global => null,
- Pre => (if Bounded then Capacity <= Container.Capacity),
+ Pre => Capacity <= Container.Capacity,
Post => Model (Container) = Model (Container)'Old;
function Is_Empty (Container : Vector) return Boolean with
procedure Clear (Container : in out Vector) with
Global => null,
Post => Length (Container) = 0;
- -- Note that this reclaims storage in the unbounded case. You need to call
- -- this before a container goes out of scope in order to avoid storage
- -- leaks. In addition, "X := ..." can leak unless you Clear(X) first.
procedure Assign (Target : in out Vector; Source : Vector) with
Global => null,
- Pre => (if Bounded then Length (Source) <= Target.Capacity),
+ Pre => Length (Source) <= Target.Capacity,
Post => Model (Target) = Model (Source);
function Copy
Capacity : Capacity_Range := 0) return Vector
with
Global => null,
- Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)),
+ Pre => (Capacity = 0 or Length (Source) <= Capacity),
Post =>
Model (Copy'Result) = Model (Source)
and (if Capacity = 0 then
procedure Move (Target : in out Vector; Source : in out Vector)
with
Global => null,
- Pre => (if Bounded then Length (Source) <= Capacity (Target)),
+ Pre => Length (Source) <= Capacity (Target),
Post => Model (Target) = Model (Source)'Old and Length (Source) = 0;
function Element
type Elements_Array is array (Array_Index range <>) of Element_Type;
function "=" (L, R : Elements_Array) return Boolean is abstract;
- type Elements_Array_Ptr is access all Elements_Array;
-
- type Vector (Capacity : Capacity_Range) is limited record
-
- -- In the bounded case, the elements are stored in Elements. In the
- -- unbounded case, the elements are initially stored in Elements, until
- -- we run out of room, then we switch to Elements_Ptr.
-
- Last : Extended_Index := No_Index;
- Elements_Ptr : Elements_Array_Ptr := null;
- Elements : aliased Elements_Array (1 .. Capacity);
+ type Vector (Capacity : Capacity_Range) is record
+ Last : Extended_Index := No_Index;
+ Elements : Elements_Array (1 .. Capacity);
end record;
- -- The primary reason Vector is limited is that in the unbounded case, once
- -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will
- -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr,
- -- so for example "Append (X, ...);" will modify BOTH X and Y. That would
- -- allow SPARK to "prove" things that are false. We could fix that by
- -- making Vector a controlled type, and override Adjust to make a deep
- -- copy, but finalization is not allowed in SPARK.
- --
- -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not
- -- allowed on Vectors.
-
function Empty_Vector return Vector is
((Capacity => 0, others => <>));
projects / gcc.git / commitdiff