[multiple changes]

2014-06-13  Yannick Moy  <moy@adacore.com>

	* sem_warn.adb (Check_Unset_References): Take
	case of Refined_Post into account in Within_Postcondition check.

2014-06-13  Hristian Kirtchev  <kirtchev@adacore.com>

	* freeze.adb (Freeze_Record_Type): Volatile types are not allowed in
	SPARK.

2014-06-13  Yannick Moy  <moy@adacore.com>

	* sem_ch13.adb (Analyze_Aspect_Specifications/Aspect_Import,
	Aspect_Export): Consider that variables may be set outside the program.

From-SVN: r211611

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b2cdbc578b8b5363f942f637da7dc5925b973baa..3a0b1e6567ed7dd4cc2d81a6b0157bd1adbd3119 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,18 @@
+2014-06-13  Yannick Moy  <moy@adacore.com>
+
+       * sem_warn.adb (Check_Unset_References): Take
+       case of Refined_Post into account in Within_Postcondition check.
+
+2014-06-13  Hristian Kirtchev  <kirtchev@adacore.com>
+
+       * freeze.adb (Freeze_Record_Type): Volatile types are not allowed in
+       SPARK.
+
+2014-06-13  Yannick Moy  <moy@adacore.com>
+
+       * sem_ch13.adb (Analyze_Aspect_Specifications/Aspect_Import,
+       Aspect_Export): Consider that variables may be set outside the program.
+
 2014-06-13  Robert Dewar  <dewar@adacore.com>
 
        * back_end.adb (Make_Id): New function.

diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 97d21d38d3decfabcf6f5eaeb19502dfe0bb1d3f..bfd15f3bd18c69179a9db2287efb14ae7c413e10 100644 (file)
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -3359,18 +3359,11 @@ package body Freeze is
          --  they are not standard Ada legality rules.
 
          if SPARK_Mode = On then
-            if Is_SPARK_Volatile (Rec) then
-
-               --  A discriminated type cannot be volatile (SPARK RM C.6(4))
-
-               if Has_Discriminants (Rec) then
-                  Error_Msg_N ("discriminated type & cannot be volatile", Rec);
 
-               --  A tagged type cannot be volatile (SPARK RM C.6(5))
+            --  Volatile types are not allowed in SPARK (SPARK RM C.6(1))
 
-               elsif Is_Tagged_Type (Rec) then
-                  Error_Msg_N ("tagged type & cannot be volatile", Rec);
-               end if;
+            if Is_SPARK_Volatile (Rec) then
+               Error_Msg_N ("volatile type not allowed", Rec);
 
             --  A non-volatile record type cannot contain volatile components
             --  (SPARK RM C.6(2)). The check is performed at freeze point

diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 3e1398ba163692fc3e8a6af46d630d0a413826ba..31256d22f8f6cf175c4acd18715d793d20a18bdf 100644 (file)
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1603,7 +1603,7 @@ package body Sem_Ch13 is
                      goto Continue;
                   end if;
 
-                  --  For case of address aspect, we don't consider that we
+                  --  For the case of aspect Address, we don't consider that we
                   --  know the entity is never set in the source, since it is
                   --  is likely aliasing is occurring.
 
@@ -2691,6 +2691,19 @@ package body Sem_Ch13 is
 
                   elsif A_Id = Aspect_Import or else A_Id = Aspect_Export then
 
+                     --  For the case of aspects Import and Export, we don't
+                     --  consider that we know the entity is never set in the
+                     --  source, since it is is likely modified outside the
+                     --  program.
+
+                     --  Note: one might think that the analysis of the
+                     --  resulting pragma would take care of that, but
+                     --  that's not the case since it won't be from source.
+
+                     if Ekind (E) = E_Variable then
+                        Set_Never_Set_In_Source (E, False);
+                     end if;
+
                      --  Verify that there is an aspect Convention that will
                      --  incorporate the Import/Export aspect, and eventual
                      --  Link/External names.

diff --git a/gcc/ada/sem_warn.adb b/gcc/ada/sem_warn.adb
index 0043ef61b7fefb1b1d36cf3913773a5933e06fe3..4c2f78c2bc29339c4a25ce63e4e6d316b773b672 100644 (file)
--- a/gcc/ada/sem_warn.adb
+++ b/gcc/ada/sem_warn.adb
@@ -1810,8 +1810,9 @@ package body Sem_Warn is
                      SE : constant Entity_Id := Scope (E);
 
                      function Within_Postcondition return Boolean;
-                     --  Returns True iff N is within a Postcondition, an
-                     --  Ensures component in a Test_Case, or a Contract_Cases.
+                     --  Returns True iff N is within a Postcondition, a
+                     --  Refined_Post, an Ensures component in a Test_Case,
+                     --  or a Contract_Cases.
 
                      --------------------------
                      -- Within_Postcondition --
@@ -1826,6 +1827,7 @@ package body Sem_Warn is
                            if Nkind (Nod) = N_Pragma
                              and then Nam_In (Pragma_Name (Nod),
                                               Name_Postcondition,
+                                              Name_Refined_Post,
                                               Name_Contract_Cases)
                            then
                               return True;