diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2013-10-10 14:26:07 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2013-10-10 14:26:07 +0200 |
| commit | 4169c2d220718a78e661a605ebd838b0ad5a40bd (patch) | |
| tree | b74e92dafacc02652acb04902f680496d7b0355b /gcc/ada/sem_prag.adb | |
| parent | aa500b7a972aebff7375a093c2a7d90aad427b65 (diff) | |
| download | gcc-4169c2d220718a78e661a605ebd838b0ad5a40bd.tar.gz | |
[multiple changes]
2013-10-10 Robert Dewar <dewar@adacore.com>
* gnat_rm.texi: Refined_Pre and Refined_Post are now allowed as
assertion identifiers for pragma Assertion_Policy.
* sem_prag.adb (Is_Valid_Assertion_Kind): Add Refined_Pre/Refined_Post
* sem_ch13.adb: Minor reformatting.
2013-10-10 Pascal Obry <obry@adacore.com>
* prj-conf.adb: Code refactoring.
From-SVN: r203361
Diffstat (limited to 'gcc/ada/sem_prag.adb')
| -rw-r--r-- | gcc/ada/sem_prag.adb | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index e698d97ef11..ef8df47cdee 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -9127,10 +9127,10 @@ package body Sem_Prag is -- Postcondition | -- Precondition | -- Predicate | + -- Refined_Post | + -- Refined_Pre | -- Statement_Assertions - -- Shouldn't Refined_Pre be in this list??? - -- Note: The RM_ASSERTION_KIND list is language-defined, and the -- ID_ASSERTION_KIND list contains implementation-defined additions -- recognized by GNAT. The effect is to control the behavior of @@ -19482,6 +19482,8 @@ package body Sem_Prag is Name_Postcondition | Name_Precondition | Name_Predicate | + Name_Refined_Post | + Name_Refined_Pre | Name_Statement_Assertions => return True; when others => return False; |