diff mbox series

[Ada] Sync doc and code for pragma Assertion_Policy

Message ID 20201127091800.GA63235@adacore.com
State New
Headers show
Series [Ada] Sync doc and code for pragma Assertion_Policy | expand

Commit Message

Pierre-Marie de Rodat Nov. 27, 2020, 9:18 a.m. UTC 
In the listing of assertion kinds accepted for pragma Assertion_Policy
some items were wrongly included while other were missing. Now this
listing is synchronized with Sem_Prag.Is_Valid_Assertion_Kind.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

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

Patch

diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
--- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
+++ b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
@@ -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
 


diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -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