2014-01-23 Robert Dewar <dewar@adacore.com>

	* opt.adb (Register_Opt_Config_Switches): Save SPARK_Mode_Pragma
	setting.

2014-01-23  Ed Schonberg  <schonberg@adacore.com>

	* sem_util.adb (Is_Potentially_Unevaluated): Predicate only
	applies to expressions that come from source.
	* sem_attr.adb (Analyze_Attribute, case 'Old): Improve error
	message.
	(Analyze_Attribute, case 'Loop_Entry): Apply SPARK 2014 legality
	rule regarding potentially unevaluated expressions, to prefix
	of attribute.

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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ae2480e..4b3c213 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,18 @@
+2014-01-23  Robert Dewar  <dewar@adacore.com>
+
+       * opt.adb (Register_Opt_Config_Switches): Save SPARK_Mode_Pragma
+       setting.
+
+2014-01-23  Ed Schonberg  <schonberg@adacore.com>
+
+       * sem_util.adb (Is_Potentially_Unevaluated): Predicate only
+       applies to expressions that come from source.
+       * sem_attr.adb (Analyze_Attribute, case 'Old): Improve error
+       message.
+       (Analyze_Attribute, case 'Loop_Entry): Apply SPARK 2014 legality
+       rule regarding potentially unevaluated expressions, to prefix
+       of attribute.
+
 2014-01-23  Ed Schonberg  <schonberg@adacore.com>
 
        * exp_util.adb (Make_Invqriant_Call): If type of expression is

diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb
index 20ecb4f..383f5f4 100644 (file)
--- a/gcc/ada/opt.adb
+++ b/gcc/ada/opt.adb
@@ -64,6 +64,7 @@ package body Opt is
       Polling_Required_Config               := Polling_Required;
       Short_Descriptors_Config              := Short_Descriptors;
       SPARK_Mode_Config                     := SPARK_Mode;
+      SPARK_Mode_Pragma_Config              := SPARK_Mode_Pragma;
       Use_VADS_Size_Config                  := Use_VADS_Size;
 
       --  Reset the indication that Optimize_Alignment was set locally, since

diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 1ce0d83..fdd1d0c 100644 (file)
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -3994,13 +3994,23 @@ package body Sem_Attr is
          Check_References_In_Prefix (Loop_Id);
 
          --  The prefix must denote a static entity if the pragma does not
-         --  apply to the innermost enclosing loop statement.
+         --  apply to the innermost enclosing loop statement, or if it appears
+         --  within a potentially unevaluated epxression.
 
-         if Present (Enclosing_Loop)
-           and then Entity (Identifier (Enclosing_Loop)) /= Loop_Id
-           and then not Is_Entity_Name (P)
+         if Is_Entity_Name (P)
+           or else Nkind (Parent (P)) = N_Object_Renaming_Declaration
          then
-            Error_Attr_P ("prefix of attribute % must denote an entity");
+            null;
+
+         elsif Present (Enclosing_Loop)
+                 and then Entity (Identifier (Enclosing_Loop)) /= Loop_Id
+         then
+            Error_Attr_P ("prefix of attribute % that applies to "
+              & "outer loop must denote an entity");
+
+         elsif Is_Potentially_Unevaluated (P) then
+            Error_Attr_P ("prefix of attribute % that is potentially "
+              & "unevaluated must denote an entity");
          end if;
       end Loop_Entry;
 
@@ -4525,9 +4535,8 @@ package body Sem_Attr is
            and then Is_Potentially_Unevaluated (N)
            and then not Is_Entity_Name (P)
          then
-            Error_Msg_N
-              ("prefix that is potentially unevaluated must denote an entity",
-               N);
+            Error_Attr_P ("prefix of attribute % that is potentially "
+                 & "unevaluated must denote an entity");
          end if;
 
          --  The attribute appears within a pre/postcondition, but refers to

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index be59c9b..9a8428d 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -10334,7 +10334,13 @@ package body Sem_Util is
          Expr := Par;
          Par  := Parent (Par);
 
-         if Nkind (Par) not in N_Subexpr then
+         --  If the context is not an expression, or if is the result of
+         --  expansion of an enclosing construct (such as another attribute)
+         --  the predicate does not apply.
+
+         if Nkind (Par) not in N_Subexpr
+           or else not Comes_From_Source (Par)
+         then
             return False;
          end if;
       end loop;