MatCat.OpenSource/8sa1-gcc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Default_Initial_Condition assertion policy is now RM defined

Browse Source 
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.
This commit is contained in:
Piotr Trojanek 2020-11-03 20:44:03 +01:00 committed by Pierre-Marie de Rodat
parent 79b149b19d
commit 8ff03120fc
2 changed files with 52 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

52
gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
View 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
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 |
Default_Initial_Condition |
Ghost |
Initial_Condition |
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 |
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

52
gcc/ada/gnat_rm.texi
View 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
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 |
Default_Initial_Condition |
Ghost |
Initial_Condition |
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 |
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