[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

gcc/ada/ChangeLog

+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.

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

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.

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;