[multiple changes]

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.

From-SVN: r219225

6 files changed, 48 insertions, 22 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6c1780d..b0b4b96 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,17 @@
+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.
diff --git a/gcc/ada/a-cfinve.adb b/gcc/ada/a-cfinve.adb
index 6574fcb..f088b9e 100644
--- a/gcc/ada/a-cfinve.adb
+++ b/gcc/ada/a-cfinve.adb
@@ -2,8 +2,7 @@
 --                                                                          --
 --                         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                                  --
 --                                                                          --
@@ -89,7 +88,8 @@ is
 
    function Contains
      (Container : Vector;
-      Item      : Element_Type) return Boolean is
+      Item      : Element_Type) return Boolean
+   is
      (Contains (Container.V, H (Item)));
 
    ----------
@@ -98,8 +98,10 @@ is
 
    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 --
@@ -139,7 +141,8 @@ is
    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));
 
    -------------------
@@ -200,7 +203,9 @@ is
    -----------------
 
    function Has_Element
-     (Container : Vector; Position : Extended_Index) return Boolean is
+     (Container : Vector;
+      Position  : Extended_Index) return Boolean
+   is
      (Has_Element (Container.V, Position));
 
    --------------
@@ -272,7 +277,8 @@ is
    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));
 
    ----------
@@ -290,7 +296,8 @@ is
 
    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;
diff --git a/gcc/ada/a-cfinve.ads b/gcc/ada/a-cfinve.ads
index b78633b..7559df6 100644
--- a/gcc/ada/a-cfinve.ads
+++ b/gcc/ada/a-cfinve.ads
@@ -2,8 +2,7 @@
 --                                                                          --
 --                         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                                  --
 --                                                                          --
@@ -41,7 +40,7 @@ generic
    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.
 
@@ -81,7 +80,8 @@ is
      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;
@@ -111,7 +111,7 @@ is
       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;
@@ -133,16 +133,17 @@ is
       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)
@@ -243,7 +244,7 @@ private
    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);
diff --git a/gcc/ada/a-cofove.adb b/gcc/ada/a-cofove.adb
index 9cfd132..ef37cc0 100644
--- a/gcc/ada/a-cofove.adb
+++ b/gcc/ada/a-cofove.adb
@@ -59,6 +59,9 @@ is
    --  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;
diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads
index 9e91bc8..3d4c1b3 100644
--- a/gcc/ada/a-cofove.ads
+++ b/gcc/ada/a-cofove.ads
@@ -84,7 +84,8 @@ is
      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;
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 6062a88..ab118c6 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -1804,12 +1804,13 @@ package body Sem_Ch12 is
                               (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
@@ -1837,7 +1838,6 @@ package body Sem_Ch12 is
                         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