+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
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);
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;
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;
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;
-- 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
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;
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;
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;
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;
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;
-- 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
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;
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);
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;
-- 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
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);
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;
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;
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;
-- 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
raise Constraint_Error;
end if;
- Target.Clear;
+ Clear (Target);
Target.Elements (1 .. LS) := Source.Elements (1 .. LS);
Target.Last := Source.Last;
-- 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)));
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;
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);
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;
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;
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;
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;
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;
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
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;
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;