diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2020-11-05 10:14:36 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-12-14 10:51:48 -0500 |
| commit | ae8c56262d635eefdb32fc4e1b8d896453348c00 (patch) | |
| tree | 600aa21c84b2ae68dfc685f122c01af3997aa3e2 | |
| parent | 3fcb8100aac71b8a109a4f0ceaabd6cfd650b668 (diff) | |
| download | gcc-ae8c56262d635eefdb32fc4e1b8d896453348c00.zip gcc-ae8c56262d635eefdb32fc4e1b8d896453348c00.tar.gz gcc-ae8c56262d635eefdb32fc4e1b8d896453348c00.tar.bz2 | |
[Ada] Update comment for processing of pragma Assertion_Policy
gcc/ada/
* sa_messages.ads: Reference Subprogram_Variant in the comment
for Assertion_Check.
* sem_prag.adb (Analyze_Pragma): Add Subprogram_Variant as an
ID_ASSERTION_KIND; move Default_Initial_Condition as an
RM_ASSERTION_KIND.
| -rw-r--r-- | gcc/ada/sa_messages.ads | 2 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 49 |
2 files changed, 26 insertions, 25 deletions
diff --git a/gcc/ada/sa_messages.ads b/gcc/ada/sa_messages.ads index 11da9fc..1f6fca8 100644 --- a/gcc/ada/sa_messages.ads +++ b/gcc/ada/sa_messages.ads @@ -94,7 +94,7 @@ package SA_Messages is -- type invariant checks (specific and class-wide), and checks for -- implementation-defined assertions such as Assert_And_Cut, Assume, -- Contract_Cases, Default_Initial_Condition, Initial_Condition, - -- Loop_Invariant, Loop_Variant, and Refined_Post. + -- Loop_Invariant, Loop_Variant, Refined_Post, and Subprogram_Variant. -- -- TBD: it might be nice to distinguish these different kinds of assertions -- as is done in SPARK's VC_Kind enumeration type, but any distinction diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 1bcbb25..094591b 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -12903,30 +12903,31 @@ package body Sem_Prag is -- ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND - -- RM_ASSERTION_KIND ::= Assert | - -- Static_Predicate | - -- Dynamic_Predicate | - -- Pre | - -- Pre'Class | - -- Post | - -- Post'Class | - -- Type_Invariant | - -- Type_Invariant'Class - - -- ID_ASSERTION_KIND ::= Assert_And_Cut | - -- Assume | - -- Contract_Cases | - -- Debug | - -- Default_Initial_Condition | - -- Ghost | - -- Initial_Condition | - -- Loop_Invariant | - -- Loop_Variant | - -- Postcondition | - -- Precondition | - -- Predicate | - -- Refined_Post | - -- Statement_Assertions + -- RM_ASSERTION_KIND ::= Assert | + -- Static_Predicate | + -- Dynamic_Predicate | + -- Pre | + -- Pre'Class | + -- Post | + -- Post'Class | + -- Type_Invariant | + -- Type_Invariant'Class | + -- Default_Initial_Condition + + -- ID_ASSERTION_KIND ::= Assert_And_Cut | + -- Assume | + -- Contract_Cases | + -- Debug | + -- Ghost | + -- Initial_Condition | + -- Loop_Invariant | + -- Loop_Variant | + -- Postcondition | + -- Precondition | + -- Predicate | + -- Refined_Post | + -- Statement_Assertions | + -- Subprogram_Variant -- Note: The RM_ASSERTION_KIND list is language-defined, and the -- ID_ASSERTION_KIND list contains implementation-defined additions |