gcc/ada/
* doc/gnat_rm/implementation_defined_pragmas.rst
(Assertion_Policy): Add "Default_Initial_Condition",
"Initial_Condition" and "Subprogram_Variant".
* gnat_rm.texi: Regenerate.
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
@copying
@quotation
-GNAT Reference Manual , Nov 19, 2020
+GNAT Reference Manual , Nov 20, 2020
AdaCore
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