From: charlet Date: Wed, 29 Jan 2014 16:23:31 +0000 (+0000) Subject: 2014-01-29 Hristian Kirtchev X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=35c923a021c88e96c8ff422ed7f1e66f612cc45e;p=thirdparty%2Fgcc.git 2014-01-29 Hristian Kirtchev * 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 * sem_ch4.adb (Find_Equality_Types, Try_One_Interp): within an instance, null is compatible with any access type. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@207269 138bc75d-0d04-0410-961f-82ee72b054a4 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f0cf6b87d4b9..84f071b4c6ca 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,22 @@ +2014-01-29 Hristian Kirtchev + + * 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 + + * sem_ch4.adb (Find_Equality_Types, Try_One_Interp): within an instance, + null is compatible with any access type. + 2014-01-29 Hristian Kirtchev * 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 cd592113d454..660a37a79a96 100644 --- 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 9dbc54b77bc1..e006455dbc27 100644 --- 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 86c492566c18..abcec64c9731 100644 --- 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 fbd955b8f93b..a3711c8353dd 100644 --- 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 f221ed4457c9..8e08367047cb 100644 --- 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 19ba490b2161..85c8592959ff 100644 --- 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 4fb30477f2e0..6aa28f2153a1 100644 --- 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