[multiple changes]

2017-01-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* ghost.adb (Mark_Ghost_Clause): New routine.
	(Prune_Node): Do not prune compilation unit nodes.
	(Remove_Ignored_Ghost_Code): Prune the compilation unit node directly.
	This does not touch the node itself, but does prune all its fields.
	* ghost.ads (Mark_Ghost_Clause): New routine.
	* sem_ch8.adb (Analyze_Use_Package): Emit an error when a use
	package clause mentions Ghost and non-Ghost packages. Mark a
	use package clause as Ghost when it mentions a Ghost package.
	(Analyze_Use_Type): Emit an error when a use type clause mentions
	Ghost and non-Ghost types. Mark a use type clause as Ghost when
	it mentions a Ghost type.
	* sem_ch10.adb (Analyze_With_Clause): Mark a with clause as
	Ghost when it withs a Ghost unit.

2017-01-20  Javier Miranda  <miranda@adacore.com>

	* sem_res.adb (Resolve_Call): If a function call
	returns a limited view of a type and at the point of the call the
	function is not declared in the extended main unit then replace
	it with the non-limited view, which must be available. If the
	called function is in the extended main unit then no action is
	needed since the back-end handles this case.

2017-01-20  Eric Botcazou  <ebotcazou@adacore.com>

	* sem_ch7.adb (Contains_Subp_Or_Const_Refs): Rename into...
	(Contains_Subprograms_Refs): ...this.  Adjust comment
	for constants.	(Is_Subp_Or_Const_Ref): Rename into...
	(Is_Subprogram_Ref): ...this.
	(Has_Referencer): Rename Has_Non_Subp_Const_Referencer variable into
	Has_Non_Subprograms_Referencer and adjust comment.  Remove
	incorrect shortcut for package declarations and bodies.

2017-01-20  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch3.adb (Complete_Private_Subtype): If the scope of the
	base type differs from that of the completion and the private
	subtype is an itype (created for a constraint on an access
	type e.g.), set Delayed_Freeze on both to prevent out-of-scope
	anomalies in gigi.

2017-01-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper):
	When inheriting the SPARK_Mode of a prior expression function,
	look at the properly resolved entity rather than the initial
	candidate which may denote a homonym.

2017-01-20  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb (Rewrite_Assertion_Kind): If the name is
	Precondition or Postcondition, and the context is pragma
	Check_Policy, indicate that this Pre-Ada2012 usage is deprecated
	and suggest the standard names Assertion_Policy /Pre /Post
	instead.

From-SVN: r244704

10 files changed, 275 insertions, 66 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 07c08e9..4db5a7d 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,63 @@
 2017-01-20  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* ghost.adb (Mark_Ghost_Clause): New routine.
+	(Prune_Node): Do not prune compilation unit nodes.
+	(Remove_Ignored_Ghost_Code): Prune the compilation unit node directly.
+	This does not touch the node itself, but does prune all its fields.
+	* ghost.ads (Mark_Ghost_Clause): New routine.
+	* sem_ch8.adb (Analyze_Use_Package): Emit an error when a use
+	package clause mentions Ghost and non-Ghost packages. Mark a
+	use package clause as Ghost when it mentions a Ghost package.
+	(Analyze_Use_Type): Emit an error when a use type clause mentions
+	Ghost and non-Ghost types. Mark a use type clause as Ghost when
+	it mentions a Ghost type.
+	* sem_ch10.adb (Analyze_With_Clause): Mark a with clause as
+	Ghost when it withs a Ghost unit.
+
+2017-01-20  Javier Miranda  <miranda@adacore.com>
+
+	* sem_res.adb (Resolve_Call): If a function call
+	returns a limited view of a type and at the point of the call the
+	function is not declared in the extended main unit then replace
+	it with the non-limited view, which must be available. If the
+	called function is in the extended main unit then no action is
+	needed since the back-end handles this case.
+
+2017-01-20  Eric Botcazou  <ebotcazou@adacore.com>
+
+	* sem_ch7.adb (Contains_Subp_Or_Const_Refs): Rename into...
+	(Contains_Subprograms_Refs): ...this.  Adjust comment
+	for constants.	(Is_Subp_Or_Const_Ref): Rename into...
+	(Is_Subprogram_Ref): ...this.
+	(Has_Referencer): Rename Has_Non_Subp_Const_Referencer variable into
+	Has_Non_Subprograms_Referencer and adjust comment.  Remove
+	incorrect shortcut for package declarations and bodies.
+
+2017-01-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch3.adb (Complete_Private_Subtype): If the scope of the
+	base type differs from that of the completion and the private
+	subtype is an itype (created for a constraint on an access
+	type e.g.), set Delayed_Freeze on both to prevent out-of-scope
+	anomalies in gigi.
+
+2017-01-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper):
+	When inheriting the SPARK_Mode of a prior expression function,
+	look at the properly resolved entity rather than the initial
+	candidate which may denote a homonym.
+
+2017-01-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_prag.adb (Rewrite_Assertion_Kind): If the name is
+	Precondition or Postcondition, and the context is pragma
+	Check_Policy, indicate that this Pre-Ada2012 usage is deprecated
+	and suggest the standard names Assertion_Policy /Pre /Post
+	instead.
+
+2017-01-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* sem_ch10.adb, sem_cat.adb: Minor reformatting.
 
 2017-01-20  Javier Miranda  <miranda@adacore.com>
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index fadb891..f40e8ea 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -1430,6 +1430,34 @@ package body Ghost is
    end Mark_Ghost_Declaration_Or_Body;
 
    -----------------------
+   -- Mark_Ghost_Clause --
+   -----------------------
+
+   procedure Mark_Ghost_Clause (N : Node_Id) is
+      Nam : Node_Id := Empty;
+
+   begin
+      if Nkind (N) = N_Use_Package_Clause then
+         Nam := First (Names (N));
+
+      elsif Nkind (N) = N_Use_Type_Clause then
+         Nam := First (Subtype_Marks (N));
+
+      elsif Nkind (N) = N_With_Clause then
+         Nam := Name (N);
+      end if;
+
+      if Present (Nam)
+        and then Is_Entity_Name (Nam)
+        and then Present (Entity (Nam))
+        and then Is_Ignored_Ghost_Entity (Entity (Nam))
+      then
+         Set_Is_Ignored_Ghost_Node (N);
+         Propagate_Ignored_Ghost_Code (N);
+      end if;
+   end Mark_Ghost_Clause;
+
+   -----------------------
    -- Mark_Ghost_Pragma --
    -----------------------
 
@@ -1574,10 +1602,17 @@ package body Ghost is
             Id : Entity_Id;
 
          begin
+            --  Do not prune compilation unit nodes because many mechanisms
+            --  depend on their presence. Note that context items must still
+            --  be processed.
+
+            if Nkind (N) = N_Compilation_Unit then
+               return OK;
+
             --  The node is either declared as ignored Ghost or is a byproduct
             --  of expansion. Destroy it and stop the traversal on this branch.
 
-            if Is_Ignored_Ghost_Node (N) then
+            elsif Is_Ignored_Ghost_Node (N) then
                Prune (N);
                return Skip;
 
@@ -1628,7 +1663,7 @@ package body Ghost is
 
    begin
       for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop
-         Prune_Tree (Unit (Ignored_Ghost_Units.Table (Index)));
+         Prune_Tree (Ignored_Ghost_Units.Table (Index));
       end loop;
    end Remove_Ignored_Ghost_Code;
 
diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads
index d5f11df..1e57183 100644
--- a/gcc/ada/ghost.ads
+++ b/gcc/ada/ghost.ads
@@ -183,6 +183,11 @@ package Ghost is
    --  prior to processing the procedure call. This routine starts a Ghost
    --  region and must be used in conjunction with Restore_Ghost_Mode.
 
+   procedure Mark_Ghost_Clause (N : Node_Id);
+   --  Mark use package, use type, or with clause N as Ghost when:
+   --
+   --    * The clause mentions a Ghost entity
+
    procedure Mark_Ghost_Pragma
      (N  : Node_Id;
       Id : Entity_Id);
diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index 5ea2baf..f168f53 100644
--- a/gcc/ada/sem_ch10.adb
+++ b/gcc/ada/sem_ch10.adb
@@ -34,6 +34,7 @@ with Elists;    use Elists;
 with Fname;     use Fname;
 with Fname.UF;  use Fname.UF;
 with Freeze;    use Freeze;
+with Ghost;     use Ghost;
 with Impunit;   use Impunit;
 with Inline;    use Inline;
 with Lib;       use Lib;
@@ -2826,6 +2827,8 @@ package body Sem_Ch10 is
                Set_Fatal_Error (Current_Sem_Unit, Error_Ignored);
             end if;
       end case;
+
+      Mark_Ghost_Clause (N);
    end Analyze_With_Clause;
 
    ------------------------------
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index dbf126e..7ee02bc 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -11929,12 +11929,22 @@ package body Sem_Ch3 is
       --  already frozen. We skip this processing if the type is an anonymous
       --  subtype of a record component, or is the corresponding record of a
       --  protected type, since these are processed when the enclosing type
-      --  is frozen.
+      --  is frozen. If the parent type is declared in a nested package then
+      --  the freezing of the private and full views also happens later.
 
       if not Is_Type (Scope (Full)) then
-         Set_Has_Delayed_Freeze (Full,
-           Has_Delayed_Freeze (Full_Base)
-             and then (not Is_Frozen (Full_Base)));
+         if Is_Itype (Priv)
+           and then In_Same_Source_Unit (Full, Full_Base)
+           and then Scope (Full_Base) /= Scope (Full)
+         then
+            Set_Has_Delayed_Freeze (Full);
+            Set_Has_Delayed_Freeze (Priv);
+
+         else
+            Set_Has_Delayed_Freeze (Full,
+              Has_Delayed_Freeze (Full_Base)
+                and then (not Is_Frozen (Full_Base)));
+         end if;
       end if;
 
       Set_Freeze_Node (Full, Empty);
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 12486f2..05631b3 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3843,12 +3843,12 @@ package body Sem_Ch6 is
       --    end P;                                      --    mode is ON
 
       elsif not Comes_From_Source (N)
-        and then Present (Prev_Id)
-        and then Is_Expression_Function (Prev_Id)
+        and then Present (Spec_Id)
+        and then Is_Expression_Function (Spec_Id)
       then
-         Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Prev_Id));
+         Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id));
          Set_SPARK_Pragma_Inherited
-           (Body_Id, SPARK_Pragma_Inherited (Prev_Id));
+           (Body_Id, SPARK_Pragma_Inherited (Spec_Id));
 
       --  Set the SPARK_Mode from the current context (may be overwritten later
       --  with explicit pragma). Exclude the case where the SPARK_Mode appears
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 709f593..c400fa8 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -214,9 +214,9 @@ package body Sem_Ch7 is
       --------------------------
 
       procedure Hide_Public_Entities (Decls : List_Id) is
-         function Contains_Subp_Or_Const_Refs (N : Node_Id) return Boolean;
+         function Contains_Subprograms_Refs (N : Node_Id) return Boolean;
          --  Subsidiary to routine Has_Referencer. Determine whether a node
-         --  contains a reference to a subprogram or a non-static constant.
+         --  contains a reference to a subprogram.
          --  WARNING: this is a very expensive routine as it performs a full
          --  tree traversal.
 
@@ -229,23 +229,21 @@ package body Sem_Ch7 is
          --  in the range Last (Decls) .. Referencer are hidden from external
          --  visibility.
 
-         ---------------------------------
-         -- Contains_Subp_Or_Const_Refs --
-         ---------------------------------
+         -------------------------------
+         -- Contains_Subprograms_Refs --
+         -------------------------------
 
-         function Contains_Subp_Or_Const_Refs (N : Node_Id) return Boolean is
+         function Contains_Subprograms_Refs (N : Node_Id) return Boolean is
             Reference_Seen : Boolean := False;
 
-            function Is_Subp_Or_Const_Ref
-              (N : Node_Id) return Traverse_Result;
-            --  Determine whether a node denotes a reference to a subprogram or
-            --  a non-static constant.
+            function Is_Subprogram_Ref (N : Node_Id) return Traverse_Result;
+            --  Determine whether a node denotes a reference to a subprogram
 
-            --------------------------
-            -- Is_Subp_Or_Const_Ref --
-            --------------------------
+            -----------------------
+            -- Is_Subprogram_Ref --
+            -----------------------
 
-            function Is_Subp_Or_Const_Ref
+            function Is_Subprogram_Ref
               (N : Node_Id) return Traverse_Result
             is
                Val : Node_Id;
@@ -271,7 +269,8 @@ package body Sem_Ch7 is
                   Reference_Seen := True;
                   return Abandon;
 
-               --  Detect the use of a non-static constant
+               --  Constants can be substituted by their value in gigi, which
+               --  may contain a reference, so be conservative for them.
 
                elsif Is_Entity_Name (N)
                  and then Present (Entity (N))
@@ -288,18 +287,18 @@ package body Sem_Ch7 is
                end if;
 
                return OK;
-            end Is_Subp_Or_Const_Ref;
+            end Is_Subprogram_Ref;
 
-            procedure Find_Subp_Or_Const_Ref is
-              new Traverse_Proc (Is_Subp_Or_Const_Ref);
+            procedure Find_Subprograms_Ref is
+              new Traverse_Proc (Is_Subprogram_Ref);
 
-         --  Start of processing for Contains_Subp_Or_Const_Refs
+         --  Start of processing for Contains_Subprograms_Refs
 
          begin
-            Find_Subp_Or_Const_Ref (N);
+            Find_Subprograms_Ref (N);
 
             return Reference_Seen;
-         end Contains_Subp_Or_Const_Refs;
+         end Contains_Subprograms_Refs;
 
          --------------------
          -- Has_Referencer --
@@ -313,9 +312,11 @@ package body Sem_Ch7 is
             Decl_Id : Entity_Id;
             Spec    : Node_Id;
 
-            Has_Non_Subp_Const_Referencer : Boolean := False;
-            --  Flag set for inlined subprogram bodies that do not contain
-            --  references to other subprograms or non-static constants.
+            Has_Non_Subprograms_Referencer : Boolean := False;
+            --  Flag set if a subprogram body was detected as a referencer but
+            --  does not contain references to other subprograms. In this case,
+            --  if we still are top level, we do not return True immediately,
+            --  but keep hiding subprograms from external visibility.
 
          begin
             if No (Decls) then
@@ -336,9 +337,7 @@ package body Sem_Ch7 is
 
                --  Package declaration
 
-               elsif Nkind (Decl) = N_Package_Declaration
-                 and then not Has_Non_Subp_Const_Referencer
-               then
+               elsif Nkind (Decl) = N_Package_Declaration then
                   Spec := Specification (Decl);
 
                   --  Inspect the declarations of a non-generic package to try
@@ -375,9 +374,7 @@ package body Sem_Ch7 is
                   --  Inspect the declarations of a non-generic package body to
                   --  try and hide more entities from external visibility.
 
-                  elsif not Has_Non_Subp_Const_Referencer
-                    and then Has_Referencer (Declarations (Decl))
-                  then
+                  elsif Has_Referencer (Declarations (Decl)) then
                      return True;
                   end if;
 
@@ -400,12 +397,12 @@ package body Sem_Ch7 is
                      then
                         --  Inspect the statements of the subprogram body
                         --  to determine whether the body references other
-                        --  subprograms and/or non-static constants.
+                        --  subprograms.
 
                         if Top_Level
-                          and then not Contains_Subp_Or_Const_Refs (Decl)
+                          and then not Contains_Subprograms_Refs (Decl)
                         then
-                           Has_Non_Subp_Const_Referencer := True;
+                           Has_Non_Subprograms_Referencer := True;
                         else
                            return True;
                         end if;
@@ -429,9 +426,9 @@ package body Sem_Ch7 is
 
                      if Has_Pragma_Inline (Decl_Id) then
                         if Top_Level
-                          and then not Contains_Subp_Or_Const_Refs (Decl)
+                          and then not Contains_Subprograms_Refs (Decl)
                         then
-                           Has_Non_Subp_Const_Referencer := True;
+                           Has_Non_Subprograms_Referencer := True;
                         else
                            return True;
                         end if;
@@ -444,6 +441,9 @@ package body Sem_Ch7 is
                --  if they are not followed by a construct which can reference
                --  and export them. The Is_Public flag is reset on top level
                --  entities only as anything nested is local to its context.
+               --  Likewise for subprograms, but we work harder for them as
+               --  their visibility can have a significant impact on inlining
+               --  decisions in the back end.
 
                elsif Nkind_In (Decl, N_Exception_Declaration,
                                      N_Object_Declaration,
@@ -458,7 +458,7 @@ package body Sem_Ch7 is
                     and then not Is_Exported (Decl_Id)
                     and then No (Interface_Name (Decl_Id))
                     and then
-                      (not Has_Non_Subp_Const_Referencer
+                      (not Has_Non_Subprograms_Referencer
                         or else Nkind (Decl) = N_Subprogram_Declaration)
                   then
                      Set_Is_Public (Decl_Id, False);
@@ -468,7 +468,7 @@ package body Sem_Ch7 is
                Prev (Decl);
             end loop;
 
-            return Has_Non_Subp_Const_Referencer;
+            return Has_Non_Subprograms_Referencer;
          end Has_Referencer;
 
          --  Local variables
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 176f6a7..d879492 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -3616,10 +3616,10 @@ package body Sem_Ch8 is
    --  within the package itself, ignore it.
 
    procedure Analyze_Use_Package (N : Node_Id) is
-      Pack_Name : Node_Id;
+      Ghost_Id  : Entity_Id := Empty;
+      Living_Id : Entity_Id := Empty;
       Pack      : Entity_Id;
-
-   --  Start of processing for Analyze_Use_Package
+      Pack_Name : Node_Id;
 
    begin
       Check_SPARK_05_Restriction ("use clause is not allowed", N);
@@ -3664,8 +3664,8 @@ package body Sem_Ch8 is
 
                if Entity (Pref) = Standard_Standard then
                   Error_Msg_N
-                   ("predefined package Standard cannot appear"
-                     & " in a context clause", Pref);
+                    ("predefined package Standard cannot appear in a context "
+                     & "clause", Pref);
                end if;
             end;
          end if;
@@ -3673,8 +3673,8 @@ package body Sem_Ch8 is
          Next (Pack_Name);
       end loop;
 
-      --  Loop through package names to mark all entities as potentially
-      --  use visible.
+      --  Loop through package names to mark all entities as potentially use
+      --  visible.
 
       Pack_Name := First (Names (N));
       while Present (Pack_Name) loop
@@ -3710,6 +3710,21 @@ package body Sem_Ch8 is
                if Applicable_Use (Pack_Name) then
                   Use_One_Package (Pack, N);
                end if;
+
+               --  Capture the first Ghost package and the first living package
+
+               if Is_Entity_Name (Pack_Name) then
+                  Pack := Entity (Pack_Name);
+
+                  if Is_Ghost_Entity (Pack) then
+                     if No (Ghost_Id) then
+                        Ghost_Id := Pack;
+                     end if;
+
+                  elsif No (Living_Id) then
+                     Living_Id := Pack;
+                  end if;
+               end if;
             end if;
 
          --  Report error because name denotes something other than a package
@@ -3720,6 +3735,25 @@ package body Sem_Ch8 is
 
          Next (Pack_Name);
       end loop;
+
+      --  Detect a mixture of Ghost packages and living packages within the
+      --  same use package clause. Ideally one would split a use package clause
+      --  with multiple names into multiple use package clauses with a single
+      --  name, however clients of the front end would have to adapt to this
+      --  change.
+
+      if Present (Ghost_Id) and then Present (Living_Id) then
+         Error_Msg_N
+           ("use clause cannot mention ghost and non-ghost ghost units", N);
+
+         Error_Msg_Sloc := Sloc (Ghost_Id);
+         Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id);
+
+         Error_Msg_Sloc := Sloc (Living_Id);
+         Error_Msg_NE ("\& # declared as non-ghost", N, Living_Id);
+      end if;
+
+      Mark_Ghost_Clause (N);
    end Analyze_Use_Package;
 
    ----------------------
@@ -3727,8 +3761,10 @@ package body Sem_Ch8 is
    ----------------------
 
    procedure Analyze_Use_Type (N : Node_Id) is
-      E  : Entity_Id;
-      Id : Node_Id;
+      E         : Entity_Id;
+      Ghost_Id  : Entity_Id := Empty;
+      Id        : Node_Id;
+      Living_Id : Entity_Id := Empty;
 
    begin
       Set_Hidden_By_Use_Clause (N, No_Elist);
@@ -3834,8 +3870,37 @@ package body Sem_Ch8 is
             end if;
          end if;
 
+         --  Capture the first Ghost type and the first living type
+
+         if Is_Ghost_Entity (E) then
+            if No (Ghost_Id) then
+               Ghost_Id := E;
+            end if;
+
+         elsif No (Living_Id) then
+            Living_Id := E;
+         end if;
+
          Next (Id);
       end loop;
+
+      --  Detect a mixture of Ghost types and living types within the same use
+      --  type clause. Ideally one would split a use type clause with multiple
+      --  marks into multiple use type clauses with a single mark, however
+      --  clients of the front end will have to adapt to this change.
+
+      if Present (Ghost_Id) and then Present (Living_Id) then
+         Error_Msg_N
+           ("use clause cannot mention ghost and non-ghost ghost types", N);
+
+         Error_Msg_Sloc := Sloc (Ghost_Id);
+         Error_Msg_NE ("\& # declared as ghost", N, Ghost_Id);
+
+         Error_Msg_Sloc := Sloc (Living_Id);
+         Error_Msg_NE ("\& # declared as non-ghost", N, Living_Id);
+      end if;
+
+      Mark_Ghost_Clause (N);
    end Analyze_Use_Type;
 
    --------------------
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 537fb7e..f1520d5 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -282,11 +282,16 @@ package body Sem_Prag is
    --  function, this routine finds the corresponding state and sets the entity
    --  of N to that of the state.
 
-   procedure Rewrite_Assertion_Kind (N : Node_Id);
+   procedure Rewrite_Assertion_Kind
+     (N           : Node_Id;
+      From_Policy : Boolean := False);
    --  If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class,
    --  then it is rewritten as an identifier with the corresponding special
    --  name _Pre, _Post, _Invariant, or _Type_Invariant. Used by pragmas Check
-   --  and Check_Policy.
+   --  and Check_Policy. If the names are Precondition or Postcondition, this
+   --  combination is deprecated in favor of Assertion_Policy and Ada2012
+   --  Aspect names. The parameter From_Policy indicates that the pragma
+   --  is the old non-standard Check_Policy and not a rewritten pragma.
 
    procedure Set_Elab_Unit_Name (N : Node_Id; With_Item : Node_Id);
    --  Place semantic information on the argument of an Elaborate/Elaborate_All
@@ -12807,7 +12812,8 @@ package body Sem_Prag is
                Check_Arg_Count (2);
                Check_Optional_Identifier (Arg1, Name_Name);
                Kind := Get_Pragma_Arg (Arg1);
-               Rewrite_Assertion_Kind (Kind);
+               Rewrite_Assertion_Kind (Kind,
+                 From_Policy => Comes_From_Source (N));
                Check_Arg_Is_Identifier (Arg1);
 
                --  Check forbidden check kind
@@ -29448,10 +29454,14 @@ package body Sem_Prag is
    -- Rewrite_Assertion_Kind --
    ----------------------------
 
-   procedure Rewrite_Assertion_Kind (N : Node_Id) is
+   procedure Rewrite_Assertion_Kind
+     (N           : Node_Id;
+      From_Policy : Boolean := False)
+   is
       Nam : Name_Id;
 
    begin
+      Nam := No_Name;
       if Nkind (N) = N_Attribute_Reference
         and then Attribute_Name (N) = Name_Class
         and then Nkind (Prefix (N)) = N_Identifier
@@ -29473,6 +29483,25 @@ package body Sem_Prag is
                return;
          end case;
 
+      --  Recommend standard use of aspect names Pre/Post
+
+      elsif Nkind (N) = N_Identifier
+        and then From_Policy
+        and then Serious_Errors_Detected = 0
+        and then not ASIS_Mode
+      then
+         if Chars (N) = Name_Precondition
+          or else Chars (N) = Name_Postcondition
+         then
+            Error_Msg_N (" Check_Policy is a non-standard pragma??", N);
+            Error_Msg_N
+              (" \use Assertion_Policy and aspect names Pre/Post"
+                & " for Ada2012 conformance?", N);
+         end if;
+         return;
+      end if;
+
+      if Nam /= No_Name then
          Rewrite (N, Make_Identifier (Sloc (N), Chars => Nam));
       end if;
    end Rewrite_Assertion_Kind;
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 7850a0c..1b91211 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6061,12 +6061,16 @@ package body Sem_Res is
          end;
 
       else
-         --  If the function returns the limited view of type, the call must
-         --  appear in a context in which the non-limited view is available.
-         --  As is done in Try_Object_Operation, use the available view to
-         --  prevent back-end confusion.
-
-         if From_Limited_With (Etype (Nam)) then
+         --  If the called function is not declared in the main unit and it
+         --  returns the limited view of type then use the available view (as
+         --  is done in Try_Object_Operation) to prevent back-end confusion;
+         --  the call must appear in a context where the nonlimited view is
+         --  available. If the called function is in the extended main unit
+         --  then no action is needed, because the back end handles this case.
+
+         if not In_Extended_Main_Code_Unit (Nam)
+           and then From_Limited_With (Etype (Nam))
+         then
             Set_Etype (Nam, Available_View (Etype (Nam)));
          end if;