diff options
author | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-01-29 17:23:31 +0100 |
---|---|---|
committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-01-29 17:23:31 +0100 |
commit | 4f7c83caa328ea011365f786c19953af274bb0c8 (patch) | |
tree | bf717a9c20a91caa3da27d7234d94e74e57b7ce8 | |
parent | 385e1a992afbbff6049b69325f211fad49e0231a (diff) | |
download | gcc-4f7c83caa328ea011365f786c19953af274bb0c8.zip gcc-4f7c83caa328ea011365f786c19953af274bb0c8.tar.gz gcc-4f7c83caa328ea011365f786c19953af274bb0c8.tar.bz2 |
[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
-rw-r--r-- | gcc/ada/ChangeLog | 19 | ||||
-rw-r--r-- | gcc/ada/einfo.adb | 3 | ||||
-rw-r--r-- | gcc/ada/einfo.ads | 2 | ||||
-rw-r--r-- | gcc/ada/sem_ch4.adb | 4 | ||||
-rw-r--r-- | gcc/ada/sem_prag.adb | 4 | ||||
-rw-r--r-- | gcc/ada/sem_res.adb | 1 | ||||
-rw-r--r-- | gcc/ada/sem_util.adb | 7 | ||||
-rw-r--r-- | gcc/ada/sinfo.ads | 1 |
8 files changed, 39 insertions, 2 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f0cf6b8..84f071b 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,24 @@ 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 placement is not in a package. diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index cd59211..660a37a 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 9dbc54b7..e006455 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 86c4925..abcec64 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 fbd955b..a3711c8 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 f221ed4..8e08367 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 19ba490..85c8592 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 4fb3047..6aa28f2 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 |