diff options
author | Piotr Trojanek <trojanek@adacore.com> | 2018-05-24 13:04:44 +0000 |
---|---|---|
committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-05-24 13:04:44 +0000 |
commit | 883ccddf496f6a6d037e72b49fee66878a11b1a1 (patch) | |
tree | db3d77a34497576092ad6e17d91374789d391539 /gcc/ada | |
parent | ebea257ee1195ce196ed005a7ee3a4b9e84117fb (diff) | |
download | gcc-883ccddf496f6a6d037e72b49fee66878a11b1a1.zip gcc-883ccddf496f6a6d037e72b49fee66878a11b1a1.tar.gz gcc-883ccddf496f6a6d037e72b49fee66878a11b1a1.tar.bz2 |
[Ada] Fix inconsistent documentation for the Contract_Cases pragma
This patch propagates the renaming from "condition" to "case guard" in the
contract grammar to the paragraphs that describe the pragma semantics.
2018-05-24 Piotr Trojanek <trojanek@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.
From-SVN: r260647
Diffstat (limited to 'gcc/ada')
-rw-r--r-- | gcc/ada/ChangeLog | 7 | ||||
-rw-r--r-- | gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst | 12 | ||||
-rw-r--r-- | gcc/ada/gnat_rm.texi | 14 |
3 files changed, 20 insertions, 13 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 50c886d..219fa8b 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2018-05-24 Piotr Trojanek <trojanek@adacore.com> + + * doc/gnat_rm/implementation_defined_pragmas.rst (Contract_Cases): + Change "condition" to "case guard" after renaming in the contract + grammar. + * gnat_rm.texi: Regenerate. + 2018-05-24 Hristian Kirtchev <kirtchev@adacore.com> * exp_util.adb (Expand_Static_Predicates_In_Choices): Indicate that the diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst index 73d7db8..353a9a5 100644 --- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst +++ b/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. diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index a0c7575..ac29d3f 100644 --- a/gcc/ada/gnat_rm.texi +++ b/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. |