diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2020-11-03 19:43:07 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-11-27 04:15:54 -0500 |
| commit | 79b149b19d9079f67dfb2c5d7b99aa103f108e19 (patch) | |
| tree | 8dda33aa0ee60e260acbb3a59ab4d372ee561e09 /gcc/ada/doc | |
| parent | 3e9238fa6435af6361fdb807525de75e1b306263 (diff) | |
| download | gcc-79b149b19d9079f67dfb2c5d7b99aa103f108e19.zip gcc-79b149b19d9079f67dfb2c5d7b99aa103f108e19.tar.gz gcc-79b149b19d9079f67dfb2c5d7b99aa103f108e19.tar.bz2 | |
[Ada] Sync doc and code for pragma Assertion_Policy
gcc/ada/
* doc/gnat_rm/implementation_defined_pragmas.rst
(Assertion_Policy): Add "Default_Initial_Condition",
"Initial_Condition" and "Subprogram_Variant".
* gnat_rm.texi: Regenerate.
Diffstat (limited to 'gcc/ada/doc')
| -rw-r--r-- | gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst | 33 |
1 files changed, 18 insertions, 15 deletions
diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst index ddf60ec..2fad1d6 100644 --- 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 |