[multiple changes]
2013-07-05 Claire Dross <dross@adacore.com> * a-cfdlli.ads, a-cfhama.ads, a-cfhase.ads, a-cforma.ads, a-cforse.ads, a-cofove.ads: Add preconditions when needed + container types are not tagged any more. 2013-07-05 Thomas Quinot <quinot@adacore.com> * freeze.adb (Freeze_Entity): For an object with captured initialization statements, do not remove Init_Stmts from the enclosing list, as Freeze_All might rely on it to know where to stop freezing. From-SVN: r200708
This commit is contained in:
parent
16788d44af
commit
a33f291d93
|
@ -1,3 +1,16 @@
|
|||
2013-07-05 Claire Dross <dross@adacore.com>
|
||||
|
||||
* a-cfdlli.ads, a-cfhama.ads, a-cfhase.ads, a-cforma.ads,
|
||||
a-cforse.ads, a-cofove.ads: Add preconditions when needed +
|
||||
container types are not tagged any more.
|
||||
|
||||
2013-07-05 Thomas Quinot <quinot@adacore.com>
|
||||
|
||||
* freeze.adb (Freeze_Entity): For an object with captured
|
||||
initialization statements, do not remove Init_Stmts from the
|
||||
enclosing list, as Freeze_All might rely on it to know where to
|
||||
stop freezing.
|
||||
|
||||
2013-07-05 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* exp_ch4.adb, a-cfdlli.ads, a-ngelfu.ads, s-bignum.adb: Minor
|
||||
|
|
|
@ -153,15 +153,11 @@ package Ada.Containers.Formal_Doubly_Linked_Lists is
|
|||
|
||||
procedure Delete_First
|
||||
(Container : in out List;
|
||||
Count : Count_Type := 1)
|
||||
with
|
||||
Pre => not Is_Empty (Container);
|
||||
Count : Count_Type := 1);
|
||||
|
||||
procedure Delete_Last
|
||||
(Container : in out List;
|
||||
Count : Count_Type := 1)
|
||||
with
|
||||
Pre => not Is_Empty (Container);
|
||||
Count : Count_Type := 1);
|
||||
|
||||
procedure Reverse_Elements (Container : in out List);
|
||||
|
||||
|
|
|
@ -64,7 +64,7 @@ generic
|
|||
package Ada.Containers.Formal_Hashed_Maps is
|
||||
pragma Pure;
|
||||
|
||||
type Map (Capacity : Count_Type; Modulus : Hash_Type) is tagged private;
|
||||
type Map (Capacity : Count_Type; Modulus : Hash_Type) is private;
|
||||
pragma Preelaborable_Initialization (Map);
|
||||
|
||||
type Cursor is private;
|
||||
|
@ -80,7 +80,9 @@ package Ada.Containers.Formal_Hashed_Maps is
|
|||
|
||||
procedure Reserve_Capacity
|
||||
(Container : in out Map;
|
||||
Capacity : Count_Type);
|
||||
Capacity : Count_Type)
|
||||
with
|
||||
Pre => Capacity <= Container.Capacity;
|
||||
|
||||
function Length (Container : Map) return Count_Type;
|
||||
|
||||
|
@ -88,67 +90,91 @@ package Ada.Containers.Formal_Hashed_Maps is
|
|||
|
||||
procedure Clear (Container : in out Map);
|
||||
|
||||
procedure Assign (Target : in out Map; Source : Map);
|
||||
procedure Assign (Target : in out Map; Source : Map) with
|
||||
Pre => Target.Capacity >= Length (Source);
|
||||
|
||||
-- Copy returns a container stricty equal to Source
|
||||
-- It must have the same cursors associated to each element
|
||||
-- Therefore:
|
||||
-- - capacity=0 means use container.capacity as cap of tgt
|
||||
-- - the modulus cannot be changed.
|
||||
function Copy
|
||||
(Source : Map;
|
||||
Capacity : Count_Type := 0) return Map;
|
||||
Capacity : Count_Type := 0) return Map
|
||||
with
|
||||
Pre => Capacity >= Source.Capacity;
|
||||
-- Copy returns a container stricty equal to Source. It must have
|
||||
-- the same cursors associated with each element. Therefore:
|
||||
-- - capacity=0 means use container.capacity as capacity of target
|
||||
-- - the modulus cannot be changed.
|
||||
|
||||
function Key (Container : Map; Position : Cursor) return Key_Type;
|
||||
function Key (Container : Map; Position : Cursor) return Key_Type with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
function Element (Container : Map; Position : Cursor) return Element_Type;
|
||||
function Element
|
||||
(Container : Map;
|
||||
Position : Cursor) return Element_Type
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Replace_Element
|
||||
(Container : in out Map;
|
||||
Position : Cursor;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Move (Target : in out Map; Source : in out Map);
|
||||
procedure Move (Target : in out Map; Source : in out Map) with
|
||||
Pre => Target.Capacity >= Length (Source);
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Map;
|
||||
Key : Key_Type;
|
||||
New_Item : Element_Type;
|
||||
Position : out Cursor;
|
||||
Inserted : out Boolean);
|
||||
Inserted : out Boolean)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Map;
|
||||
Key : Key_Type;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity
|
||||
and then (not Contains (Container, Key));
|
||||
|
||||
procedure Include
|
||||
(Container : in out Map;
|
||||
Key : Key_Type;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Replace
|
||||
(Container : in out Map;
|
||||
Key : Key_Type;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Contains (Container, Key);
|
||||
|
||||
procedure Exclude (Container : in out Map; Key : Key_Type);
|
||||
|
||||
procedure Delete (Container : in out Map; Key : Key_Type);
|
||||
procedure Delete (Container : in out Map; Key : Key_Type) with
|
||||
Pre => Contains (Container, Key);
|
||||
|
||||
procedure Delete (Container : in out Map; Position : in out Cursor);
|
||||
procedure Delete (Container : in out Map; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
function First (Container : Map) return Cursor;
|
||||
|
||||
function Next (Container : Map; Position : Cursor) return Cursor;
|
||||
function Next (Container : Map; Position : Cursor) return Cursor with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
procedure Next (Container : Map; Position : in out Cursor);
|
||||
procedure Next (Container : Map; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Find (Container : Map; Key : Key_Type) return Cursor;
|
||||
|
||||
function Contains (Container : Map; Key : Key_Type) return Boolean;
|
||||
|
||||
function Element (Container : Map; Key : Key_Type) return Element_Type;
|
||||
function Element (Container : Map; Key : Key_Type) return Element_Type with
|
||||
Pre => Contains (Container, Key);
|
||||
|
||||
function Has_Element (Container : Map; Position : Cursor) return Boolean;
|
||||
|
||||
|
@ -175,8 +201,10 @@ package Ada.Containers.Formal_Hashed_Maps is
|
|||
-- they are structurally equal (function "=" returns True) and that they
|
||||
-- have the same set of cursors.
|
||||
|
||||
function Left (Container : Map; Position : Cursor) return Map;
|
||||
function Right (Container : Map; Position : Cursor) return Map;
|
||||
function Left (Container : Map; Position : Cursor) return Map with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
function Right (Container : Map; Position : Cursor) return Map with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
-- Left returns a container containing all elements preceding Position
|
||||
-- (excluded) in Container. Right returns a container containing all
|
||||
-- elements following Position (included) in Container. These two new
|
||||
|
|
|
@ -66,7 +66,7 @@ generic
|
|||
package Ada.Containers.Formal_Hashed_Sets is
|
||||
pragma Pure;
|
||||
|
||||
type Set (Capacity : Count_Type; Modulus : Hash_Type) is tagged private;
|
||||
type Set (Capacity : Count_Type; Modulus : Hash_Type) is private;
|
||||
pragma Preelaborable_Initialization (Set);
|
||||
|
||||
type Cursor is private;
|
||||
|
@ -86,7 +86,9 @@ package Ada.Containers.Formal_Hashed_Sets is
|
|||
|
||||
procedure Reserve_Capacity
|
||||
(Container : in out Set;
|
||||
Capacity : Count_Type);
|
||||
Capacity : Count_Type)
|
||||
with
|
||||
Pre => Capacity <= Container.Capacity;
|
||||
|
||||
function Length (Container : Set) return Count_Type;
|
||||
|
||||
|
@ -94,39 +96,60 @@ package Ada.Containers.Formal_Hashed_Sets is
|
|||
|
||||
procedure Clear (Container : in out Set);
|
||||
|
||||
procedure Assign (Target : in out Set; Source : Set);
|
||||
procedure Assign (Target : in out Set; Source : Set) with
|
||||
Pre => Target.Capacity >= Length (Source);
|
||||
|
||||
function Copy (Source : Set;
|
||||
Capacity : Count_Type := 0) return Set;
|
||||
function Copy
|
||||
(Source : Set;
|
||||
Capacity : Count_Type := 0) return Set
|
||||
with
|
||||
Pre => Capacity >= Source.Capacity;
|
||||
|
||||
function Element (Container : Set; Position : Cursor) return Element_Type;
|
||||
function Element
|
||||
(Container : Set;
|
||||
Position : Cursor) return Element_Type
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Replace_Element
|
||||
(Container : in out Set;
|
||||
Position : Cursor;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Move (Target : in out Set; Source : in out Set);
|
||||
procedure Move (Target : in out Set; Source : in out Set) with
|
||||
Pre => Target.Capacity >= Length (Source);
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Set;
|
||||
New_Item : Element_Type;
|
||||
Position : out Cursor;
|
||||
Inserted : out Boolean);
|
||||
Inserted : out Boolean)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Insert (Container : in out Set; New_Item : Element_Type);
|
||||
procedure Insert (Container : in out Set; New_Item : Element_Type) with
|
||||
Pre => Length (Container) < Container.Capacity
|
||||
and then (not Contains (Container, New_Item));
|
||||
|
||||
procedure Include (Container : in out Set; New_Item : Element_Type);
|
||||
procedure Include (Container : in out Set; New_Item : Element_Type) with
|
||||
Pre => Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Replace (Container : in out Set; New_Item : Element_Type);
|
||||
procedure Replace (Container : in out Set; New_Item : Element_Type) with
|
||||
Pre => Contains (Container, New_Item);
|
||||
|
||||
procedure Exclude (Container : in out Set; Item : Element_Type);
|
||||
|
||||
procedure Delete (Container : in out Set; Item : Element_Type);
|
||||
procedure Delete (Container : in out Set; Item : Element_Type) with
|
||||
Pre => Contains (Container, Item);
|
||||
|
||||
procedure Delete (Container : in out Set; Position : in out Cursor);
|
||||
procedure Delete (Container : in out Set; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Union (Target : in out Set; Source : Set);
|
||||
procedure Union (Target : in out Set; Source : Set) with
|
||||
Pre => Length (Target) + Length (Source) -
|
||||
Length (Intersection (Target, Source)) <= Target.Capacity;
|
||||
|
||||
function Union (Left, Right : Set) return Set;
|
||||
|
||||
|
@ -149,7 +172,7 @@ package Ada.Containers.Formal_Hashed_Sets is
|
|||
function Symmetric_Difference (Left, Right : Set) return Set;
|
||||
|
||||
function "xor" (Left, Right : Set) return Set
|
||||
renames Symmetric_Difference;
|
||||
renames Symmetric_Difference;
|
||||
|
||||
function Overlap (Left, Right : Set) return Boolean;
|
||||
|
||||
|
@ -157,9 +180,11 @@ package Ada.Containers.Formal_Hashed_Sets is
|
|||
|
||||
function First (Container : Set) return Cursor;
|
||||
|
||||
function Next (Container : Set; Position : Cursor) return Cursor;
|
||||
function Next (Container : Set; Position : Cursor) return Cursor with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
procedure Next (Container : Set; Position : in out Cursor);
|
||||
procedure Next (Container : Set; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Find
|
||||
(Container : Set;
|
||||
|
@ -217,8 +242,10 @@ package Ada.Containers.Formal_Hashed_Sets is
|
|||
-- they are structurally equal (function "=" returns True) and that they
|
||||
-- have the same set of cursors.
|
||||
|
||||
function Left (Container : Set; Position : Cursor) return Set;
|
||||
function Right (Container : Set; Position : Cursor) return Set;
|
||||
function Left (Container : Set; Position : Cursor) return Set with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
function Right (Container : Set; Position : Cursor) return Set with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
-- Left returns a container containing all elements preceding Position
|
||||
-- (excluded) in Container. Right returns a container containing all
|
||||
-- elements following Position (included) in Container. These two new
|
||||
|
|
|
@ -67,7 +67,7 @@ package Ada.Containers.Formal_Ordered_Maps is
|
|||
|
||||
function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
|
||||
|
||||
type Map (Capacity : Count_Type) is tagged private;
|
||||
type Map (Capacity : Count_Type) is private;
|
||||
pragma Preelaborable_Initialization (Map);
|
||||
|
||||
type Cursor is private;
|
||||
|
@ -85,48 +85,69 @@ package Ada.Containers.Formal_Ordered_Maps is
|
|||
|
||||
procedure Clear (Container : in out Map);
|
||||
|
||||
procedure Assign (Target : in out Map; Source : Map);
|
||||
procedure Assign (Target : in out Map; Source : Map) with
|
||||
Pre => Target.Capacity >= Length (Source);
|
||||
|
||||
function Copy (Source : Map; Capacity : Count_Type := 0) return Map;
|
||||
function Copy (Source : Map; Capacity : Count_Type := 0) return Map with
|
||||
Pre => Capacity >= Source.Capacity;
|
||||
|
||||
function Key (Container : Map; Position : Cursor) return Key_Type;
|
||||
function Key (Container : Map; Position : Cursor) return Key_Type with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
function Element (Container : Map; Position : Cursor) return Element_Type;
|
||||
function Element
|
||||
(Container : Map;
|
||||
Position : Cursor) return Element_Type
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Replace_Element
|
||||
(Container : in out Map;
|
||||
Position : Cursor;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Move (Target : in out Map; Source : in out Map);
|
||||
procedure Move (Target : in out Map; Source : in out Map) with
|
||||
Pre => Target.Capacity >= Length (Source);
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Map;
|
||||
Key : Key_Type;
|
||||
New_Item : Element_Type;
|
||||
Position : out Cursor;
|
||||
Inserted : out Boolean);
|
||||
Inserted : out Boolean)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Map;
|
||||
Key : Key_Type;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity
|
||||
and then (not Contains (Container, Key));
|
||||
|
||||
procedure Include
|
||||
(Container : in out Map;
|
||||
Key : Key_Type;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Replace
|
||||
(Container : in out Map;
|
||||
Key : Key_Type;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Contains (Container, Key);
|
||||
|
||||
procedure Exclude (Container : in out Map; Key : Key_Type);
|
||||
|
||||
procedure Delete (Container : in out Map; Key : Key_Type);
|
||||
procedure Delete (Container : in out Map; Key : Key_Type) with
|
||||
Pre => Contains (Container, Key);
|
||||
|
||||
procedure Delete (Container : in out Map; Position : in out Cursor);
|
||||
procedure Delete (Container : in out Map; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Delete_First (Container : in out Map);
|
||||
|
||||
|
@ -134,27 +155,36 @@ package Ada.Containers.Formal_Ordered_Maps is
|
|||
|
||||
function First (Container : Map) return Cursor;
|
||||
|
||||
function First_Element (Container : Map) return Element_Type;
|
||||
function First_Element (Container : Map) return Element_Type with
|
||||
Pre => not Is_Empty (Container);
|
||||
|
||||
function First_Key (Container : Map) return Key_Type;
|
||||
function First_Key (Container : Map) return Key_Type with
|
||||
Pre => not Is_Empty (Container);
|
||||
|
||||
function Last (Container : Map) return Cursor;
|
||||
|
||||
function Last_Element (Container : Map) return Element_Type;
|
||||
function Last_Element (Container : Map) return Element_Type with
|
||||
Pre => not Is_Empty (Container);
|
||||
|
||||
function Last_Key (Container : Map) return Key_Type;
|
||||
function Last_Key (Container : Map) return Key_Type with
|
||||
Pre => not Is_Empty (Container);
|
||||
|
||||
function Next (Container : Map; Position : Cursor) return Cursor;
|
||||
function Next (Container : Map; Position : Cursor) return Cursor with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
procedure Next (Container : Map; Position : in out Cursor);
|
||||
procedure Next (Container : Map; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Previous (Container : Map; Position : Cursor) return Cursor;
|
||||
function Previous (Container : Map; Position : Cursor) return Cursor with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
procedure Previous (Container : Map; Position : in out Cursor);
|
||||
procedure Previous (Container : Map; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Find (Container : Map; Key : Key_Type) return Cursor;
|
||||
|
||||
function Element (Container : Map; Key : Key_Type) return Element_Type;
|
||||
function Element (Container : Map; Key : Key_Type) return Element_Type with
|
||||
Pre => Contains (Container, Key);
|
||||
|
||||
function Floor (Container : Map; Key : Key_Type) return Cursor;
|
||||
|
||||
|
@ -169,8 +199,10 @@ package Ada.Containers.Formal_Ordered_Maps is
|
|||
-- they are structurally equal (function "=" returns True) and that they
|
||||
-- have the same set of cursors.
|
||||
|
||||
function Left (Container : Map; Position : Cursor) return Map;
|
||||
function Right (Container : Map; Position : Cursor) return Map;
|
||||
function Left (Container : Map; Position : Cursor) return Map with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
function Right (Container : Map; Position : Cursor) return Map with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
-- Left returns a container containing all elements preceding Position
|
||||
-- (excluded) in Container. Right returns a container containing all
|
||||
-- elements following Position (included) in Container. These two new
|
||||
|
|
|
@ -65,9 +65,8 @@ package Ada.Containers.Formal_Ordered_Sets is
|
|||
|
||||
function Equivalent_Elements (Left, Right : Element_Type) return Boolean;
|
||||
|
||||
type Set (Capacity : Count_Type) is tagged private;
|
||||
-- why is this commented out ???
|
||||
-- pragma Preelaborable_Initialization (Set);
|
||||
type Set (Capacity : Count_Type) is private;
|
||||
pragma Preelaborable_Initialization (Set);
|
||||
|
||||
type Cursor is private;
|
||||
pragma Preelaborable_Initialization (Cursor);
|
||||
|
@ -88,36 +87,54 @@ package Ada.Containers.Formal_Ordered_Sets is
|
|||
|
||||
procedure Clear (Container : in out Set);
|
||||
|
||||
procedure Assign (Target : in out Set; Source : Set);
|
||||
procedure Assign (Target : in out Set; Source : Set) with
|
||||
Pre => Target.Capacity >= Length (Source);
|
||||
|
||||
function Copy (Source : Set; Capacity : Count_Type := 0) return Set;
|
||||
function Copy (Source : Set; Capacity : Count_Type := 0) return Set with
|
||||
Pre => Capacity >= Source.Capacity;
|
||||
|
||||
function Element (Container : Set; Position : Cursor) return Element_Type;
|
||||
function Element
|
||||
(Container : Set;
|
||||
Position : Cursor) return Element_Type
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Replace_Element
|
||||
(Container : in out Set;
|
||||
Position : Cursor;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Move (Target : in out Set; Source : in out Set);
|
||||
procedure Move (Target : in out Set; Source : in out Set) with
|
||||
Pre => Target.Capacity >= Length (Source);
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Set;
|
||||
New_Item : Element_Type;
|
||||
Position : out Cursor;
|
||||
Inserted : out Boolean);
|
||||
Inserted : out Boolean)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Set;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity
|
||||
and then (not Contains (Container, New_Item));
|
||||
|
||||
procedure Include
|
||||
(Container : in out Set;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Replace
|
||||
(Container : in out Set;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Contains (Container, New_Item);
|
||||
|
||||
procedure Exclude
|
||||
(Container : in out Set;
|
||||
|
@ -125,17 +142,23 @@ package Ada.Containers.Formal_Ordered_Sets is
|
|||
|
||||
procedure Delete
|
||||
(Container : in out Set;
|
||||
Item : Element_Type);
|
||||
Item : Element_Type)
|
||||
with
|
||||
Pre => Contains (Container, Item);
|
||||
|
||||
procedure Delete
|
||||
(Container : in out Set;
|
||||
Position : in out Cursor);
|
||||
Position : in out Cursor)
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Delete_First (Container : in out Set);
|
||||
|
||||
procedure Delete_Last (Container : in out Set);
|
||||
|
||||
procedure Union (Target : in out Set; Source : Set);
|
||||
procedure Union (Target : in out Set; Source : Set) with
|
||||
Pre => Length (Target) + Length (Source) -
|
||||
Length (Intersection (Target, Source)) <= Target.Capacity;
|
||||
|
||||
function Union (Left, Right : Set) return Set;
|
||||
|
||||
|
@ -165,19 +188,25 @@ package Ada.Containers.Formal_Ordered_Sets is
|
|||
|
||||
function First (Container : Set) return Cursor;
|
||||
|
||||
function First_Element (Container : Set) return Element_Type;
|
||||
function First_Element (Container : Set) return Element_Type with
|
||||
Pre => not Is_Empty (Container);
|
||||
|
||||
function Last (Container : Set) return Cursor;
|
||||
|
||||
function Last_Element (Container : Set) return Element_Type;
|
||||
function Last_Element (Container : Set) return Element_Type with
|
||||
Pre => not Is_Empty (Container);
|
||||
|
||||
function Next (Container : Set; Position : Cursor) return Cursor;
|
||||
function Next (Container : Set; Position : Cursor) return Cursor with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
procedure Next (Container : Set; Position : in out Cursor);
|
||||
procedure Next (Container : Set; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Previous (Container : Set; Position : Cursor) return Cursor;
|
||||
function Previous (Container : Set; Position : Cursor) return Cursor with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
procedure Previous (Container : Set; Position : in out Cursor);
|
||||
procedure Previous (Container : Set; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Find (Container : Set; Item : Element_Type) return Cursor;
|
||||
|
||||
|
@ -228,8 +257,10 @@ package Ada.Containers.Formal_Ordered_Sets is
|
|||
-- they are structurally equal (function "=" returns True) and that they
|
||||
-- have the same set of cursors.
|
||||
|
||||
function Left (Container : Set; Position : Cursor) return Set;
|
||||
function Right (Container : Set; Position : Cursor) return Set;
|
||||
function Left (Container : Set; Position : Cursor) return Set with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
function Right (Container : Set; Position : Cursor) return Set with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
-- Left returns a container containing all elements preceding Position
|
||||
-- (excluded) in Container. Right returns a container containing all
|
||||
-- elements following Position (included) in Container. These two new
|
||||
|
|
|
@ -251,7 +251,7 @@ package body Ada.Containers.Formal_Vectors is
|
|||
raise Constraint_Error;
|
||||
end if;
|
||||
|
||||
Target.Clear;
|
||||
Clear (Target);
|
||||
|
||||
Target.Elements (1 .. LS) := Source.Elements (1 .. LS);
|
||||
Target.Last := Source.Last;
|
||||
|
@ -641,10 +641,10 @@ package body Ada.Containers.Formal_Vectors is
|
|||
-- I think we're missing this check in a-convec.adb... ???
|
||||
|
||||
I := Length (Target);
|
||||
Target.Set_Length (I + Length (Source));
|
||||
Set_Length (Target, I + Length (Source));
|
||||
|
||||
J := Length (Target);
|
||||
while not Source.Is_Empty loop
|
||||
while not Is_Empty (Source) loop
|
||||
pragma Assert (Length (Source) <= 1
|
||||
or else not (SA (Length (Source)) <
|
||||
SA (Length (Source) - 1)));
|
||||
|
@ -1487,20 +1487,20 @@ package body Ada.Containers.Formal_Vectors is
|
|||
|
||||
procedure Set_Length
|
||||
(Container : in out Vector;
|
||||
Length : Count_Type)
|
||||
New_Length : Count_Type)
|
||||
is
|
||||
begin
|
||||
if Length = Formal_Vectors.Length (Container) then
|
||||
if New_Length = Formal_Vectors.Length (Container) then
|
||||
return;
|
||||
end if;
|
||||
|
||||
if Length > Container.Capacity then
|
||||
if New_Length > Container.Capacity then
|
||||
raise Constraint_Error; -- ???
|
||||
end if;
|
||||
|
||||
declare
|
||||
Last_As_Int : constant Int'Base :=
|
||||
Int (Index_Type'First) + Int (Length) - 1;
|
||||
Int (Index_Type'First) + Int (New_Length) - 1;
|
||||
begin
|
||||
Container.Last := Index_Type'Base (Last_As_Int);
|
||||
end;
|
||||
|
|
|
@ -73,7 +73,7 @@ package Ada.Containers.Formal_Vectors is
|
|||
|
||||
No_Index : constant Extended_Index := Extended_Index'First;
|
||||
|
||||
type Vector (Capacity : Count_Type) is tagged private;
|
||||
type Vector (Capacity : Count_Type) is private;
|
||||
|
||||
type Cursor is private;
|
||||
pragma Preelaborable_Initialization (Cursor);
|
||||
|
@ -100,23 +100,30 @@ package Ada.Containers.Formal_Vectors is
|
|||
|
||||
procedure Reserve_Capacity
|
||||
(Container : in out Vector;
|
||||
Capacity : Count_Type);
|
||||
Capacity : Count_Type)
|
||||
with
|
||||
Pre => Capacity <= Container.Capacity;
|
||||
|
||||
function Length (Container : Vector) return Count_Type;
|
||||
|
||||
procedure Set_Length
|
||||
(Container : in out Vector;
|
||||
Length : Count_Type);
|
||||
New_Length : Count_Type)
|
||||
with
|
||||
Pre => New_Length <= Length (Container);
|
||||
|
||||
function Is_Empty (Container : Vector) return Boolean;
|
||||
|
||||
procedure Clear (Container : in out Vector);
|
||||
|
||||
procedure Assign (Target : in out Vector; Source : Vector);
|
||||
procedure Assign (Target : in out Vector; Source : Vector) with
|
||||
Pre => Length (Source) <= Target.Capacity;
|
||||
|
||||
function Copy
|
||||
(Source : Vector;
|
||||
Capacity : Count_Type := 0) return Vector;
|
||||
Capacity : Count_Type := 0) return Vector
|
||||
with
|
||||
Pre => Length (Source) <= Capacity;
|
||||
|
||||
function To_Cursor
|
||||
(Container : Vector;
|
||||
|
@ -126,86 +133,134 @@ package Ada.Containers.Formal_Vectors is
|
|||
|
||||
function Element
|
||||
(Container : Vector;
|
||||
Index : Index_Type) return Element_Type;
|
||||
Index : Index_Type) return Element_Type
|
||||
with
|
||||
Pre => First_Index (Container) <= Index
|
||||
and then Index <= Last_Index (Container);
|
||||
|
||||
function Element
|
||||
(Container : Vector;
|
||||
Position : Cursor) return Element_Type;
|
||||
Position : Cursor) return Element_Type
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Replace_Element
|
||||
(Container : in out Vector;
|
||||
Index : Index_Type;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => First_Index (Container) <= Index
|
||||
and then Index <= Last_Index (Container);
|
||||
|
||||
procedure Replace_Element
|
||||
(Container : in out Vector;
|
||||
Position : Cursor;
|
||||
New_Item : Element_Type);
|
||||
New_Item : Element_Type)
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Move (Target : in out Vector; Source : in out Vector);
|
||||
procedure Move (Target : in out Vector; Source : in out Vector) with
|
||||
Pre => Length (Source) <= Target.Capacity;
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Vector;
|
||||
Before : Extended_Index;
|
||||
New_Item : Vector);
|
||||
New_Item : Vector)
|
||||
with
|
||||
Pre => First_Index (Container) <= Before
|
||||
and then Before <= Last_Index (Container) + 1
|
||||
and then Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Vector;
|
||||
Before : Cursor;
|
||||
New_Item : Vector);
|
||||
New_Item : Vector)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity
|
||||
and then (Has_Element (Container, Before)
|
||||
or else Before = No_Element);
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Vector;
|
||||
Before : Cursor;
|
||||
New_Item : Vector;
|
||||
Position : out Cursor);
|
||||
Position : out Cursor)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity
|
||||
and then (Has_Element (Container, Before)
|
||||
or else Before = No_Element);
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Vector;
|
||||
Before : Extended_Index;
|
||||
New_Item : Element_Type;
|
||||
Count : Count_Type := 1);
|
||||
Count : Count_Type := 1)
|
||||
with
|
||||
Pre => First_Index (Container) <= Before
|
||||
and then Before <= Last_Index (Container) + 1
|
||||
and then Length (Container) + Count <= Container.Capacity;
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Vector;
|
||||
Before : Cursor;
|
||||
New_Item : Element_Type;
|
||||
Count : Count_Type := 1);
|
||||
Count : Count_Type := 1)
|
||||
with
|
||||
Pre => Length (Container) + Count <= Container.Capacity
|
||||
and then (Has_Element (Container, Before)
|
||||
or else Before = No_Element);
|
||||
|
||||
procedure Insert
|
||||
(Container : in out Vector;
|
||||
Before : Cursor;
|
||||
New_Item : Element_Type;
|
||||
Position : out Cursor;
|
||||
Count : Count_Type := 1);
|
||||
Count : Count_Type := 1)
|
||||
with
|
||||
Pre => Length (Container) + Count <= Container.Capacity
|
||||
and then (Has_Element (Container, Before)
|
||||
or else Before = No_Element);
|
||||
|
||||
procedure Prepend
|
||||
(Container : in out Vector;
|
||||
New_Item : Vector);
|
||||
New_Item : Vector)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Prepend
|
||||
(Container : in out Vector;
|
||||
New_Item : Element_Type;
|
||||
Count : Count_Type := 1);
|
||||
Count : Count_Type := 1)
|
||||
with
|
||||
Pre => Length (Container) + Count <= Container.Capacity;
|
||||
|
||||
procedure Append
|
||||
(Container : in out Vector;
|
||||
New_Item : Vector);
|
||||
New_Item : Vector)
|
||||
with
|
||||
Pre => Length (Container) < Container.Capacity;
|
||||
|
||||
procedure Append
|
||||
(Container : in out Vector;
|
||||
New_Item : Element_Type;
|
||||
Count : Count_Type := 1);
|
||||
Count : Count_Type := 1)
|
||||
with
|
||||
Pre => Length (Container) + Count <= Container.Capacity;
|
||||
|
||||
procedure Delete
|
||||
(Container : in out Vector;
|
||||
Index : Extended_Index;
|
||||
Count : Count_Type := 1);
|
||||
Count : Count_Type := 1)
|
||||
with
|
||||
Pre => First_Index (Container) <= Index
|
||||
and then Index <= Last_Index (Container) + 1;
|
||||
|
||||
procedure Delete
|
||||
(Container : in out Vector;
|
||||
Position : in out Cursor;
|
||||
Count : Count_Type := 1);
|
||||
Count : Count_Type := 1)
|
||||
with
|
||||
Pre => Has_Element (Container, Position);
|
||||
|
||||
procedure Delete_First
|
||||
(Container : in out Vector;
|
||||
|
@ -217,29 +272,39 @@ package Ada.Containers.Formal_Vectors is
|
|||
|
||||
procedure Reverse_Elements (Container : in out Vector);
|
||||
|
||||
procedure Swap (Container : in out Vector; I, J : Index_Type);
|
||||
procedure Swap (Container : in out Vector; I, J : Index_Type) with
|
||||
Pre => First_Index (Container) <= I and then I <= Last_Index (Container)
|
||||
and then First_Index (Container) <= J
|
||||
and then J <= Last_Index (Container);
|
||||
|
||||
procedure Swap (Container : in out Vector; I, J : Cursor);
|
||||
procedure Swap (Container : in out Vector; I, J : Cursor) with
|
||||
Pre => Has_Element (Container, I) and then Has_Element (Container, J);
|
||||
|
||||
function First_Index (Container : Vector) return Index_Type;
|
||||
|
||||
function First (Container : Vector) return Cursor;
|
||||
|
||||
function First_Element (Container : Vector) return Element_Type;
|
||||
function First_Element (Container : Vector) return Element_Type with
|
||||
Pre => not Is_Empty (Container);
|
||||
|
||||
function Last_Index (Container : Vector) return Extended_Index;
|
||||
|
||||
function Last (Container : Vector) return Cursor;
|
||||
|
||||
function Last_Element (Container : Vector) return Element_Type;
|
||||
function Last_Element (Container : Vector) return Element_Type with
|
||||
Pre => not Is_Empty (Container);
|
||||
|
||||
function Next (Container : Vector; Position : Cursor) return Cursor;
|
||||
function Next (Container : Vector; Position : Cursor) return Cursor with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
procedure Next (Container : Vector; Position : in out Cursor);
|
||||
procedure Next (Container : Vector; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Previous (Container : Vector; Position : Cursor) return Cursor;
|
||||
function Previous (Container : Vector; Position : Cursor) return Cursor with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
procedure Previous (Container : Vector; Position : in out Cursor);
|
||||
procedure Previous (Container : Vector; Position : in out Cursor) with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Find_Index
|
||||
(Container : Vector;
|
||||
|
@ -249,7 +314,9 @@ package Ada.Containers.Formal_Vectors is
|
|||
function Find
|
||||
(Container : Vector;
|
||||
Item : Element_Type;
|
||||
Position : Cursor := No_Element) return Cursor;
|
||||
Position : Cursor := No_Element) return Cursor
|
||||
with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Reverse_Find_Index
|
||||
(Container : Vector;
|
||||
|
@ -259,7 +326,9 @@ package Ada.Containers.Formal_Vectors is
|
|||
function Reverse_Find
|
||||
(Container : Vector;
|
||||
Item : Element_Type;
|
||||
Position : Cursor := No_Element) return Cursor;
|
||||
Position : Cursor := No_Element) return Cursor
|
||||
with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Contains
|
||||
(Container : Vector;
|
||||
|
@ -279,9 +348,11 @@ package Ada.Containers.Formal_Vectors is
|
|||
|
||||
end Generic_Sorting;
|
||||
|
||||
function Left (Container : Vector; Position : Cursor) return Vector;
|
||||
function Left (Container : Vector; Position : Cursor) return Vector with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
function Right (Container : Vector; Position : Cursor) return Vector;
|
||||
function Right (Container : Vector; Position : Cursor) return Vector with
|
||||
Pre => Has_Element (Container, Position) or else Position = No_Element;
|
||||
|
||||
private
|
||||
|
||||
|
@ -298,7 +369,7 @@ private
|
|||
type Elements_Array is array (Count_Type range <>) of Element_Type;
|
||||
function "=" (L, R : Elements_Array) return Boolean is abstract;
|
||||
|
||||
type Vector (Capacity : Count_Type) is tagged record
|
||||
type Vector (Capacity : Count_Type) is record
|
||||
Elements : Elements_Array (1 .. Capacity);
|
||||
Last : Extended_Index := No_Index;
|
||||
end record;
|
||||
|
|
|
@ -3360,7 +3360,16 @@ package body Freeze is
|
|||
and then Nkind (Expression (Init_Stmts)) = N_Null_Statement
|
||||
then
|
||||
Insert_List_Before (Init_Stmts, Actions (Init_Stmts));
|
||||
Remove (Init_Stmts);
|
||||
|
||||
-- Note that we rewrite Init_Stmts into a NULL statement,
|
||||
-- rather than just removing it, because Freeze_All may
|
||||
-- depend on this particular Node_Id still being present
|
||||
-- in the enclosing list to signal where to stop
|
||||
-- freezing.
|
||||
|
||||
Rewrite (Init_Stmts,
|
||||
Make_Null_Statement (Sloc (Init_Stmts)));
|
||||
|
||||
Set_Initialization_Statements (E, Empty);
|
||||
end if;
|
||||
end;
|
||||
|
|
Loading…
Reference in New Issue