Default_Initial_Condition was created for SPARK, but has been adopted by Ada 202x, so now it is an RM defined aspect and an assertion policy.
Tested on x86_64-pc-linux-gnu, committed on trunk
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.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
@@ -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
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
@@ -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
