From: Ed Schonberg <schonberg@adacore.com>
Date: Mon, 1 Aug 2011 08:59:50 +0000 (+0000)
Subject: sem_attr.adb (Analyze_Attribute, [...]): Handle properly a quantified expression... 
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=67e28ef818ad694185e3738dad037864d2c51240;p=gcc.git

sem_attr.adb (Analyze_Attribute, [...]): Handle properly a quantified expression that appears within a postcondition and...

2011-08-01  Ed Schonberg  <schonberg@adacore.com>

	* sem_attr.adb (Analyze_Attribute, case 'Result): Handle properly a
	quantified expression that appears within a postcondition and uses the
	Ada2012 'Result attribute.

From-SVN: r177001
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3ca191c5769..46032fdff3b 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2011-08-01  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_attr.adb (Analyze_Attribute, case 'Result): Handle properly a
+	quantified expression that appears within a postcondition and uses the
+	Ada2012 'Result attribute.
+
 2011-07-28  Rainer Orth  <ro@CeBiTec.Uni-Bielefeld.DE>
 
 	* init.c (__gnat_error_handler): Cast reason to int.
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index b2c7a835674..734c1a723c6 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -3947,14 +3947,29 @@ package body Sem_Attr is
       ------------
 
       when Attribute_Result => Result : declare
-         CS : Entity_Id := Current_Scope;
-         PS : Entity_Id := Scope (CS);
+         CS : Entity_Id;
+         --  The enclosing scope, excluding loops for quantified expressions
+
+         PS : Entity_Id;
+         --  During analysis, CS is the postcondition subprogram and PS the
+         --  source subprogram to which the postcondition applies. During
+         --  pre-analysis, CS is the scope of the subprogram declaration.
 
       begin
+         --  Find enclosing scopes, excluding loops
+
+         CS := Current_Scope;
+         while Ekind (CS) = E_Loop loop
+            CS := Scope (CS);
+         end loop;
+
+         PS := Scope (CS);
+
          --  If the enclosing subprogram is always inlined, the enclosing
          --  postcondition will not be propagated to the expanded call.
 
-         if Has_Pragma_Inline_Always (PS)
+         if not In_Spec_Expression
+           and then Has_Pragma_Inline_Always (PS)
            and then Warn_On_Redundant_Constructs
          then
             Error_Msg_N
@@ -3994,9 +4009,7 @@ package body Sem_Attr is
          --  current one.
 
          else
-            while Present (CS)
-              and then CS /= Standard_Standard
-            loop
+            while Present (CS) and then CS /= Standard_Standard loop
                if Chars (CS) = Name_uPostconditions then
                   exit;
                else
@@ -4038,7 +4051,7 @@ package body Sem_Attr is
             else
                Error_Attr
                  ("% attribute can only appear" &
-                   "  in function Postcondition pragma", P);
+                   " in function Postcondition pragma", P);
             end if;
          end if;
       end Result;