[multiple changes]

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

	* einfo.adb (Get_Pragma): Handle the retrieval of pragma Refined_Post.
	* einfo.ads (Get_Pragma): Update the comment on special pragmas
	handled by this routine.
	* sem_prag.adb (Analyze_Pragma): Add a legal pragma Refined_Post
	to the contract of the related subprogram body.
	* sem_util.adb (Add_Contract_Item): Handle the insertion of
	pragma Refined_Post into the contract of a subprogram body.
	* sinfo.ads Update the documentation of node N_Contract.
	* sem_res.adb (Resolve_Entity_Name): Add a guard
	to detect abstract states and variables only when checking the
	SPARK 2014 rules concerning volatile object placement.

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

	* sem_ch4.adb (Find_Equality_Types, Try_One_Interp): within an instance,
	null is compatible with any access type.

From-SVN: r207269

gcc/ada/ChangeLog

@@ -1,3 +1,22 @@
+2014-01-29  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* einfo.adb (Get_Pragma): Handle the retrieval of pragma Refined_Post.
+	* einfo.ads (Get_Pragma): Update the comment on special pragmas
+	handled by this routine.
+	* sem_prag.adb (Analyze_Pragma): Add a legal pragma Refined_Post
+	to the contract of the related subprogram body.
+	* sem_util.adb (Add_Contract_Item): Handle the insertion of
+	pragma Refined_Post into the contract of a subprogram body.
+	* sinfo.ads Update the documentation of node N_Contract.
+	* sem_res.adb (Resolve_Entity_Name): Add a guard
+	to detect abstract states and variables only when checking the
+	SPARK 2014 rules concerning volatile object placement.
+
+2014-01-29  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch4.adb (Find_Equality_Types, Try_One_Interp): within an instance,
+	null is compatible with any access type.
+
 2014-01-29  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_util.adb (Find_Placement_In_State_Space): Assume that the default

gcc/ada/einfo.adb

@@ -6455,7 +6455,8 @@ package body Einfo is
                   Id = Pragma_Test_Case;
       Is_PPC : constant Boolean :=
                   Id = Pragma_Precondition      or else
-                  Id = Pragma_Postcondition;
+                  Id = Pragma_Postcondition     or else
+                  Id = Pragma_Refined_Post;
 
       In_Contract : constant Boolean := Is_CDG or Is_CTC or Is_PPC;
 

gcc/ada/einfo.ads

@@ -7509,7 +7509,9 @@ package Einfo is
    --    Postcondition
    --    Refined_Depends
    --    Refined_Global
+   --    Refined_Post
    --    Refined_State
+   --    Test_Case
 
    function Get_Record_Representation_Clause (E : Entity_Id) return Node_Id;
    --  Searches the Rep_Item chain for a given entity E, for a record

gcc/ada/sem_ch4.adb

@@ -5892,6 +5892,9 @@ package body Sem_Ch4 is
 
          --  In Ada 2005, the equality on anonymous access types is declared
          --  in Standard, and is always visible.
+         --  In an instance, the type may have been immediately visible.
+         --  Either the types are compatible, or one operand is universal
+         --  (numeric or null).
 
          elsif In_Open_Scopes (Scope (Bas))
            or else Is_Potentially_Use_Visible (Bas)
@@ -5900,6 +5903,7 @@ package body Sem_Ch4 is
            or else (In_Instance
                      and then
                        (First_Subtype (T1) = First_Subtype (Etype (R))
+                         or else Nkind (R) = N_Null
                          or else
                            (Is_Numeric_Type (T1)
                              and then Is_Universal_Numeric_Type (Etype (R)))))

gcc/ada/sem_prag.adb

@@ -18475,6 +18475,10 @@ package body Sem_Prag is
                        ("pragma % does not mention function result?T?");
                   end if;
                end if;
+
+               --  Chain the pragma on the contract for easy retrieval
+
+               Add_Contract_Item (N, Body_Id);
             end if;
          end Refined_Post;
 

gcc/ada/sem_res.adb

@@ -6513,6 +6513,7 @@ package body Sem_Res is
       --  standard Ada legality rules.
 
       if SPARK_Mode = On
+        and then Ekind_In (E, E_Abstract_State, E_Variable)
         and then Is_SPARK_Volatile_Object (E)
         and then
           (Async_Writers_Enabled (E)

gcc/ada/sem_util.adb

@@ -345,9 +345,14 @@ package body Sem_Util is
       --  are:
       --    Refined_Depends
       --    Refined_Global
+      --    Refined_Post
 
       elsif Ekind (Id) = E_Subprogram_Body then
-         if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then
+         if Nam = Name_Refined_Post then
+            Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
+            Set_Pre_Post_Conditions (Items, Prag);
+
+         elsif Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then
             Set_Next_Pragma (Prag, Classifications (Items));
             Set_Classifications (Items, Prag);
 

gcc/ada/sinfo.ads

@@ -7260,6 +7260,7 @@ package Sinfo is
       --    Postcondition
       --    Pre
       --    Precondition
+      --    Refined_Post
       --  The ordering in the list is in LIFO fashion.
 
       --  Note that there might be multiple preconditions or postconditions