+2015-01-06 Bob Duff <duff@adacore.com>
+
+ * a-cfinve.adb (Copy): Set the discriminant to the Length when
+ Capacity = 0.
+ * a-cofove.ads (Capacity): Add a postcondition.
+ * a-cfinve.ads (Capacity): Add a postcondition.
+ (Reserve_Capacity): Correct the postcondition in the case where
+ Capacity = 0; that means "Capacity => Length (Container)".
+ * a-cofove.adb (Elems[c]): Add a comment
+ explaining the dangers and how to avoid them.
+
+2015-01-06 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch12.adb: Code clean up.
2015-01-06 Arnaud Charlet <charlet@adacore.com>
* gnatvsn.ads: Bump copyright year.
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
--- A D A . C O N T A I N E R S
--- . F O R M A L _ I N D E F I N I T E _ V E C T O R S --
+-- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS --
-- --
-- B o d y --
-- --
function Contains
(Container : Vector;
- Item : Element_Type) return Boolean is
+ Item : Element_Type) return Boolean
+ is
(Contains (Container.V, H (Item)));
----------
function Copy
(Source : Vector;
- Capacity : Capacity_Range := 0) return Vector is
- (Capacity, V => Copy (Source.V, Capacity));
+ Capacity : Capacity_Range := 0) return Vector
+ is
+ ((if Capacity = 0 then Length (Source) else Capacity),
+ V => Copy (Source.V, Capacity));
---------------------
-- Current_To_Last --
function Find_Index
(Container : Vector;
Item : Element_Type;
- Index : Index_Type := Index_Type'First) return Extended_Index is
+ Index : Index_Type := Index_Type'First) return Extended_Index
+ is
(Find_Index (Container.V, H (Item), Index));
-------------------
-----------------
function Has_Element
- (Container : Vector; Position : Extended_Index) return Boolean is
+ (Container : Vector;
+ Position : Extended_Index) return Boolean
+ is
(Has_Element (Container.V, Position));
--------------
function Reverse_Find_Index
(Container : Vector;
Item : Element_Type;
- Index : Index_Type := Index_Type'Last) return Extended_Index is
+ Index : Index_Type := Index_Type'Last) return Extended_Index
+ is
(Reverse_Find_Index (Container.V, H (Item), Index));
----------
function To_Vector
(New_Item : Element_Type;
- Length : Capacity_Range) return Vector is
+ Length : Capacity_Range) return Vector
+ is
begin
return (Length, To_Vector (H (New_Item), Length));
end To_Vector;
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
--- A D A . C O N T A I N E R S
--- . F O R M A L _ I N D E F I N I T E _ V E C T O R S --
+-- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS --
-- --
-- S p e c --
-- --
type Index_Type is range <>;
type Element_Type (<>) is private;
Max_Size_In_Storage_Elements : Natural :=
- Element_Type'Max_Size_In_Storage_Elements;
+ Element_Type'Max_Size_In_Storage_Elements;
-- This has the same meaning as in Ada.Containers.Bounded_Holders, with the
-- same restrictions.
Global => null;
function Capacity (Container : Vector) return Capacity_Range with
- Global => null;
+ Global => null,
+ Post => Capacity'Result >= Container.Capacity;
procedure Reserve_Capacity
(Container : in out Vector;
Capacity : Capacity_Range := 0) return Vector
with
Global => null,
- Pre => (if Bounded then Length (Source) <= Capacity);
+ Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity));
function Element
(Container : Vector;
New_Item : Vector)
with
Global => null,
- Pre => (if Bounded then
- Length (Container) + Length (New_Item) <= Container.Capacity);
+ Pre => (if Bounded
+ then Length (Container) + Length (New_Item) <=
+ Container.Capacity);
procedure Append
(Container : in out Vector;
New_Item : Element_Type)
with
Global => null,
- Pre => (if Bounded then
- Length (Container) < Container.Capacity);
+ Pre => (if Bounded
+ then Length (Container) < Container.Capacity);
procedure Delete_Last
(Container : in out Vector)
package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded);
use Def;
- -- ????Assert that Def subtypes have the same range.
+ -- ????Assert that Def subtypes have the same range
type Vector (Capacity : Capacity_Range) is limited record
V : Def.Vector (Capacity);
-- 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;
Global => null;
function Capacity (Container : Vector) return Capacity_Range with
- Global => null;
+ Global => null,
+ Post => Capacity'Result >= Container.Capacity;
procedure Reserve_Capacity
(Container : in out Vector;
(Defining_Entity (Analyzed_Formal)))
and then Ekind (Defining_Entity (Analyzed_Formal)) =
E_Function
+ and then Expander_Active
then
-- If actual is an entity (function or operator),
-- and expander is active, build wrapper for it.
-- Note that wrappers play no role within a generic.
- if Present (Match) and then Expander_Active then
+ if Present (Match) then
if Nkind (Match) = N_Operator_Symbol then
-- If the name is a default, find its visible
elsif Box_Present (Formal)
and then Nkind (Defining_Entity (Analyzed_Formal)) =
N_Defining_Operator_Symbol
- and then Expander_Active
then
Append_To (Assoc,
Build_Operator_Wrapper