[multiple changes]

2013-09-10  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Handle properly
	a subprogram body without previous spec.

2013-09-10  Gary Dismukes  <dismukes@adacore.com>

	* sem_ch4.adb: Minor typo fixes.

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

	* aspects.adb (Aspects_On_Body_OK): New routine.
	* aspects.ads: Modify type Aspect_Expression to include
	the Optional_XXX variants. Update the contents of
	table Aspect_Argument. Add table Aspect_On_Body_OK.
	(Aspects_On_Body_OK): New routine.
	* par-ch13.adb (Get_Aspect_Specifications): Account for optional
	names and expressions when parsing an aspect.
	* sem_ch6.adb: Add with and use clause for Aspects.
	(Analyze_Subprogram_Body_Helper): Do not emit an error when
	analyzing a body with aspects that can be applied simultaneously
	to both spec and body.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Insert the
	corresponding pragma of an aspect that applies to a subprogram
	body in the declarative part.
	(Make_Aitem_Pragma): Do not generate a pragma with an empty argument
	list.

From-SVN: r202462

gcc/ada/ChangeLog

+2013-09-10  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Handle properly
+	a subprogram body without previous spec.
+
+2013-09-10  Gary Dismukes  <dismukes@adacore.com>
+
+	* sem_ch4.adb: Minor typo fixes.
+
+2013-09-10  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* aspects.adb (Aspects_On_Body_OK): New routine.
+	* aspects.ads: Modify type Aspect_Expression to include
+	the Optional_XXX variants. Update the contents of
+	table Aspect_Argument. Add table Aspect_On_Body_OK.
+	(Aspects_On_Body_OK): New routine.
+	* par-ch13.adb (Get_Aspect_Specifications): Account for optional
+	names and expressions when parsing an aspect.
+	* sem_ch6.adb: Add with and use clause for Aspects.
+	(Analyze_Subprogram_Body_Helper): Do not emit an error when
+	analyzing a body with aspects that can be applied simultaneously
+	to both spec and body.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Insert the
+	corresponding pragma of an aspect that applies to a subprogram
+	body in the declarative part.
+	(Make_Aitem_Pragma): Do not generate a pragma with an empty argument
+	list.
+
 2013-09-10  Robert Dewar  <dewar@adacore.com>
 
 	* switch-c.adb: Diagnose -gnatc given after -gnatRm.

gcc/ada/aspects.adb

@@ -140,6 +140,40 @@ package body Aspects is
       end if;
    end Aspect_Specifications;
 
+   ------------------------
+   -- Aspects_On_Body_OK --
+   ------------------------
+
+   function Aspects_On_Body_OK (N : Node_Id) return Boolean is
+      Aspect  : Node_Id;
+      Aspects : List_Id;
+
+   begin
+      --  The routine should be invoked on a body [stub] with aspects
+
+      pragma Assert (Has_Aspects (N));
+      pragma Assert (Nkind (N) in N_Body_Stub
+                       or else Nkind_In (N, N_Package_Body,
+                                            N_Protected_Body,
+                                            N_Subprogram_Body,
+                                            N_Task_Body));
+
+      --  Look through all aspects and see whether they can be applied to a
+      --  body.
+
+      Aspects := Aspect_Specifications (N);
+      Aspect  := First (Aspects);
+      while Present (Aspect) loop
+         if not Aspect_On_Body_OK (Get_Aspect_Id (Aspect)) then
+            return False;
+         end if;
+
+         Next (Aspect);
+      end loop;
+
+      return True;
+   end Aspects_On_Body_OK;
+
    -----------------
    -- Find_Aspect --
    -----------------

gcc/ada/aspects.ads

@@ -273,14 +273,15 @@ package Aspects is
    --  The following type is used for indicating allowed expression forms
 
    type Aspect_Expression is
-     (Optional,               -- Optional boolean expression
-      Expression,             -- Required expression
-      Name);                  -- Required name
+     (Expression,             -- Required expression
+      Name,                   -- Required name
+      Optional_Expression,    -- Optional boolean expression
+      Optional_Name);         -- Optional name
 
    --  The following array indicates what argument type is required
 
    Aspect_Argument : constant array (Aspect_Id) of Aspect_Expression :=
-     (No_Aspect                      => Optional,
+     (No_Aspect                      => Optional_Expression,
       Aspect_Abstract_State          => Expression,
       Aspect_Address                 => Expression,
       Aspect_Alignment               => Expression,
@@ -323,7 +324,7 @@ package Aspects is
       Aspect_Simple_Storage_Pool     => Name,
       Aspect_Size                    => Expression,
       Aspect_Small                   => Expression,
-      Aspect_SPARK_Mode              => Name,
+      Aspect_SPARK_Mode              => Optional_Name,
       Aspect_Static_Predicate        => Expression,
       Aspect_Storage_Pool            => Name,
       Aspect_Storage_Size            => Expression,
@@ -338,8 +339,8 @@ package Aspects is
       Aspect_Warnings                => Name,
       Aspect_Write                   => Name,
 
-      Boolean_Aspects                => Optional,
-      Library_Unit_Aspects           => Optional);
+      Boolean_Aspects                => Optional_Expression,
+      Library_Unit_Aspects           => Optional_Expression);
 
    -----------------------------------------
    -- Table Linking Names and Aspect_Id's --
@@ -656,6 +657,17 @@ package Aspects is
       Aspect_Volatile                     => Rep_Aspect,
       Aspect_Volatile_Components          => Rep_Aspect);
 
+   --  The following table indicates which aspects can apply simultaneously to
+   --  both subprogram/package specs and bodies. For instance, the following is
+   --  legal:
+
+   --    package P with SPARK_Mode ...;
+   --    package body P with SPARK_Mode is ...;
+
+   Aspect_On_Body_OK : constant array (Aspect_Id) of Boolean :=
+     (Aspect_SPARK_Mode                   => True,
+      others                              => False);
+
    ---------------------------------------------------
    -- Handling of Aspect Specifications in the Tree --
    ---------------------------------------------------
@@ -684,6 +696,10 @@ package Aspects is
    --  Replace calls, and this function may be used to retrieve the aspect
    --  specifications for the original rewritten node in such cases.
 
+   function Aspects_On_Body_OK (N : Node_Id) return Boolean;
+   --  N denotes a body [stub] with aspects. Determine whether all aspects of N
+   --  can appear simultaneously in bodies and specs.
+
    function Find_Aspect (Id : Entity_Id; A : Aspect_Id) return Node_Id;
    --  Find the aspect specification of aspect A associated with entity I.
    --  Return Empty if Id does not have the requested aspect.

gcc/ada/par-ch13.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-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- --
@@ -266,15 +266,20 @@ package body Ch13 is
             if Token = Tok_Comma
               or else Token = Tok_Semicolon
             then
-               if Aspect_Argument (A_Id) /= Optional then
+               if Aspect_Argument (A_Id) /= Optional_Expression
+                    and then
+                  Aspect_Argument (A_Id) /= Optional_Name
+               then
                   Error_Msg_Node_1 := Identifier (Aspect);
                   Error_Msg_AP ("aspect& requires an aspect definition");
                   OK := False;
                end if;
 
             elsif not Semicolon and then Token /= Tok_Arrow then
-               if Aspect_Argument (A_Id) /= Optional then
-
+               if Aspect_Argument (A_Id) /= Optional_Expression
+                    and then
+                  Aspect_Argument (A_Id) /= Optional_Name
+               then
                   --  The name or expression may be there, but the arrow is
                   --  missing. Skip to the end of the declaration.
 
@@ -292,9 +297,17 @@ package body Ch13 is
                   OK := False;
                end if;
 
-               if Aspect_Argument (A_Id) = Name then
+               if Aspect_Argument (A_Id) = Name
+                    or else
+                  Aspect_Argument (A_Id) = Optional_Name
+               then
                   Set_Expression (Aspect, P_Name);
+
                else
+                  pragma Assert
+                    (Aspect_Argument (A_Id) = Expression
+                       or else
+                     Aspect_Argument (A_Id) = Optional_Expression);
                   Set_Expression (Aspect, P_Expression);
                end if;
             end if;

gcc/ada/sem_ch13.adb

@@ -1357,17 +1357,26 @@ package body Sem_Ch13 is
               (Pragma_Argument_Associations : List_Id;
                Pragma_Name                  : Name_Id)
             is
+               Args : List_Id := Pragma_Argument_Associations;
+
             begin
                --  We should never get here if aspect was disabled
 
                pragma Assert (not Is_Disabled (Aspect));
 
+               --  Certan aspects allow for an optional name or expression. Do
+               --  not generate a pragma with an empty argument association
+               --  list.
+
+               if No (Args) or else No (Expression (First (Args))) then
+                  Args := No_List;
+               end if;
+
                --  Build the pragma
 
                Aitem :=
                  Make_Pragma (Loc,
-                   Pragma_Argument_Associations =>
-                     Pragma_Argument_Associations,
+                   Pragma_Argument_Associations => Args,
                    Pragma_Identifier =>
                      Make_Identifier (Sloc (Id), Pragma_Name),
                    Class_Present     => Class_Present (Aspect),
@@ -2433,10 +2442,10 @@ package body Sem_Ch13 is
                Set_Has_Delayed_Aspects (E);
                Record_Rep_Item (E, Aspect);
 
-            --  When delay is not required and the context is a package body,
-            --  insert the pragma in the declarations of the body.
+            --  When delay is not required and the context is a package or a
+            --  subprogram body, insert the pragma in the body declarations.
 
-            elsif Nkind (N) = N_Package_Body then
+            elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
                if No (Declarations (N)) then
                   Set_Declarations (N, New_List);
                end if;

gcc/ada/sem_ch4.adb

@@ -1037,7 +1037,7 @@ package body Sem_Ch4 is
          --  function that returns a pointer_to_procedure which is the entity
          --  being called. Finally, F (X) may be a call to a parameterless
          --  function that returns a pointer to a function with parameters.
-         --  Note that if F return an access to subprogram whose designated
+         --  Note that if F returns an access-to-subprogram whose designated
          --  type is an array, F (X) cannot be interpreted as an indirect call
          --  through the result of the call to F.
 
@@ -3003,7 +3003,7 @@ package body Sem_Ch4 is
          return;
       end if;
 
-      --  An indexing requires at least one actual.The name of the call cannot
+      --  An indexing requires at least one actual. The name of the call cannot
       --  be an implicit indirect call, so it cannot be a generated explicit
       --  dereference.
 
@@ -3057,7 +3057,7 @@ package body Sem_Ch4 is
       if not Norm_OK then
 
          --  If an indirect call is a possible interpretation, indicate
-         --  success to the caller. This may be an indecing of an explicit
+         --  success to the caller. This may be an indexing of an explicit
          --  dereference of a call that returns an access type (see above).
 
          if Is_Indirect

gcc/ada/sem_ch6.adb

@@ -23,6 +23,7 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+with Aspects;  use Aspects;
 with Atree;    use Atree;
 with Checks;   use Checks;
 with Debug;    use Debug;
@@ -2671,18 +2672,16 @@ package body Sem_Ch6 is
          end if;
       end if;
 
-      --  Ada 2012 aspects may appear in a subprogram body, but only if there
-      --  is no previous spec. Ditto for a subprogram stub that does not have
-      --  a corresponding spec, but for which there may also be a spec_id.
+      --  Language-defined aspects cannot appear in a subprogram body if the
+      --  corresponding spec already has aspects. Exception to this rule are
+      --  certain user-defined aspects. Aspects that apply to a body stub are
+      --  moved to the proper body. Do not emit an error in this case.
 
       if Has_Aspects (N) then
-
-         --  Aspects that apply to a body stub are relocated to the proper
-         --  body. Do not emit an error in this case.
-
          if Present (Spec_Id)
            and then Nkind (N) not in N_Body_Stub
            and then Nkind (Parent (N)) /= N_Subunit
+           and then not Aspects_On_Body_OK (N)
          then
             Error_Msg_N
               ("aspect specifications must appear in subprogram declaration",

gcc/ada/sem_prag.adb

@@ -16406,7 +16406,7 @@ package body Sem_Prag is
             --  the consistency between modes of visible/private declarations
             --  and body declarations/statements.
 
-            procedure Check_Conformance
+            procedure Check_Spark_Mode_Conformance
               (Governing_Id : Entity_Id;
                New_Id       : Entity_Id);
             --  Verify the "monotonicity" of SPARK modes between two entities.
@@ -16450,11 +16450,11 @@ package body Sem_Prag is
                end if;
             end Chain_Pragma;
 
-            -----------------------
-            -- Check_Conformance --
-            -----------------------
+            ----------------------------------
+            -- Check_Spark_Mode_Conformance --
+            ----------------------------------
 
-            procedure Check_Conformance
+            procedure Check_Spark_Mode_Conformance
               (Governing_Id : Entity_Id;
                New_Id       : Entity_Id)
             is
@@ -16486,7 +16486,7 @@ package body Sem_Prag is
                     (Governing_Mode => Gov_Prag,
                      New_Mode       => New_Prag);
                end if;
-            end Check_Conformance;
+            end Check_Spark_Mode_Conformance;
 
             ------------------------------
             -- Check_Pragma_Conformance --
@@ -16689,7 +16689,13 @@ package body Sem_Prag is
                   Body_Id := Defining_Unit_Name (Context);
 
                   Chain_Pragma (Body_Id, N);
-                  Check_Conformance (Spec_Id, Body_Id);
+
+                  --  Verify that the SPARK modes are consistent between
+                  --  body and spec, if any.
+
+                  if Present (Spec_Id) then
+                     Check_Spark_Mode_Conformance (Spec_Id, Body_Id);
+                  end if;
 
                --  The pragma applies to the statements of a package body
 
@@ -16705,7 +16711,7 @@ package body Sem_Prag is
                   Body_Id := Defining_Unit_Name (Context);
 
                   Chain_Pragma (Body_Id, N);
-                  Check_Conformance (Spec_Id, Body_Id);
+                  Check_Spark_Mode_Conformance (Spec_Id, Body_Id);
 
                --  The pragma does not apply to a legal construct, issue error