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 /gcc/ada/sem_util.adb | |
| 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
Diffstat (limited to 'gcc/ada/sem_util.adb')
| -rw-r--r-- | gcc/ada/sem_util.adb | 7 |
1 files changed, 6 insertions, 1 deletions
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); |