[multiple changes]

2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry for Aspect_Refined_Post in table
	Canonical_Aspect.
	* aspects.ads: Add an entry for Aspect_Refined_Post in tables
	Aspect_Id, Aspect_Argument, Aspect_Names, Aspect_Delay,
	Aspect_On_Body_Or_Stub_OK. Update the comment on the use of
	table Aspect_On_Body_Or_Stub_OK.
	* par-prag.adb: Add pragma Refined_Post to the list of pragmas
	that do not require special processing by the parser.
	* sem_attr.adb (Analyze_Attribute): Add special analysis for
	attributes 'Old and 'Result when code generation is disabled and
	they appear in aspect/pragma Refined_Post.
	(In_Refined_Post): New routine.
	* sem_ch6.adb (Analyze_Expression_Function): Move various
	aspects and/or pragmas that apply to an expression function to the
	corresponding spec or body.
	(Collect_Body_Postconditions): New routine.
	(Process_PPCs): Use routine Collect_Body_Postconditions
	to gather all postcondition pragmas.
	* sem_ch10.adb (Analyze_Proper_Body): Use routine
	Relocate_Pragmas_To_Body to move all source pragmas that follow
	a body stub to the proper body.
	(Move_Stub_Pragmas_To_Body): Removed.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Refined_Post.
	(Check_Aspect_At_Freeze_Point): Aspect
	Refined_Post does not need delayed processing at the freeze point.
	* sem_prag.adb: Add an entry for pragma Refined_Post in
	table Sig_Flags.
	(Analyze_Pragma): Add processing for pragma
	Refined_Post. Update the processing of pragma Refined_Pre
	to use common routine Analyze_Refined_Pre_Post.
	(Analyze_Refined_Pre_Post): New routine.
	(Relocate_Pragmas_To_Body): New routine.
	* sem_prag.ads: Table Pragma_On_Stub_OK is now known as
	Pragma_On_Body_Or_Stub_OK. Update the comment on usage of
	table Pragma_On_Body_Or_Stub_OK.
	(Relocate_Pragmas_To_Body): New routine.
	* snames.ads-tmpl: Add new predefined name for Refined_Post. Add
	new Pragma_Id for Refined_Post.

2013-10-10  Robert Dewar  <dewar@adacore.com>

	* exp_ch3.adb (Expand_N_Variant_Part): Now null, expansion of
	last choice to others is moved to Freeze_Record_Type.
	* freeze.adb (Freeze_Record_Type): Expand last variant to others
	if necessary (moved here from Expand_N_Variant_Part

From-SVN: r203359

1 files changed, 85 insertions, 43 deletions

diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index b1c5908..e313f35 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -349,15 +349,25 @@ package body Sem_Ch6 is
             Make_Handled_Sequence_Of_Statements (LocX,
               Statements => New_List (Ret)));
 
+      --  If the expression completes a generic subprogram, we must create a
+      --  separate node for the body, because at instantiation the original
+      --  node of the generic copy must be a generic subprogram body, and
+      --  cannot be a expression function. Otherwise we just rewrite the
+      --  expression with the non-generic body.
+
       if Present (Prev) and then Ekind (Prev) = E_Generic_Function then
+         Insert_After (N, New_Body);
 
-         --  If the expression completes a generic subprogram, we must create a
-         --  separate node for the body, because at instantiation the original
-         --  node of the generic copy must be a generic subprogram body, and
-         --  cannot be a expression function. Otherwise we just rewrite the
-         --  expression with the non-generic body.
+         --  Propagate any aspects or pragmas that apply to the expression
+         --  function to the proper body when the expression function acts
+         --  as a completion.
+
+         if Has_Aspects (N) then
+            Move_Aspects (N, To => New_Body);
+         end if;
+
+         Relocate_Pragmas_To_Body (New_Body);
 
-         Insert_After (N, New_Body);
          Rewrite (N, Make_Null_Statement (Loc));
          Set_Has_Completion (Prev, False);
          Analyze (N);
@@ -371,6 +381,12 @@ package body Sem_Ch6 is
 
          Generate_Reference (Prev, Defining_Entity (N), 'b', Force => True);
          Rewrite (N, New_Body);
+
+         --  Propagate any pragmas that apply to the expression function to the
+         --  proper body when the expression function acts as a completion.
+         --  Aspects are automatically transfered because of node rewriting.
+
+         Relocate_Pragmas_To_Body (N);
          Analyze (N);
 
          --  Prev is the previous entity with the same name, but it is can
@@ -11274,6 +11290,11 @@ package body Sem_Ch6 is
       --  under the same visibility conditions as for other invariant checks,
       --  the type invariant must be applied to the returned value.
 
+      procedure Collect_Body_Postconditions (Post_Nam : Name_Id);
+      --  Examine the declarations of the body, looking for pragmas with name
+      --  Post_Nam. Parameter Post_Nam must denote either Name_Postcondition or
+      --  Name_Refined_Post. Chain any relevant postconditions to Plist.
+
       function Grab_PPC (Pspec : Entity_Id := Empty) return Node_Id;
       --  Prag contains an analyzed precondition or postcondition pragma. This
       --  function copies the pragma, changes it to the corresponding Check
@@ -11365,6 +11386,60 @@ package body Sem_Ch6 is
          end if;
       end Check_Access_Invariants;
 
+      ---------------------------------
+      -- Collect_Body_Postconditions --
+      ---------------------------------
+
+      procedure Collect_Body_Postconditions (Post_Nam : Name_Id) is
+         Next_Prag : Node_Id;
+
+      begin
+         pragma Assert
+           (Nam_In (Post_Nam, Name_Postcondition, Name_Refined_Post));
+
+         Prag := First (Declarations (N));
+         while Present (Prag) loop
+            Next_Prag := Next (Prag);
+
+            if Nkind (Prag) = N_Pragma then
+
+               --  Capture postcondition pragmas
+
+               if Pragma_Name (Prag) = Post_Nam then
+                  Analyze (Prag);
+
+                  --  All Refined_Post pragmas must be relocated to the body
+                  --  of the generated _Postconditions routine, otherwise they
+                  --  will be duplicated twice - once in the declarations of
+                  --  the body and once in _Postconditions.
+
+                  if Pragma_Name (Prag) = Name_Refined_Post then
+                     Remove (Prag);
+                  end if;
+
+                  --  If expansion is disabled, as in a generic unit, save
+                  --  pragma for later expansion.
+
+                  if not Expander_Active then
+                     Prepend (Grab_PPC, Declarations (N));
+                  else
+                     Append_Enabled_Item (Grab_PPC, Plist);
+                  end if;
+               end if;
+
+            --  Skip internally generated code
+
+            elsif not Comes_From_Source (Prag) then
+               null;
+
+            else
+               exit;
+            end if;
+
+            Prag := Next_Prag;
+         end loop;
+      end Collect_Body_Postconditions;
+
       --------------
       -- Grab_PPC --
       --------------
@@ -11791,6 +11866,8 @@ package body Sem_Ch6 is
 
       --     procedure _postconditions [(_Result : resulttype)] is
       --     begin
+      --        pragma Check (Refined_Post, condition);
+      --        pragma Check (Refined_Post, condition);
       --        pragma Check (Postcondition, condition [,message]);
       --        pragma Check (Postcondition, condition [,message]);
       --        ...
@@ -11801,43 +11878,8 @@ package body Sem_Ch6 is
 
       --  First we deal with the postconditions in the body
 
-      if Is_Non_Empty_List (Declarations (N)) then
-
-         --  Loop through declarations
-
-         Prag := First (Declarations (N));
-         while Present (Prag) loop
-            if Nkind (Prag) = N_Pragma then
-
-               --  Capture postcondition pragmas
-
-               if Pragma_Name (Prag) = Name_Postcondition then
-                  Analyze (Prag);
-
-                  --  If expansion is disabled, as in a generic unit, save
-                  --  pragma for later expansion.
-
-                  if not Expander_Active then
-                     Prepend (Grab_PPC, Declarations (N));
-                  else
-                     Append_Enabled_Item (Grab_PPC, Plist);
-                  end if;
-               end if;
-
-               Next (Prag);
-
-            --  Not a pragma, if comes from source, then end scan
-
-            elsif Comes_From_Source (Prag) then
-               exit;
-
-            --  Skip stuff not coming from source
-
-            else
-               Next (Prag);
-            end if;
-         end loop;
-      end if;
+      Collect_Body_Postconditions (Name_Refined_Post);
+      Collect_Body_Postconditions (Name_Postcondition);
 
       --  Now deal with any postconditions from the spec