[Ada] Sync doc and code for pragma Assertion_Policy
authorPiotr Trojanek <trojanek@adacore.com>
Tue, 3 Nov 2020 18:43:07 +0000 (19:43 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Fri, 27 Nov 2020 09:15:54 +0000 (04:15 -0500)
gcc/ada/

* doc/gnat_rm/implementation_defined_pragmas.rst
(Assertion_Policy): Add "Default_Initial_Condition",
"Initial_Condition" and "Subprogram_Variant".
* gnat_rm.texi: Regenerate.

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

index ddf60ec3dba15aca154707f7cf6c50a097c30e32..2fad1d656a040f0c9311bdb579bf84ebad9c5de3 100644 (file)
@@ -444,21 +444,24 @@ Syntax::
                         Type_Invariant       |
                         Type_Invariant'Class
 
-  ID_ASSERTION_KIND ::= Assertions           |
-                        Assert_And_Cut       |
-                        Assume               |
-                        Contract_Cases       |
-                        Debug                |
-                        Ghost                |
-                        Invariant            |
-                        Invariant'Class      |
-                        Loop_Invariant       |
-                        Loop_Variant         |
-                        Postcondition        |
-                        Precondition         |
-                        Predicate            |
-                        Refined_Post         |
-                        Statement_Assertions
+  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      |
+                        Subprogram_Variant
 
   POLICY_IDENTIFIER ::= Check | Disable | Ignore | Suppressible
 
index 66665206c4c9f56408b8f56867d75e38adc51b2c..c51c605a9f263da0301fe4afb07fd7f7c19bc272 100644 (file)
@@ -21,7 +21,7 @@
 
 @copying
 @quotation
-GNAT Reference Manual , Nov 19, 2020
+GNAT Reference Manual , Nov 20, 2020
 
 AdaCore
 
@@ -1817,21 +1817,24 @@ RM_ASSERTION_KIND ::= Assert               |
                       Type_Invariant       |
                       Type_Invariant'Class
 
-ID_ASSERTION_KIND ::= Assertions           |
-                      Assert_And_Cut       |
-                      Assume               |
-                      Contract_Cases       |
-                      Debug                |
-                      Ghost                |
-                      Invariant            |
-                      Invariant'Class      |
-                      Loop_Invariant       |
-                      Loop_Variant         |
-                      Postcondition        |
-                      Precondition         |
-                      Predicate            |
-                      Refined_Post         |
-                      Statement_Assertions
+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      |
+                      Subprogram_Variant
 
 POLICY_IDENTIFIER ::= Check | Disable | Ignore | Suppressible
 @end example