[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f0cf6b87d4b9ad84c961ecf1d7728b751da89d84..84f071b4c6caf5ab104ed588646744138b7ef3b6 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/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

diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index cd592113d4540d9a36a573140fbb91fd42b389d0..660a37a79a96b47be3a06bf0be3209642bdf44a5 100644 (file)
--- a/gcc/ada/einfo.adb
+++ b/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;
 

diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 9dbc54b77bc10ef11c0f46fca3f4aecd2a4bb418..e006455dbc270669cfbf61e56172cfab8607226a 100644 (file)
--- a/gcc/ada/einfo.ads
+++ b/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

diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 86c492566c18de54b14b65c0e2e0ac615959d6f1..abcec64c973116ce2aebad221917926e79ec5c4f 100644 (file)
--- a/gcc/ada/sem_ch4.adb
+++ b/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)))))

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index fbd955b8f93b7a7f2060201e2c8cc2cb81916709..a3711c8353ddbbbe208bc79a2035e6e7c0d36354 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/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;
 

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index f221ed4457c92721b1b5345f31243cad13d63c35..8e08367047cb15898002099c670e5af2c6242bca 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/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)

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 19ba490b21615e356281613821f31c4eb3fc15f8..85c8592959ff70514bb068e6af59d3744fd07730 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/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);
 

diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 4fb30477f2e0bd173f01deec9d0bf87ff0d63dc8..6aa28f2153a1592264ad14c1701377297c7a23cd 100644 (file)
--- a/gcc/ada/sinfo.ads
+++ b/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