From ae8c56262d635eefdb32fc4e1b8d896453348c00 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Thu, 5 Nov 2020 10:14:36 +0100 Subject: [PATCH] [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. --- gcc/ada/sa_messages.ads | 2 +- 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 11da9fc8073..1f6fca8c939 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 1bcbb25d5f9..094591b5ec9 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 -- 2.30.2