[multiple changes]

2009-04-10  Robert Dewar  <dewar@adacore.com>

	* gnat_rm.texi: Document that postconditions are tested on implicit
	returns.

	* sem_aux.adb: Minor reformatting

2009-04-10  Gary Dismukes  <dismukes@adacore.com>

	* itypes.adb (Create_Null_Excluding_Itype): Apply Base_Type when
	setting Etype.
	
	* par-ch3.adb (P_Access_Type_Definition): Set new attribute
	Null_Exclusion_In_Return_Present when an access-to-function type has a
	result type with an explicit not null.

	* sem_ch3.adb (Access_Subprogram_Definition): If a null exclusion is
	given on the result type, then create a null-excluding itype for the
	function.

	* sem_ch6.adb (Analyze_Return_Type): Create a null-excluding itype in
	the case where a null exclusion is imposed on a named access type.
	(Analyze_Subprogram_Specification): Push and pop the scope of the
	function around the call to Analyze_Return_Type in the case of no
	formals, for consistency with handling when formals are present
	(Process_Formals does this). Ensures that any itype created for the
	return type will be associated with the proper scope.

	* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): If a null
	exclusion is given on a generic function's result type, then create a
	null-excluding itype for the generic function.
	(Instantiate_Object): Set Null_Exclusion_Present of a constant created
	for an actual for a formal in object according to the setting on the
	formal. Ensures null exclusion checks are done when the association is
	elaborated.

	* sinfo.ads: Add new flag Null_Exclusion_In_Return_Present on
	N_Access_Function_Definition.

	* sinfo.adb: Add Get_ and Set_ operations for
	Null_Exclusion_In_Return_Present.

From-SVN: r145912

10 files changed, 173 insertions, 30 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index bd16930..0849bda 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,45 @@
+2009-04-10  Robert Dewar  <dewar@adacore.com>
+
+	* gnat_rm.texi: Document that postconditions are tested on implicit
+	returns.
+
+	* sem_aux.adb: Minor reformatting
+
+2009-04-10  Gary Dismukes  <dismukes@adacore.com>
+
+	* itypes.adb (Create_Null_Excluding_Itype): Apply Base_Type when
+	setting Etype.
+	
+	* par-ch3.adb (P_Access_Type_Definition): Set new attribute
+	Null_Exclusion_In_Return_Present when an access-to-function type has a
+	result type with an explicit not null.
+
+	* sem_ch3.adb (Access_Subprogram_Definition): If a null exclusion is
+	given on the result type, then create a null-excluding itype for the
+	function.
+
+	* sem_ch6.adb (Analyze_Return_Type): Create a null-excluding itype in
+	the case where a null exclusion is imposed on a named access type.
+	(Analyze_Subprogram_Specification): Push and pop the scope of the
+	function around the call to Analyze_Return_Type in the case of no
+	formals, for consistency with handling when formals are present
+	(Process_Formals does this). Ensures that any itype created for the
+	return type will be associated with the proper scope.
+
+	* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): If a null
+	exclusion is given on a generic function's result type, then create a
+	null-excluding itype for the generic function.
+	(Instantiate_Object): Set Null_Exclusion_Present of a constant created
+	for an actual for a formal in object according to the setting on the
+	formal. Ensures null exclusion checks are done when the association is
+	elaborated.
+
+	* sinfo.ads: Add new flag Null_Exclusion_In_Return_Present on
+	N_Access_Function_Definition.
+
+	* sinfo.adb: Add Get_ and Set_ operations for
+	Null_Exclusion_In_Return_Present.
+
 2009-04-10  Bob Duff  <duff@adacore.com>
 
 	* exp_ch5.adb, exp_ch6.adb, sem_ch6.adb: Move the code that creates a
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index ae93d01..adb3193 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -3738,8 +3738,11 @@ pragma Postcondition (
 The @code{Postcondition} pragma allows specification of automatic
 postcondition checks for subprograms. These checks are similar to
 assertions, but are automatically inserted just prior to the return
-statements of the subprogram with which they are associated.
-Furthermore, the boolean expression which is the condition which
+statements of the subprogram with which they are associated (including
+implicit returns at the end of procedure bodies and associated
+exception handlers).
+
+In addition, the boolean expression which is the condition which
 must be true may contain references to function'Result in the case
 of a function to refer to the returned value.
 
diff --git a/gcc/ada/itypes.adb b/gcc/ada/itypes.adb
index 59155dc..1c43032 100644
--- a/gcc/ada/itypes.adb
+++ b/gcc/ada/itypes.adb
@@ -102,7 +102,7 @@ package body Itypes is
                              Scope_Id    => Scope_Id);
 
       Set_Directly_Designated_Type (I_Typ, Directly_Designated_Type (T));
-      Set_Etype                    (I_Typ, T);
+      Set_Etype                    (I_Typ, Base_Type (T));
       Set_Depends_On_Private       (I_Typ, Depends_On_Private (T));
       Set_Is_Public                (I_Typ, Is_Public          (T));
       Set_From_With_Type           (I_Typ, From_With_Type     (T));
diff --git a/gcc/ada/par-ch3.adb b/gcc/ada/par-ch3.adb
index 9a5a8d3..a7e6fb6 100644
--- a/gcc/ada/par-ch3.adb
+++ b/gcc/ada/par-ch3.adb
@@ -3827,13 +3827,14 @@ package body Ch3 is
          else
             Result_Node := P_Subtype_Mark;
             No_Constraint;
-         end if;
 
-         --  Note: A null exclusion given on the result type needs to
-         --  be coded by a distinct flag, since Null_Exclusion_Present
-         --  on an access-to-function type pertains to a null exclusion
-         --  on the access type itself (as set above). ???
-         --  Set_Null_Exclusion_Present??? (Type_Def_Node, Result_Not_Null);
+            --  A null exclusion on the result type must be recorded in a flag
+            --  distinct from the one used for the access-to-subprogram type's
+            --  null exclusion.
+
+            Set_Null_Exclusion_In_Return_Present
+              (Type_Def_Node, Result_Not_Null);
+         end if;
 
          Set_Result_Definition (Type_Def_Node, Result_Node);
 
diff --git a/gcc/ada/sem_aux.adb b/gcc/ada/sem_aux.adb
index 39b7443..8d111a8 100755
--- a/gcc/ada/sem_aux.adb
+++ b/gcc/ada/sem_aux.adb
@@ -120,8 +120,7 @@ package body Sem_Aux is
          return Renamed_Object (Ent);
 
       --  If this is a component declaration whose entity is constant, it is
-      --  a prival within a protected function. It does not have a constant
-      --  value.
+      --  a prival within a protected function (and so has no constant value).
 
       elsif Nkind (D) = N_Component_Declaration then
          return Empty;
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index d5a8a2e..24d6b4d 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -32,6 +32,7 @@ with Fname;    use Fname;
 with Fname.UF; use Fname.UF;
 with Freeze;   use Freeze;
 with Hostparm;
+with Itypes;   use Itypes;
 with Lib;      use Lib;
 with Lib.Load; use Lib.Load;
 with Lib.Xref; use Lib.Xref;
@@ -2740,6 +2741,7 @@ package body Sem_Ch12 is
       New_N       : Node_Id;
       Result_Type : Entity_Id;
       Save_Parent : Node_Id;
+      Typ         : Entity_Id;
 
    begin
       --  Create copy of generic unit, and save for instantiation. If the unit
@@ -2788,7 +2790,23 @@ package body Sem_Ch12 is
             Set_Etype (Id, Result_Type);
          else
             Find_Type (Result_Definition (Spec));
-            Set_Etype (Id, Entity (Result_Definition (Spec)));
+            Typ := Entity (Result_Definition (Spec));
+
+            --  If a null exclusion is imposed on the result type, then create
+            --  a null-excluding itype (an access subtype) and use it as the
+            --  function's Etype.
+
+            if Is_Access_Type (Typ)
+              and then Null_Exclusion_Present (Spec)
+            then
+               Set_Etype  (Id,
+                 Create_Null_Excluding_Itype
+                   (T           => Typ,
+                    Related_Nod => Spec,
+                    Scope_Id    => Defining_Unit_Name (Spec)));
+            else
+               Set_Etype (Id, Typ);
+            end if;
          end if;
 
       else
@@ -8310,10 +8328,11 @@ package body Sem_Ch12 is
 
             Decl_Node :=
               Make_Object_Declaration (Loc,
-                Defining_Identifier => New_Copy (Formal_Id),
-                Constant_Present    => True,
-                Object_Definition   => New_Copy_Tree (Def),
-                Expression          => Actual);
+                Defining_Identifier    => New_Copy (Formal_Id),
+                Constant_Present       => True,
+                Null_Exclusion_Present => Null_Exclusion_Present (Formal),
+                Object_Definition      => New_Copy_Tree (Def),
+                Expression             => Actual);
 
             Set_Corresponding_Generic_Association (Decl_Node, Act_Assoc);
 
@@ -8379,11 +8398,12 @@ package body Sem_Ch12 is
 
             Decl_Node :=
               Make_Object_Declaration (Sloc (Formal),
-                Defining_Identifier => New_Copy (Formal_Id),
-                Constant_Present    => True,
-                Object_Definition   => New_Copy (Def),
-                Expression          => New_Copy_Tree
-                                         (Default_Expression (Formal)));
+                Defining_Identifier    => New_Copy (Formal_Id),
+                Constant_Present       => True,
+                Null_Exclusion_Present => Null_Exclusion_Present (Formal),
+                Object_Definition      => New_Copy (Def),
+                Expression             => New_Copy_Tree
+                                            (Default_Expression (Formal)));
 
             Append (Decl_Node, List);
             Set_Analyzed (Expression (Decl_Node), False);
@@ -8410,10 +8430,11 @@ package body Sem_Ch12 is
 
                Decl_Node :=
                  Make_Object_Declaration (Loc,
-                   Defining_Identifier => New_Copy (Formal_Id),
-                   Constant_Present    => True,
-                   Object_Definition   => New_Copy (Def),
-                   Expression          =>
+                   Defining_Identifier    => New_Copy (Formal_Id),
+                   Constant_Present       => True,
+                   Null_Exclusion_Present => Null_Exclusion_Present (Formal),
+                   Object_Definition      => New_Copy (Def),
+                   Expression             =>
                      Make_Attribute_Reference (Sloc (Formal_Id),
                        Attribute_Name => Name_First,
                        Prefix         => New_Copy (Def)));
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index bc6635f..bc3ffad 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -1118,7 +1118,27 @@ package body Sem_Ch3 is
 
          else
             Analyze (Result_Definition (T_Def));
-            Set_Etype (Desig_Type, Entity (Result_Definition (T_Def)));
+
+            declare
+               Typ : constant Entity_Id := Entity (Result_Definition (T_Def));
+
+            begin
+               --  If a null exclusion is imposed on the result type, then
+               --  create a null-excluding itype (an access subtype) and use
+               --  it as the function's Etype.
+
+               if Is_Access_Type (Typ)
+                 and then Null_Exclusion_In_Return_Present (T_Def)
+               then
+                  Set_Etype  (Desig_Type,
+                    Create_Null_Excluding_Itype
+                      (T           => Typ,
+                       Related_Nod => T_Def,
+                       Scope_Id    => Current_Scope));
+               else
+                  Set_Etype (Desig_Type, Typ);
+               end if;
+            end;
          end if;
 
          if not (Is_Type (Etype (Desig_Type))) then
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index a509640..9f1761e 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -1282,6 +1282,10 @@ package body Sem_Ch6 is
             Set_Is_Local_Anonymous_Access (Typ);
             Set_Etype (Designator, Typ);
 
+            --  Ada 2005 (AI-231): Ensure proper usage of null exclusion
+
+            Null_Exclusion_Static_Checks (N);
+
          --  Subtype_Mark case
 
          else
@@ -1289,6 +1293,28 @@ package body Sem_Ch6 is
             Typ := Entity (Result_Definition (N));
             Set_Etype (Designator, Typ);
 
+            --  Ada 2005 (AI-231): Ensure proper usage of null exclusion
+
+            Null_Exclusion_Static_Checks (N);
+
+            --  If a null exclusion is imposed on the result type, then create
+            --  a null-excluding itype (an access subtype) and use it as the
+            --  function's Etype. Note that the null exclusion checks are done
+            --  right before this, because they don't get applied to types that
+            --  do not come from source.
+
+            if Is_Access_Type (Typ)
+              and then Null_Exclusion_Present (N)
+            then
+               Set_Etype  (Designator,
+                 Create_Null_Excluding_Itype
+                   (T           => Typ,
+                    Related_Nod => N,
+                    Scope_Id    => Scope (Current_Scope)));
+            else
+               Set_Etype (Designator, Typ);
+            end if;
+
             if Ekind (Typ) = E_Incomplete_Type
               and then Is_Value_Type (Typ)
             then
@@ -1304,10 +1330,6 @@ package body Sem_Ch6 is
             end if;
          end if;
 
-         --  Ada 2005 (AI-231): Ensure proper usage of null exclusion
-
-         Null_Exclusion_Static_Checks (N);
-
       --  Case where result definition does indicate an error
 
       else
@@ -2731,8 +2753,18 @@ package body Sem_Ch6 is
 
          End_Scope;
 
+      --  The subprogram scope is pushed and popped around the processing of
+      --  the return type for consistency with call above to Process_Formals
+      --  (which itself can call Analyze_Return_Type), and to ensure that any
+      --  itype created for the return type will be associated with the proper
+      --  scope.
+
       elsif Nkind (N) = N_Function_Specification then
+         Push_Scope (Designator);
+
          Analyze_Return_Type (N);
+
+         End_Scope;
       end if;
 
       if Nkind (N) = N_Function_Specification then
diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb
index e421226..59ddd5c 100644
--- a/gcc/ada/sinfo.adb
+++ b/gcc/ada/sinfo.adb
@@ -2088,6 +2088,14 @@ package body Sinfo is
       return Flag11 (N);
    end Null_Exclusion_Present;
 
+   function Null_Exclusion_In_Return_Present
+      (N : Node_Id) return Boolean is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Access_Function_Definition);
+      return Flag14 (N);
+   end Null_Exclusion_In_Return_Present;
+
    function Null_Record_Present
       (N : Node_Id) return Boolean is
    begin
@@ -4860,6 +4868,14 @@ package body Sinfo is
       Set_Flag11 (N, Val);
    end Set_Null_Exclusion_Present;
 
+   procedure Set_Null_Exclusion_In_Return_Present
+      (N : Node_Id; Val : Boolean := True) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Access_Function_Definition);
+      Set_Flag14 (N, Val);
+   end Set_Null_Exclusion_In_Return_Present;
+
    procedure Set_Null_Record_Present
       (N : Node_Id; Val : Boolean := True) is
    begin
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 9ef69c5..90c10f9 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -2883,6 +2883,7 @@ package Sinfo is
       --  N_Access_Function_Definition
       --  Sloc points to ACCESS
       --  Null_Exclusion_Present (Flag11)
+      --  Null_Exclusion_In_Return_Present (Flag14)
       --  Protected_Present (Flag6)
       --  Parameter_Specifications (List3) (set to No_List if no formal part)
       --  Result_Definition (Node4) result subtype (subtype mark or access def)
@@ -8088,6 +8089,9 @@ package Sinfo is
    function Null_Exclusion_Present
      (N : Node_Id) return Boolean;    -- Flag11
 
+   function Null_Exclusion_In_Return_Present
+     (N : Node_Id) return Boolean;    -- Flag14
+
    function Null_Record_Present
      (N : Node_Id) return Boolean;    -- Flag17
 
@@ -8970,6 +8974,9 @@ package Sinfo is
    procedure Set_Null_Exclusion_Present
      (N : Node_Id; Val : Boolean := True);    -- Flag11
 
+   procedure Set_Null_Exclusion_In_Return_Present
+     (N : Node_Id; Val : Boolean := True);    -- Flag14
+
    procedure Set_Null_Record_Present
      (N : Node_Id; Val : Boolean := True);    -- Flag17
 
@@ -11062,6 +11069,7 @@ package Sinfo is
    pragma Inline (No_Truncation);
    pragma Inline (Null_Present);
    pragma Inline (Null_Exclusion_Present);
+   pragma Inline (Null_Exclusion_In_Return_Present);
    pragma Inline (Null_Record_Present);
    pragma Inline (Object_Definition);
    pragma Inline (Original_Discriminant);
@@ -11353,6 +11361,7 @@ package Sinfo is
    pragma Inline (Set_No_Truncation);
    pragma Inline (Set_Null_Present);
    pragma Inline (Set_Null_Exclusion_Present);
+   pragma Inline (Set_Null_Exclusion_In_Return_Present);
    pragma Inline (Set_Null_Record_Present);
    pragma Inline (Set_Object_Definition);
    pragma Inline (Set_Original_Discriminant);