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

	* sem_attr.adb (Analyze_Attribute): Attributes 'Old and 'Result
	can now apply to a refined postcondition.
	* sem_ch6.adb (Analyze_Subprogram_Contract): Remove local
	variable Result_Seen. Add variables Case_Prag, Post_Prag,
	Seen_In_Case and Seen_In_Post. Update the mechanism that detects
	whether postconditions and/or constract-cases mention attribute
	'Result and introduce a post-state when applied to functions.
	(Check_Result_And_Post_State): Removed.
	* sem_prag.adb (Analyze_Pragma): Add local variable
	Result_Seen. Verify that the expression of pragma Refined_Post
	mentions attribute 'Result and introduces a post-state.
	* sem_util.ads, sem_util.adb (Check_Result_And_Post_State): New routine.

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

	* exp_ch7.adb (Is_Subprogram_Call): New routine.
	(Process_Transient_Objects): Make variable Must_Hook global with
	respect to all locally declared subprograms. Search the context
	for at least one subprogram call.
	(Requires_Hooking): Removed.

2014-01-20  Claire Dross  <dross@adacore.com>

	* a-cfdlli.ads a-cfhama.ads a-cfhase.ads a-cforma.ads
	* a-cforse.ads a-cofove.ads: Add pragma Annotate (GNATprove,
	External_Axiomatization);



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@206819 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 39 insertions, 21 deletions

diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index a5238585b6c..25e4ef3c624 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -4480,33 +4480,45 @@ package body Exp_Ch7 is
          Last_Object  : Node_Id;
          Related_Node : Node_Id)
       is
-         function Requires_Hooking return Boolean;
-         --  Determine whether the context requires transient variable export
-         --  to the outer finalizer. This scenario arises when the context may
-         --  raise an exception.
+         Must_Hook : Boolean := False;
+         --  Flag denoting whether the context requires transient variable
+         --  export to the outer finalizer.
 
-         ----------------------
-         -- Requires_Hooking --
-         ----------------------
+         function Is_Subprogram_Call (N : Node_Id) return Traverse_Result;
+         --  Determine whether an arbitrary node denotes a subprogram call
 
-         function Requires_Hooking return Boolean is
+         ------------------------
+         -- Is_Subprogram_Call --
+         ------------------------
+
+         function Is_Subprogram_Call (N : Node_Id) return Traverse_Result is
          begin
-            --  The context is either a procedure or function call or an object
-            --  declaration initialized by a function call. Note that in the
-            --  latter case, a function call that returns on the secondary
-            --  stack is usually rewritten into something else. Its proper
-            --  detection requires examination of the original initialization
-            --  expression.
-
-            return Nkind (N) in N_Subprogram_Call
-              or else (Nkind (N) = N_Object_Declaration
-                         and then Nkind (Original_Node (Expression (N))) =
-                                    N_Function_Call);
-         end Requires_Hooking;
+            --  A regular procedure or function call
+
+            if Nkind (N) in N_Subprogram_Call then
+               Must_Hook := True;
+               return Abandon;
+
+            --  Detect a call to a function that returns on the secondary stack
+
+            elsif Nkind (N) = N_Object_Declaration
+              and then Nkind (Original_Node (Expression (N))) = N_Function_Call
+            then
+               Must_Hook := True;
+               return Abandon;
+
+            --  Keep searching
+
+            else
+               return OK;
+            end if;
+         end Is_Subprogram_Call;
+
+         procedure Detect_Subprogram_Call is
+           new Traverse_Proc (Is_Subprogram_Call);
 
          --  Local variables
 
-         Must_Hook : constant Boolean := Requires_Hooking;
          Built     : Boolean := False;
          Desig_Typ : Entity_Id;
          Fin_Block : Node_Id;
@@ -4525,6 +4537,12 @@ package body Exp_Ch7 is
       --  Start of processing for Process_Transient_Objects
 
       begin
+         --  Search the context for at least one subprogram call. If found, the
+         --  machinery exports all transient objects to the enclosing finalizer
+         --  due to the possibility of abnormal call termination.
+
+         Detect_Subprogram_Call (N);
+
          --  Examine all objects in the list First_Object .. Last_Object
 
          Stmt := First_Object;