[multiple changes]

2014-02-19  Ed Schonberg  <schonberg@adacore.com>

	* sem_util.ads, sem_util.adb (Get_Cursor_Type): Moved to sem_util
	from sem_ch13, for use elsewhere.
	* sem_ch13.adb (Get_Cursor_Type): Moved to sem_util.
	* sem_ch5.adb (Analyze_Iterator_Specification): Set properly the
	cursor type on the loop variable when the iteration is over o
	formal container.

2014-02-19  Vincent Celier  <celier@adacore.com>

	* prj-conf.adb (Add_Default_GNAT_Naming_Scheme): Add declaration
	for an empty Target (Check_Target): Never fail when an empty
	target is declared in the configuration project.

2014-02-19  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb (Check_Arg_Is_Local_Name): Argument is local if
	the pragma comes fron a predicate aspect and the context is a
	record declaration within the scope that declares the type.

2014-02-19  Robert Dewar  <dewar@adacore.com>

	* gnat_rm.texi: Minor clarifications.
	* expander.adb, sem_aggr.adb: Add comments.

From-SVN: r207903

10 files changed, 194 insertions, 109 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 583e37e..55b0724 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,31 @@
 2014-02-19  Ed Schonberg  <schonberg@adacore.com>
 
+	* sem_util.ads, sem_util.adb (Get_Cursor_Type): Moved to sem_util
+	from sem_ch13, for use elsewhere.
+	* sem_ch13.adb (Get_Cursor_Type): Moved to sem_util.
+	* sem_ch5.adb (Analyze_Iterator_Specification): Set properly the
+	cursor type on the loop variable when the iteration is over o
+	formal container.
+
+2014-02-19  Vincent Celier  <celier@adacore.com>
+
+	* prj-conf.adb (Add_Default_GNAT_Naming_Scheme): Add declaration
+	for an empty Target (Check_Target): Never fail when an empty
+	target is declared in the configuration project.
+
+2014-02-19  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_prag.adb (Check_Arg_Is_Local_Name): Argument is local if
+	the pragma comes fron a predicate aspect and the context is a
+	record declaration within the scope that declares the type.
+
+2014-02-19  Robert Dewar  <dewar@adacore.com>
+
+	* gnat_rm.texi: Minor clarifications.
+	* expander.adb, sem_aggr.adb: Add comments.
+
+2014-02-19  Ed Schonberg  <schonberg@adacore.com>
+
 	* sem_prag.adb (Check_Arg_Is_Local_Name): For an aspect that
 	applies to a subprogram body, the name is the current scope,
 	rather than being declared in the current scope.
diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb
index 65e8a67..f6e65e7 100644
--- a/gcc/ada/expander.adb
+++ b/gcc/ada/expander.adb
@@ -89,9 +89,12 @@ package body Expander is
       --  Full_Analysis flag indicates whether we are performing a complete
       --  analysis, in which case Full_Analysis = True or a pre-analysis in
       --  which case Full_Analysis = False. See the spec of Sem for more info
-      --  on this. Additionally, the GNATprove_Mode flag indicates that a light
+      --  on this.
+
+      --  Additionally, the GNATprove_Mode flag indicates that a light
       --  expansion for formal verification should be used. This expansion is
-      --  never done inside generics.
+      --  never done inside generics, because otherwise, this breaks the name
+      --  resolution mechanism for generic instances
 
       --  The second reason for the Expander_Active flag to be False is that
       --  we are performing a pre-analysis. During pre-analysis all expansion
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 78c6052..b93d220 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -17523,8 +17523,12 @@ is specifically authorized by the Ada Reference Manual
 This child of @code{Ada.Containers} defines a modified version of the
 Ada 2005 container for doubly linked lists, meant to facilitate formal
 verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014. Note that the API of this unit may
-be subject to incompatible changes as SPARK 2014 evolves.
+unit is compatible with SPARK 2014.
+
+Note that although this container was designed with formal verification
+in mind, it may well be generally useful in that it is a simplified more
+efficient version than the one defined in the standard. In particular it
+does not have the complex overhead required to detect cursor tampering.
 
 @node Ada.Containers.Formal_Hashed_Maps (a-cfhama.ads)
 @section @code{Ada.Containers.Formal_Hashed_Maps} (@file{a-cfhama.ads})
@@ -17535,8 +17539,12 @@ be subject to incompatible changes as SPARK 2014 evolves.
 This child of @code{Ada.Containers} defines a modified version of the
 Ada 2005 container for hashed maps, meant to facilitate formal
 verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014. Note that the API of this unit may
-be subject to incompatible changes as SPARK 2014 evolves.
+unit is compatible with SPARK 2014.
+
+Note that although this container was designed with formal verification
+in mind, it may well be generally useful in that it is a simplified more
+efficient version than the one defined in the standard. In particular it
+does not have the complex overhead required to detect cursor tampering.
 
 @node Ada.Containers.Formal_Hashed_Sets (a-cfhase.ads)
 @section @code{Ada.Containers.Formal_Hashed_Sets} (@file{a-cfhase.ads})
@@ -17547,8 +17555,12 @@ be subject to incompatible changes as SPARK 2014 evolves.
 This child of @code{Ada.Containers} defines a modified version of the
 Ada 2005 container for hashed sets, meant to facilitate formal
 verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014. Note that the API of this unit may
-be subject to incompatible changes as SPARK 2014 evolves.
+unit is compatible with SPARK 2014.
+
+Note that although this container was designed with formal verification
+in mind, it may well be generally useful in that it is a simplified more
+efficient version than the one defined in the standard. In particular it
+does not have the complex overhead required to detect cursor tampering.
 
 @node Ada.Containers.Formal_Ordered_Maps (a-cforma.ads)
 @section @code{Ada.Containers.Formal_Ordered_Maps} (@file{a-cforma.ads})
@@ -17559,8 +17571,12 @@ be subject to incompatible changes as SPARK 2014 evolves.
 This child of @code{Ada.Containers} defines a modified version of the
 Ada 2005 container for ordered maps, meant to facilitate formal
 verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014. Note that the API of this unit may
-be subject to incompatible changes as SPARK 2014 evolves.
+unit is compatible with SPARK 2014.
+
+Note that although this container was designed with formal verification
+in mind, it may well be generally useful in that it is a simplified more
+efficient version than the one defined in the standard. In particular it
+does not have the complex overhead required to detect cursor tampering.
 
 @node Ada.Containers.Formal_Ordered_Sets (a-cforse.ads)
 @section @code{Ada.Containers.Formal_Ordered_Sets} (@file{a-cforse.ads})
@@ -17571,8 +17587,12 @@ be subject to incompatible changes as SPARK 2014 evolves.
 This child of @code{Ada.Containers} defines a modified version of the
 Ada 2005 container for ordered sets, meant to facilitate formal
 verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014. Note that the API of this unit may
-be subject to incompatible changes as SPARK 2014 evolves.
+unit is compatible with SPARK 2014.
+
+Note that although this container was designed with formal verification
+in mind, it may well be generally useful in that it is a simplified more
+efficient version than the one defined in the standard. In particular it
+does not have the complex overhead required to detect cursor tampering.
 
 @node Ada.Containers.Formal_Vectors (a-cofove.ads)
 @section @code{Ada.Containers.Formal_Vectors} (@file{a-cofove.ads})
@@ -17583,8 +17603,12 @@ be subject to incompatible changes as SPARK 2014 evolves.
 This child of @code{Ada.Containers} defines a modified version of the
 Ada 2005 container for vectors, meant to facilitate formal
 verification of code using such containers. The specification of this
-unit is compatible with SPARK 2014. Note that the API of this unit may
-be subject to incompatible changes as SPARK 2014 evolves.
+unit is compatible with SPARK 2014.
+
+Note that although this container was designed with formal verification
+in mind, it may well be generally useful in that it is a simplified more
+efficient version than the one defined in the standard. In particular it
+does not have the complex overhead required to detect cursor tampering.
 
 @node Ada.Command_Line.Environment (a-colien.ads)
 @section @code{Ada.Command_Line.Environment} (@file{a-colien.ads})
diff --git a/gcc/ada/prj-conf.adb b/gcc/ada/prj-conf.adb
index 300c33c..8d35fe2 100644
--- a/gcc/ada/prj-conf.adb
+++ b/gcc/ada/prj-conf.adb
@@ -202,6 +202,10 @@ package body Prj.Conf is
             Create_Attribute (Name_Library_Auto_Init_Supported, "false");
          end if;
 
+         --  Declare an empty target
+
+         Create_Attribute (Name_Target, "");
+
          --  Setup Ada support (Ada is the default language here, since this
          --  is only called when no config file existed initially, ie for
          --  gnatmake).
@@ -574,7 +578,8 @@ package body Prj.Conf is
       OK :=
         Target = ""
           or else (Tgt_Name /= No_Name
-                    and then Target = Get_Name_String (Tgt_Name));
+                   and then (Length_Of_Name (Tgt_Name) = 0
+                    or else Target = Get_Name_String (Tgt_Name)));
 
       if not OK then
          if Autoconf_Specified then
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 81beb71..aeddc1f 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -455,9 +455,12 @@ package body Sem_Aggr is
       end if;
 
       --  This is really expansion activity, so make sure that expansion is
-      --  on and is allowed. In GNATprove mode, we also want check flags to be
-      --  added in the tree, so that the formal verification can rely on those
-      --  to be present.
+      --  on and is allowed. In GNATprove mode, we also want check flags to
+      --  be added in the tree, so that the formal verification can rely on
+      --  those to be present. In GNATprove mode for formal verification, some
+      --  treatment typically only done during expansion needs to be performed
+      --  on the tree, but it should not be applied inside generics. Otherwise,
+      --  this breaks the name resolution mechanism for generic instances.
 
       if not Expander_Active
         and (Inside_A_Generic or not Full_Analysis or not GNATprove_Mode)
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index a55899c..7e2600f 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -128,12 +128,6 @@ package body Sem_Ch13 is
    --  Uint value. If the value is inappropriate, then error messages are
    --  posted as required, and a value of No_Uint is returned.
 
-   function Get_Cursor_Type
-     (Aspect : Node_Id;
-      Typ    : Entity_Id) return Entity_Id;
-   --  Find Cursor type in scope of Typ, by locating primitive operation First.
-   --  For use in resolving the other primitive operations of an Iterable type.
-
    function Is_Operational_Item (N : Node_Id) return Boolean;
    --  A specification for a stream attribute is allowed before the full type
    --  is declared, as explained in AI-00137 and the corrigendum. Attributes
@@ -9756,81 +9750,6 @@ package body Sem_Ch13 is
       end if;
    end Get_Alignment_Value;
 
-   ---------------------
-   -- Get_Cursor_Type --
-   ---------------------
-
-   function Get_Cursor_Type
-     (Aspect : Node_Id;
-      Typ    : Entity_Id) return Entity_Id
-   is
-      Assoc    : Node_Id;
-      Func     : Entity_Id;
-      First_Op : Entity_Id;
-      Cursor   : Entity_Id;
-
-   begin
-      --  If error already detected, return
-
-      if Error_Posted (Aspect) then
-         return Any_Type;
-      end if;
-
-      --  The cursor type for an Iterable aspect is the return type of a
-      --  non-overloaded First primitive operation. Locate association for
-      --  First.
-
-      Assoc := First (Component_Associations (Expression (Aspect)));
-      First_Op  := Any_Id;
-      while Present (Assoc) loop
-         if Chars (First (Choices (Assoc))) = Name_First then
-            First_Op := Expression (Assoc);
-            exit;
-         end if;
-
-         Next (Assoc);
-      end loop;
-
-      if First_Op = Any_Id then
-         Error_Msg_N ("aspect Iterable must specify First operation", Aspect);
-         return Any_Type;
-      end if;
-
-      Cursor := Any_Type;
-
-      --  Locate function with desired name and profile in scope of type
-
-      Func := First_Entity (Scope (Typ));
-      while Present (Func) loop
-         if Chars (Func) = Chars (First_Op)
-           and then Ekind (Func) = E_Function
-           and then Present (First_Formal (Func))
-           and then Etype (First_Formal (Func)) = Typ
-           and then No (Next_Formal (First_Formal (Func)))
-         then
-            if Cursor /= Any_Type then
-               Error_Msg_N
-                 ("Operation First for iterable type must be unique", Aspect);
-               return Any_Type;
-
-            else
-               Cursor :=  Etype (Func);
-            end if;
-         end if;
-
-         Next_Entity (Func);
-      end loop;
-
-      --  If not found, no way to resolve remaining primitives.
-
-      if Cursor = Any_Type then
-         Error_Msg_N
-           ("No legal primitive operation First for Iterable type", Aspect);
-      end if;
-
-      return Cursor;
-   end Get_Cursor_Type;
-
    -------------------------------------
    -- Inherit_Aspects_At_Freeze_Point --
    -------------------------------------
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 02a7c99..c66b416 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -1807,7 +1807,10 @@ package body Sem_Ch5 is
          end if;
       end if;
 
-      Typ := Etype (Iter_Name);
+      --  Get base type of container, for proper retrieval of Cursor type
+      --  and primitive operations.
+
+      Typ := Base_Type (Etype (Iter_Name));
 
       if Is_Array_Type (Typ) then
          if Of_Present (N) then
@@ -1918,17 +1921,25 @@ package body Sem_Ch5 is
 
             --  The result type of Iterate function is the classwide type of
             --  the interface parent. We need the specific Cursor type defined
-            --  in the container package.
+            --  in the container package. We obtain it by name for a predefined
+            --  container, or through the Iterable aspect for a formal one.
 
-            Ent := First_Entity (Scope (Typ));
-            while Present (Ent) loop
-               if Chars (Ent) = Name_Cursor then
-                  Set_Etype (Def_Id, Etype (Ent));
-                  exit;
-               end if;
+            if Has_Aspect (Typ, Aspect_Iterable) then
+               Set_Etype (Def_Id,
+                 Get_Cursor_Type
+                  (Parent (Find_Value_Of_Aspect (Typ, Aspect_Iterable)), Typ));
 
-               Next_Entity (Ent);
-            end loop;
+            else
+               Ent := First_Entity (Scope (Typ));
+               while Present (Ent) loop
+                  if Chars (Ent) = Name_Cursor then
+                     Set_Etype (Def_Id, Etype (Ent));
+                     exit;
+                  end if;
+
+                  Next_Entity (Ent);
+               end loop;
+            end if;
          end if;
       end if;
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index ed8df6e..1b102b4 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -3898,6 +3898,18 @@ package body Sem_Prag is
                then
                   OK := True;
 
+               --  If the aspect is a predicate (possibly others ???)  and the
+               --  context is a record type, this is a discriminant expression
+               --  within a type declaration, that freezes the predicated
+               --  subtype.
+
+               elsif From_Aspect_Specification (N)
+                 and then Prag_Id = Pragma_Predicate
+                 and then Ekind (Current_Scope) = E_Record_Type
+                 and then Scop = Scope (Current_Scope)
+               then
+                  OK := True;
+
                --  Default case, just check that the pragma occurs in the scope
                --  of the entity denoted by the name.
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index ceef8fa..d21d648 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -6387,6 +6387,80 @@ package body Sem_Util is
       return Proper_Body (Unit (Library_Unit (N)));
    end Get_Body_From_Stub;
 
+   ---------------------
+   -- Get_Cursor_Type --
+   ---------------------
+
+   function Get_Cursor_Type
+     (Aspect : Node_Id;
+      Typ    : Entity_Id) return Entity_Id
+   is
+      Assoc    : Node_Id;
+      Func     : Entity_Id;
+      First_Op : Entity_Id;
+      Cursor   : Entity_Id;
+
+   begin
+      --  If error already detected, return
+
+      if Error_Posted (Aspect) then
+         return Any_Type;
+      end if;
+
+      --  The cursor type for an Iterable aspect is the return type of a
+      --  non-overloaded First primitive operation. Locate association for
+      --  First.
+
+      Assoc := First (Component_Associations (Expression (Aspect)));
+      First_Op  := Any_Id;
+      while Present (Assoc) loop
+         if Chars (First (Choices (Assoc))) = Name_First then
+            First_Op := Expression (Assoc);
+            exit;
+         end if;
+
+         Next (Assoc);
+      end loop;
+
+      if First_Op = Any_Id then
+         Error_Msg_N ("aspect Iterable must specify First operation", Aspect);
+         return Any_Type;
+      end if;
+
+      Cursor := Any_Type;
+
+      --  Locate function with desired name and profile in scope of type
+
+      Func := First_Entity (Scope (Typ));
+      while Present (Func) loop
+         if Chars (Func) = Chars (First_Op)
+           and then Ekind (Func) = E_Function
+           and then Present (First_Formal (Func))
+           and then Etype (First_Formal (Func)) = Typ
+           and then No (Next_Formal (First_Formal (Func)))
+         then
+            if Cursor /= Any_Type then
+               Error_Msg_N
+                 ("Operation First for iterable type must be unique", Aspect);
+               return Any_Type;
+
+            else
+               Cursor :=  Etype (Func);
+            end if;
+         end if;
+
+         Next_Entity (Func);
+      end loop;
+
+      --  If not found, no way to resolve remaining primitives.
+
+      if Cursor = Any_Type then
+         Error_Msg_N
+           ("No legal primitive operation First for Iterable type", Aspect);
+      end if;
+
+      return Cursor;
+   end Get_Cursor_Type;
    -------------------------------
    -- Get_Default_External_Name --
    -------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 139f6d6..c6d078c 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -777,6 +777,14 @@ package Sem_Util is
    function Get_Body_From_Stub (N : Node_Id) return Node_Id;
    --  Return the body node for a stub (subprogram or package)
 
+   function Get_Cursor_Type
+     (Aspect : Node_Id;
+      Typ    : Entity_Id) return Entity_Id;
+   --  Find Cursor type in scope of formal container Typ, by locating primitive
+   --  operation First.
+   --  For use in resolving the other primitive operations of an Iterable type
+   --  and expanding loops and quantified expressions over formal containers.
+
    function Get_Default_External_Name (E : Node_Or_Entity_Id) return Node_Id;
    --  This is used to construct the string literal node representing a
    --  default external name, i.e. one that is constructed from the name of an