[Ada] Default_Initial_Condition assertion policy is now RM defined
authorPiotr Trojanek <trojanek@adacore.com>
Tue, 3 Nov 2020 19:44:03 +0000 (20:44 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Fri, 27 Nov 2020 09:15:55 +0000 (04:15 -0500)
gcc/ada/

* doc/gnat_rm/implementation_defined_pragmas.rst:
(Assertion_Policy): Move "Default_Initial_Condition" from
ID_ASSERTION_KIND to RM_ASSERTION_KIND section.
* gnat_rm.texi: Regenerate.

gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
gcc/ada/gnat_rm.texi

index 2fad1d6..f8a62a5 100644 (file)
@@ -434,33 +434,33 @@ Syntax::
 
   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 ::= Assertions                |
-                        Assert_And_Cut            |
-                        Assume                    |
-                        Contract_Cases            |
-                        Debug                     |
-                        Default_Initial_Condition |
-                        Ghost                     |
-                        Initial_Condition         |
-                        Invariant                 |
-                        Invariant'Class           |
-                        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 ::= Assertions           |
+                        Assert_And_Cut       |
+                        Assume               |
+                        Contract_Cases       |
+                        Debug                |
+                        Ghost                |
+                        Initial_Condition    |
+                        Invariant            |
+                        Invariant'Class      |
+                        Loop_Invariant       |
+                        Loop_Variant         |
+                        Postcondition        |
+                        Precondition         |
+                        Predicate            |
+                        Refined_Post         |
+                        Statement_Assertions |
                         Subprogram_Variant
 
   POLICY_IDENTIFIER ::= Check | Disable | Ignore | Suppressible
index c51c605..b6ea1e4 100644 (file)
@@ -1807,33 +1807,33 @@ pragma Assertion_Policy (
 
 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 ::= Assertions                |
-                      Assert_And_Cut            |
-                      Assume                    |
-                      Contract_Cases            |
-                      Debug                     |
-                      Default_Initial_Condition |
-                      Ghost                     |
-                      Initial_Condition         |
-                      Invariant                 |
-                      Invariant'Class           |
-                      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 ::= Assertions           |
+                      Assert_And_Cut       |
+                      Assume               |
+                      Contract_Cases       |
+                      Debug                |
+                      Ghost                |
+                      Initial_Condition    |
+                      Invariant            |
+                      Invariant'Class      |
+                      Loop_Invariant       |
+                      Loop_Variant         |
+                      Postcondition        |
+                      Precondition         |
+                      Predicate            |
+                      Refined_Post         |
+                      Statement_Assertions |
                       Subprogram_Variant
 
 POLICY_IDENTIFIER ::= Check | Disable | Ignore | Suppressible