[multiple changes]

2014-01-31  Yannick Moy  <moy@adacore.com>

	* erroutc.adb (Validate_Specific_Warnings): Remove special case for
	GNATprove_Mode.

2014-01-31  Robert Dewar  <dewar@adacore.com>

	* prj-attr.ads (First_Attribute_Of): Returns Empty_Attribute
	for Unknown_Package.
	* sem_ch6.adb, sem_attr.adb: Minor comment addition.

2014-01-31  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_util.adb (Build_Allocate_Deallocate_Proc): Rewrite
	the logic that generates a runtime check to determine the
	controlled status of the object about to be allocated or
	deallocated. Class-wide types now always use a runtime check
	even if they appear as generic actuals.
	(Find_Object): Detect
	a special case that involves interface class-wide types because
	the object appears as a complex expression.

From-SVN: r207356

6 files changed, 136 insertions, 95 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f5748bf..27d0c3f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,25 @@
+2014-01-31  Yannick Moy  <moy@adacore.com>
+
+	* erroutc.adb (Validate_Specific_Warnings): Remove special case for
+	GNATprove_Mode.
+
+2014-01-31  Robert Dewar  <dewar@adacore.com>
+
+	* prj-attr.ads (First_Attribute_Of): Returns Empty_Attribute
+	for Unknown_Package.
+	* sem_ch6.adb, sem_attr.adb: Minor comment addition.
+
+2014-01-31  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_util.adb (Build_Allocate_Deallocate_Proc): Rewrite
+	the logic that generates a runtime check to determine the
+	controlled status of the object about to be allocated or
+	deallocated. Class-wide types now always use a runtime check
+	even if they appear as generic actuals.
+	(Find_Object): Detect
+	a special case that involves interface class-wide types because
+	the object appears as a complex expression.
+
 2014-01-31  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_ch6.adb (Process_Formals): In Ada2012 mode, place
diff --git a/gcc/ada/erroutc.adb b/gcc/ada/erroutc.adb
index 3387623..541cd43 100644
--- a/gcc/ada/erroutc.adb
+++ b/gcc/ada/erroutc.adb
@@ -1322,13 +1322,6 @@ package body Erroutc is
 
                elsif not SWE.Used
 
-                 --  Do not issue this warning in GNATprove_Mode, as not
-                 --  all warnings may be generated in this mode, and pragma
-                 --  Warnings(Off) may correspond to warnings generated by the
-                 --  formal verification backend instead of frontend warnings.
-
-                 and then not GNATprove_Mode
-
                  --  Do not issue this warning for -Wxxx messages since the
                  --  back-end doesn't report the information.
 
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index b2ca141..c79c067 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -511,13 +511,32 @@ package body Exp_Util is
 
          Expr := E;
          loop
-            if Nkind_In (Expr, N_Qualified_Expression,
-                               N_Unchecked_Type_Conversion)
-            then
+            if Nkind (Expr) = N_Explicit_Dereference then
+               Expr := Prefix (Expr);
+
+            elsif Nkind (Expr) = N_Qualified_Expression then
                Expr := Expression (Expr);
 
-            elsif Nkind (Expr) = N_Explicit_Dereference then
-               Expr := Prefix (Expr);
+            elsif Nkind (Expr) = N_Unchecked_Type_Conversion then
+
+               --  When interface class-wide types are involved in allocation,
+               --  the expander introduces several levels of address arithmetic
+               --  to perform dispatch table displacement. In this scenario the
+               --  object appears as:
+               --
+               --    Tag_Ptr (Base_Address (<object>'Address))
+               --
+               --  Detect this case and utilize the whole expression as the
+               --  "object" since it now points to the proper dispatch table.
+
+               if Is_RTE (Etype (Expr), RE_Tag_Ptr) then
+                  exit;
+
+               --  Continue to strip the object
+
+               else
+                  Expr := Expression (Expr);
+               end if;
 
             else
                exit;
@@ -790,101 +809,105 @@ package body Exp_Util is
 
          --  h) Is_Controlled
 
-         --  Generate a run-time check to determine whether a class-wide object
-         --  is truly controlled.
-
          if Needs_Finalization (Desig_Typ) then
-            if Is_Class_Wide_Type (Desig_Typ)
-              or else Is_Generic_Actual_Type (Desig_Typ)
-            then
-               declare
-                  Flag_Id   : constant Entity_Id := Make_Temporary (Loc, 'F');
-                  Flag_Expr : Node_Id;
-                  Param     : Node_Id;
-                  Temp      : Node_Id;
+            declare
+               Flag_Id   : constant Entity_Id := Make_Temporary (Loc, 'F');
+               Flag_Expr : Node_Id;
+               Param     : Node_Id;
+               Temp      : Node_Id;
 
-               begin
-                  if Is_Allocate then
-                     Temp := Find_Object (Expression (Expr));
-                  else
-                     Temp := Expr;
-                  end if;
+            begin
+               if Is_Allocate then
+                  Temp := Find_Object (Expression (Expr));
+               else
+                  Temp := Expr;
+               end if;
 
-                  --  Processing for generic actuals
+               --  Processing for allocations where the expression is a subtype
+               --  indication.
 
-                  if Is_Generic_Actual_Type (Desig_Typ) then
-                     Flag_Expr :=
-                       New_Reference_To (Boolean_Literals
-                         (Needs_Finalization (Base_Type (Desig_Typ))), Loc);
+               if Is_Allocate
+                 and then Is_Entity_Name (Temp)
+                 and then Is_Type (Entity (Temp))
+               then
+                  Flag_Expr :=
+                    New_Reference_To (Boolean_Literals
+                      (Needs_Finalization (Entity (Temp))), Loc);
 
-                  --  Processing for subtype indications
+               --  The allocation / deallocation of a class-wide object relies
+               --  on a runtime check to determine whether the object is truly
+               --  controlled or not. Depending on this check, the finalization
+               --  machinery will request or reclaim extra storage reserved for
+               --  a list header.
 
-                  elsif Nkind (Temp) in N_Has_Entity
-                    and then Is_Type (Entity (Temp))
-                  then
-                     Flag_Expr :=
-                       New_Reference_To (Boolean_Literals
-                         (Needs_Finalization (Entity (Temp))), Loc);
+               elsif Is_Class_Wide_Type (Desig_Typ) then
 
-                  --  Generate a runtime check to test the controlled state of
-                  --  an object for the purposes of allocation / deallocation.
+                  --  Detect a special case where interface class-wide types
+                  --  are involved as the object appears as:
+                  --
+                  --    Tag_Ptr (Base_Address (<object>'Address))
+                  --
+                  --  The expression already yields the proper tag, generate:
+                  --
+                  --    Temp.all
 
-                  else
-                     --  The following case arises when allocating through an
-                     --  interface class-wide type, generate:
-                     --
-                     --    Temp.all
+                  if Is_RTE (Etype (Temp), RE_Tag_Ptr) then
+                     Param :=
+                       Make_Explicit_Dereference (Loc,
+                         Prefix => Relocate_Node (Temp));
 
-                     if Is_RTE (Etype (Temp), RE_Tag_Ptr) then
-                        Param :=
-                          Make_Explicit_Dereference (Loc,
-                            Prefix =>
-                              Relocate_Node (Temp));
+                  --  In the default case, obtain the tag of the object about
+                  --  to be allocated / deallocated. Generate:
+                  --
+                  --    Temp'Tag
 
-                     --  Generate:
-                     --    Temp'Tag
+                  else
+                     Param :=
+                       Make_Attribute_Reference (Loc,
+                         Prefix         => Relocate_Node (Temp),
+                         Attribute_Name => Name_Tag);
+                  end if;
 
-                     else
-                        Param :=
-                          Make_Attribute_Reference (Loc,
-                            Prefix =>
-                              Relocate_Node (Temp),
-                            Attribute_Name => Name_Tag);
-                     end if;
+                  --  Generate:
+                  --    Needs_Finalization (<Param>)
 
-                     --  Generate:
-                     --    Needs_Finalization (<Param>)
+                  Flag_Expr :=
+                    Make_Function_Call (Loc,
+                      Name                   =>
+                        New_Reference_To (RTE (RE_Needs_Finalization), Loc),
+                      Parameter_Associations => New_List (Param));
 
-                     Flag_Expr :=
-                       Make_Function_Call (Loc,
-                         Name =>
-                           New_Reference_To (RTE (RE_Needs_Finalization), Loc),
-                         Parameter_Associations => New_List (Param));
-                  end if;
+               --  Processing for generic actuals
 
-                  --  Create the temporary which represents the finalization
-                  --  state of the expression. Generate:
-                  --
-                  --    F : constant Boolean := <Flag_Expr>;
+               elsif Is_Generic_Actual_Type (Desig_Typ) then
+                  Flag_Expr :=
+                    New_Reference_To (Boolean_Literals
+                      (Needs_Finalization (Base_Type (Desig_Typ))), Loc);
 
-                  Insert_Action (N,
-                    Make_Object_Declaration (Loc,
-                      Defining_Identifier => Flag_Id,
-                      Constant_Present => True,
-                      Object_Definition =>
-                        New_Reference_To (Standard_Boolean, Loc),
-                      Expression => Flag_Expr));
+               --  The object does not require any specialized checks, it is
+               --  known to be controlled.
 
-                  --  The flag acts as the last actual
+               else
+                  Flag_Expr := New_Reference_To (Standard_True, Loc);
+               end if;
 
-                  Append_To (Actuals, New_Reference_To (Flag_Id, Loc));
-               end;
+               --  Create the temporary which represents the finalization state
+               --  of the expression. Generate:
+               --
+               --    F : constant Boolean := <Flag_Expr>;
 
-            --  The object is statically known to be controlled
+               Insert_Action (N,
+                 Make_Object_Declaration (Loc,
+                   Defining_Identifier => Flag_Id,
+                   Constant_Present    => True,
+                   Object_Definition   =>
+                     New_Reference_To (Standard_Boolean, Loc),
+                    Expression          => Flag_Expr));
 
-            else
-               Append_To (Actuals, New_Reference_To (Standard_True, Loc));
-            end if;
+               Append_To (Actuals, New_Reference_To (Flag_Id, Loc));
+            end;
+
+         --  The object is not controlled
 
          else
             Append_To (Actuals, New_Reference_To (Standard_False, Loc));
diff --git a/gcc/ada/prj-attr.ads b/gcc/ada/prj-attr.ads
index 03e63d1..dc60cd6 100644
--- a/gcc/ada/prj-attr.ads
+++ b/gcc/ada/prj-attr.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2001-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 2001-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -246,7 +246,7 @@ package Prj.Attr is
    function First_Attribute_Of
      (Pkg : Package_Node_Id) return Attribute_Node_Id;
    --  Returns the first attribute in the list of attributes of package Pkg.
-   --  Returns Empty_Attribute if Pkg is Empty_Package.
+   --  Returns Empty_Attribute if Pkg is Empty_Package or Unknown_Package.
 
 private
    ----------------
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 8e3b806..24faf86 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -6149,6 +6149,11 @@ package body Sem_Attr is
                   end;
 
                elsif Is_Record_Type (P_Type) then
+
+                  --  Make sure we have an identifier. Old SPARK allowed
+                  --  a component selection e.g. A.B in the corresponding
+                  --  context, but we do not yet permit this for 'Update.
+
                   if Nkind (Comp) /= N_Identifier then
                      Error_Msg_N ("name should be identifier or OTHERS", Comp);
                   else
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index b9520de..5b91519 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -1908,10 +1908,8 @@ package body Sem_Ch6 is
                      null;
 
                   elsif Nkind (Parent (N)) = N_Subprogram_Body
-                    or else
-                      Nkind_In (Parent (Parent (N)),
-                        N_Accept_Statement,
-                        N_Entry_Body)
+                    or else Nkind_In (Parent (Parent (N)), N_Accept_Statement,
+                                                           N_Entry_Body)
                   then
                      Error_Msg_NE
                        ("invalid use of untagged incomplete type&",
@@ -1919,7 +1917,7 @@ package body Sem_Ch6 is
                   end if;
 
                   --  The type must be completed in the current package. This
-                  --  is checked at the end of the package declaraton, when
+                  --  is checked at the end of the package declaration when
                   --  Taft-amendment types are identified. If the return type
                   --  is class-wide, there is no required check, the type can
                   --  be a bona fide TAT.