[multiple changes]

2014-07-30  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.ads Add a comment explaining why SPARK 2014 aspects are
	not delayed. Update the delay status of most SPARK 2014 aspects.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Update all calls
	to Decorate_Aspect_And_Pragma and Insert_Delayed_Pragma to refert
	to Decorate and Insert_Pragma. Add various comments concerning
	the delay status of several SPARK 2014 aspects. The insertion
	of Refined_State now uses routine Insert_After_SPARK_Mode.
	(Decorate): New routine.
	(Decorate_Aspect_And_Pragma): Removed.
	(Insert_Delayed_Pragma): Removed.
	(Insert_Pragma): New routine.

2014-07-30  Ed Schonberg  <schonberg@adacore.com>

	* inline.adb (Expand_Inlined_Call): In GNATprove mode, emit
	only a warning, not an error on an attempt to inline a recursive
	subprogram.

From-SVN: r213243

gcc/ada/ChangeLog

+2014-07-30  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* aspects.ads Add a comment explaining why SPARK 2014 aspects are
+	not delayed. Update the delay status of most SPARK 2014 aspects.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Update all calls
+	to Decorate_Aspect_And_Pragma and Insert_Delayed_Pragma to refert
+	to Decorate and Insert_Pragma. Add various comments concerning
+	the delay status of several SPARK 2014 aspects. The insertion
+	of Refined_State now uses routine Insert_After_SPARK_Mode.
+	(Decorate): New routine.
+	(Decorate_Aspect_And_Pragma): Removed.
+	(Insert_Delayed_Pragma): Removed.
+	(Insert_Pragma): New routine.
+
+2014-07-30  Ed Schonberg  <schonberg@adacore.com>
+
+	* inline.adb (Expand_Inlined_Call): In GNATprove mode, emit
+	only a warning, not an error on an attempt to inline a recursive
+	subprogram.
+
 2014-07-30  Robert Dewar  <dewar@adacore.com>
 
 	* g-forstr.adb: Minor code reorganization (use J rather than I

gcc/ada/aspects.ads

@@ -543,6 +543,14 @@ package Aspects is
    --  information from the parent type, which must be frozen at that point
    --  (since freezing the derived type first freezes the parent type).
 
+   --  SPARK 2014 aspects do not follow the general delay mechanism as they
+   --  act as annotations and cannot modify the attributes of their related
+   --  constructs. To handle forward references in such aspects, the compiler
+   --  delays the analysis of their respective pragmas by collecting them in
+   --  N_Contract nodes. The pragmas are then analyzed at the end of the
+   --  declarative region which contains the related construct. For details,
+   --  see routines Analyze_xxx_In_Decl_Part.
+
    --  The following shows which aspects are delayed. There are three cases:
 
    type Delay_Type is
@@ -593,12 +601,10 @@ package Aspects is
       Aspect_Asynchronous                 => Always_Delay,
       Aspect_Attach_Handler               => Always_Delay,
       Aspect_Constant_Indexing            => Always_Delay,
-      Aspect_Contract_Cases               => Always_Delay,
       Aspect_CPU                          => Always_Delay,
       Aspect_Default_Iterator             => Always_Delay,
       Aspect_Default_Value                => Always_Delay,
       Aspect_Default_Component_Value      => Always_Delay,
-      Aspect_Depends                      => Always_Delay,
       Aspect_Discard_Names                => Always_Delay,
       Aspect_Dispatching_Domain           => Always_Delay,
       Aspect_Dynamic_Predicate            => Always_Delay,
@@ -607,15 +613,12 @@ package Aspects is
       Aspect_External_Tag                 => Always_Delay,
       Aspect_Export                       => Always_Delay,
       Aspect_Favor_Top_Level              => Always_Delay,
-      Aspect_Global                       => Always_Delay,
       Aspect_Implicit_Dereference         => Always_Delay,
       Aspect_Import                       => Always_Delay,
       Aspect_Independent                  => Always_Delay,
       Aspect_Independent_Components       => Always_Delay,
       Aspect_Inline                       => Always_Delay,
       Aspect_Inline_Always                => Always_Delay,
-      Aspect_Initial_Condition            => Always_Delay,
-      Aspect_Initializes                  => Always_Delay,
       Aspect_Input                        => Always_Delay,
       Aspect_Interrupt_Handler            => Always_Delay,
       Aspect_Interrupt_Priority           => Always_Delay,
@@ -639,9 +642,6 @@ package Aspects is
       Aspect_Pure                         => Always_Delay,
       Aspect_Pure_Function                => Always_Delay,
       Aspect_Read                         => Always_Delay,
-      Aspect_Refined_Depends              => Always_Delay,
-      Aspect_Refined_Global               => Always_Delay,
-      Aspect_Refined_State                => Always_Delay,
       Aspect_Relative_Deadline            => Always_Delay,
       Aspect_Remote_Access_Type           => Always_Delay,
       Aspect_Remote_Call_Interface        => Always_Delay,
@@ -671,13 +671,21 @@ package Aspects is
       Aspect_Annotate                     => Never_Delay,
       Aspect_Async_Readers                => Never_Delay,
       Aspect_Async_Writers                => Never_Delay,
+      Aspect_Contract_Cases               => Never_Delay,
       Aspect_Convention                   => Never_Delay,
+      Aspect_Depends                      => Never_Delay,
       Aspect_Dimension                    => Never_Delay,
       Aspect_Dimension_System             => Never_Delay,
       Aspect_Effective_Reads              => Never_Delay,
       Aspect_Effective_Writes             => Never_Delay,
+      Aspect_Global                       => Never_Delay,
+      Aspect_Initial_Condition            => Never_Delay,
+      Aspect_Initializes                  => Never_Delay,
       Aspect_Part_Of                      => Never_Delay,
+      Aspect_Refined_Depends              => Never_Delay,
+      Aspect_Refined_Global               => Never_Delay,
       Aspect_Refined_Post                 => Never_Delay,
+      Aspect_Refined_State                => Never_Delay,
       Aspect_SPARK_Mode                   => Never_Delay,
       Aspect_Synchronization              => Never_Delay,
       Aspect_Test_Case                    => Never_Delay,

gcc/ada/inline.adb

@@ -3619,7 +3619,19 @@ package body Inline is
       A := First_Actual (N);
       while Present (F) loop
          if Present (Renamed_Object (F)) then
-            Error_Msg_N ("cannot inline call to recursive subprogram", N);
+
+            --  If expander is active, it's an error to try to inline a
+            --  recursive program. In GNATprove mode, just indicate that
+            --  the inlining will not happen.
+
+            if Expander_Active then
+               Error_Msg_N ("cannot inline call to recursive subprogram", N);
+
+            else
+               Cannot_Inline
+                 ("cannot inline call to recursive subprogram?", N, Subp);
+            end if;
+
             return;
          end if;