This patch propagates the renaming from "condition" to "case guard" in the
contract grammar to the paragraphs that describe the pragma semantics.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-05-24 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* doc/gnat_rm/implementation_defined_pragmas.rst (Contract_Cases):
Change "condition" to "case guard" after renaming in the contract
grammar.
* gnat_rm.texi: Regenerate.--- gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
+++ gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
@@ -1173,9 +1173,9 @@ are equivalent to
pragma Postcondition (if C2 then Pred2);
-The precondition ensures that one and only one of the conditions is
+The precondition ensures that one and only one of the case guards is
satisfied on entry to the subprogram.
-The postcondition ensures that for the condition that was True on entry,
+The postcondition ensures that for the case guard that was True on entry,
the corrresponding consequence is True on exit. Other consequence expressions
are not evaluated.
@@ -1190,13 +1190,13 @@ expressed as contract cases:
The placement and visibility rules for ``Contract_Cases`` pragmas are
identical to those described for preconditions and postconditions.
-The compiler checks that boolean expressions given in conditions and
-consequences are valid, where the rules for conditions are the same as
+The compiler checks that boolean expressions given in case guards and
+consequences are valid, where the rules for case guards are the same as
the rule for an expression in ``Precondition`` and the rules for
consequences are the same as the rule for an expression in
``Postcondition``. In particular, attributes ``'Old`` and
``'Result`` can only be used within consequence expressions.
-The condition for the last contract case may be ``others``, to denote
+The case guard for the last contract case may be ``others``, to denote
any case not captured by the previous cases. The
following is an example of use within a package spec:
@@ -1214,7 +1214,7 @@ following is an example of use within a package spec:
The meaning of contract cases is that only one case should apply at each
-call, as determined by the corresponding condition evaluating to True,
+call, as determined by the corresponding case guard evaluating to True,
and that the consequence for this case should hold when the subprogram
returns.
--- gcc/ada/gnat_rm.texi
+++ gcc/ada/gnat_rm.texi
@@ -21,7 +21,7 @@
@copying
@quotation
-GNAT Reference Manual , Apr 23, 2018
+GNAT Reference Manual , Apr 24, 2018
AdaCore
@@ -2556,9 +2556,9 @@ pragma Postcondition (if C1 then Pred1);
pragma Postcondition (if C2 then Pred2);
@end example
-The precondition ensures that one and only one of the conditions is
+The precondition ensures that one and only one of the case guards is
satisfied on entry to the subprogram.
-The postcondition ensures that for the condition that was True on entry,
+The postcondition ensures that for the case guard that was True on entry,
the corrresponding consequence is True on exit. Other consequence expressions
are not evaluated.
@@ -2572,13 +2572,13 @@ pragma Contract_Cases (P => Q);
The placement and visibility rules for @code{Contract_Cases} pragmas are
identical to those described for preconditions and postconditions.
-The compiler checks that boolean expressions given in conditions and
-consequences are valid, where the rules for conditions are the same as
+The compiler checks that boolean expressions given in case guards and
+consequences are valid, where the rules for case guards are the same as
the rule for an expression in @code{Precondition} and the rules for
consequences are the same as the rule for an expression in
@code{Postcondition}. In particular, attributes @code{'Old} and
@code{'Result} can only be used within consequence expressions.
-The condition for the last contract case may be @code{others}, to denote
+The case guard for the last contract case may be @code{others}, to denote
any case not captured by the previous cases. The
following is an example of use within a package spec:
@@ -2594,7 +2594,7 @@ end Math_Functions;
@end example
The meaning of contract cases is that only one case should apply at each
-call, as determined by the corresponding condition evaluating to True,
+call, as determined by the corresponding case guard evaluating to True,
and that the consequence for this case should hold when the subprogram
returns.
