From: Piotr Trojanek Date: Thu, 24 May 2018 13:04:44 +0000 (+0000) Subject: [Ada] Fix inconsistent documentation for the Contract_Cases pragma X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=883ccddf496f6a6d037e72b49fee66878a11b1a1;p=gcc.git [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 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 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 50c886d4e6f..219fa8bfe97 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2018-05-24 Piotr Trojanek + + * 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 * 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 73d7db89873..353a9a5f346 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 a0c75753f04..ac29d3f6af8 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.