[Ada] Improve documentation of validation checking control switches

[Ada] Improve documentation of validation checking control switches

[Marc Poulhiès]

[-- Attachment #1: Type: text/plain, Size: 390 bytes --]

Correct incorrect text and clarify unclear text that has been identified
in the "Validity Checking" section of the GNAT UG.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* doc/gnat_ugn/building_executable_programs_with_gnat.rst:
	Improve -gnatVa, -gnatVc, -gnatVd, -gnatVe, -gnatVf, -gnatVo,
	-gnatVp, -gnatVr, and -gnatVs switch descriptions.
	* gnat_ugn.texi: Regenerate.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 15020 bytes --]

diff --git a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
--- a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
+++ b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
@@ -4455,7 +4455,7 @@ to the default checks required by Ada as described above.
 
   All validity checks are turned on.
   That is, :switch:`-gnatVa` is
-  equivalent to ``gnatVcdfimoprst``.
+  equivalent to ``gnatVcdefimoprst``.
 
 
 .. index:: -gnatVc  (gcc)
@@ -4463,8 +4463,8 @@ to the default checks required by Ada as described above.
 :switch:`-gnatVc`
   *Validity checks for copies.*
 
-  The right hand side of assignments, and the initializing values of
-  object declarations are validity checked.
+  The right-hand side of assignments, and the (explicit) initializing values
+  of object declarations are validity checked.
 
 
 .. index:: -gnatVd  (gcc)
@@ -4472,12 +4472,14 @@ to the default checks required by Ada as described above.
 :switch:`-gnatVd`
   *Default (RM) validity checks.*
 
-  Some validity checks are done by default following normal Ada semantics
-  (RM 13.9.1 (9-11)).
-  A check is done in case statements that the expression is within the range
-  of the subtype. If it is not, Constraint_Error is raised.
-  For assignments to array components, a check is done that the expression used
-  as index is within the range. If it is not, Constraint_Error is raised.
+  Some validity checks are required by Ada (see RM 13.9.1 (9-11)); these
+  (and only these) validity checks are enabled by default.
+  For case statements (and case expressions) that lack a "when others =>"
+  choice, a check is made that the value of the selector expression
+  belongs to its nominal subtype. If it does not, Constraint_Error is raised.
+  For assignments to array components (and for indexed components in some
+  other contexts), a check is made that each index expression belongs to the
+  corresponding index subtype. If it does not, Constraint_Error is raised.
   Both these validity checks may be turned off using switch :switch:`-gnatVD`.
   They are turned on by default. If :switch:`-gnatVD` is specified, a subsequent
   switch :switch:`-gnatVd` will leave the checks turned on.
@@ -4490,28 +4492,31 @@ to the default checks required by Ada as described above.
 .. index:: -gnatVe  (gcc)
 
 :switch:`-gnatVe`
-  *Validity checks for elementary components.*
-
-  In the absence of this switch, assignments to record or array components are
-  not validity checked, even if validity checks for assignments generally
-  (:switch:`-gnatVc`) are turned on. In Ada, assignment of composite values do not
-  require valid data, but assignment of individual components does. So for
-  example, there is a difference between copying the elements of an array with a
-  slice assignment, compared to assigning element by element in a loop. This
-  switch allows you to turn off validity checking for components, even when they
-  are assigned component by component.
+  *Validity checks for scalar components.*
 
+  In the absence of this switch, assignments to scalar components of
+  enclosing record or array objects are not validity checked, even if
+  validity checks for assignments generally (:switch:`-gnatVc`) are turned on.
+  Specifying this switch enables such checks.
+  This switch has no effect if the :switch:`-gnatVc` switch is not specified.
 
 .. index:: -gnatVf  (gcc)
 
 :switch:`-gnatVf`
   *Validity checks for floating-point values.*
 
-  In the absence of this switch, validity checking occurs only for discrete
-  values. If :switch:`-gnatVf` is specified, then validity checking also applies
+  Specifying this switch enables validity checking for floating-point
+  values in the same contexts where validity checking is enabled for
+  other scalar values.
+  In the absence of this switch, validity checking is not performed for
+  floating-point values. This takes precedence over other statements about
+  performing validity checking for scalar objects in various scenarios.
+  One way to look at it is that if this switch is not set, then whenever
+  any of the other rules in this section use the word "scalar" they
+  really mean "scalar and not floating-point".
+  If :switch:`-gnatVf` is specified, then validity checking also applies
   for floating-point values, and NaNs and infinities are considered invalid,
-  as well as out of range values for constrained types. Note that this means
-  that standard IEEE infinity mode is not allowed. The exact contexts
+  as well as out-of-range values for constrained types. The exact contexts
   in which floating-point values are checked depends on the setting of other
   options. For example, :switch:`-gnatVif` or :switch:`-gnatVfi`
   (the order does not matter) specifies that floating-point parameters of mode
@@ -4558,7 +4563,8 @@ to the default checks required by Ada as described above.
 :switch:`-gnatVo`
   *Validity checks for operator and attribute operands.*
 
-  Arguments for predefined operators and attributes are validity checked.
+  Scalar arguments for predefined operators and for attributes are
+  validity checked.
   This includes all operators in package ``Standard``,
   the shift operators defined as intrinsic in package ``Interfaces``
   and operands for attributes such as ``Pos``. Checks are also made
@@ -4572,22 +4578,22 @@ to the default checks required by Ada as described above.
 :switch:`-gnatVp`
   *Validity checks for parameters.*
 
-  This controls the treatment of parameters within a subprogram (as opposed
-  to :switch:`-gnatVi` and :switch:`-gnatVm` which control validity testing
-  of parameters on a call. If either of these call options is used, then
-  normally an assumption is made within a subprogram that the input arguments
-  have been validity checking at the point of call, and do not need checking
-  again within a subprogram). If :switch:`-gnatVp` is set, then this assumption
-  is not made, and parameters are not assumed to be valid, so their validity
-  will be checked (or rechecked) within the subprogram.
-
+  This controls the treatment of formal parameters within a subprogram (as
+  opposed to :switch:`-gnatVi` and :switch:`-gnatVm`, which control validity
+  testing of actual parameters of a call). If either of these call options is
+  specified, then normally an assumption is made within a subprogram that
+  the validity of any incoming formal parameters of the corresponding mode(s)
+  has already been checked at the point of call and does not need rechecking.
+  If :switch:`-gnatVp` is set, then this assumption is not made and so their
+  validity may be checked (or rechecked) within the subprogram. If neither of
+  the two call-related options is specified, then this switch has no effect.
 
 .. index:: -gnatVr  (gcc)
 
 :switch:`-gnatVr`
   *Validity checks for function returns.*
 
-  The expression in ``return`` statements in functions is validity
+  The expression in simple ``return`` statements in functions is validity
   checked.
 
 
@@ -4596,9 +4602,10 @@ to the default checks required by Ada as described above.
 :switch:`-gnatVs`
   *Validity checks for subscripts.*
 
-  All subscripts expressions are checked for validity, whether they appear
-  on the right side or left side (in default mode only left side subscripts
-  are validity checked).
+  All subscript expressions are checked for validity, whatever context
+  they occur in (in default mode some subscripts are not validity checked;
+  for example, validity checking may be omitted in some cases involving
+  a read of a component of an array).
 
 
 .. index:: -gnatVt  (gcc)


diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -12984,7 +12984,7 @@ to the default checks required by Ada as described above.
 
 All validity checks are turned on.
 That is, @code{-gnatVa} is
-equivalent to @code{gnatVcdfimoprst}.
+equivalent to @code{gnatVcdefimoprst}.
 @end table
 
 @geindex -gnatVc (gcc)
@@ -12996,8 +12996,8 @@ equivalent to @code{gnatVcdfimoprst}.
 
 `Validity checks for copies.'
 
-The right hand side of assignments, and the initializing values of
-object declarations are validity checked.
+The right-hand side of assignments, and the (explicit) initializing values
+of object declarations are validity checked.
 @end table
 
 @geindex -gnatVd (gcc)
@@ -13009,12 +13009,14 @@ object declarations are validity checked.
 
 `Default (RM) validity checks.'
 
-Some validity checks are done by default following normal Ada semantics
-(RM 13.9.1 (9-11)).
-A check is done in case statements that the expression is within the range
-of the subtype. If it is not, Constraint_Error is raised.
-For assignments to array components, a check is done that the expression used
-as index is within the range. If it is not, Constraint_Error is raised.
+Some validity checks are required by Ada (see RM 13.9.1 (9-11)); these
+(and only these) validity checks are enabled by default.
+For case statements (and case expressions) that lack a “when others =>”
+choice, a check is made that the value of the selector expression
+belongs to its nominal subtype. If it does not, Constraint_Error is raised.
+For assignments to array components (and for indexed components in some
+other contexts), a check is made that each index expression belongs to the
+corresponding index subtype. If it does not, Constraint_Error is raised.
 Both these validity checks may be turned off using switch @code{-gnatVD}.
 They are turned on by default. If @code{-gnatVD} is specified, a subsequent
 switch @code{-gnatVd} will leave the checks turned on.
@@ -13031,16 +13033,13 @@ overwriting may occur.
 
 @item @code{-gnatVe}
 
-`Validity checks for elementary components.'
+`Validity checks for scalar components.'
 
-In the absence of this switch, assignments to record or array components are
-not validity checked, even if validity checks for assignments generally
-(@code{-gnatVc}) are turned on. In Ada, assignment of composite values do not
-require valid data, but assignment of individual components does. So for
-example, there is a difference between copying the elements of an array with a
-slice assignment, compared to assigning element by element in a loop. This
-switch allows you to turn off validity checking for components, even when they
-are assigned component by component.
+In the absence of this switch, assignments to scalar components of
+enclosing record or array objects are not validity checked, even if
+validity checks for assignments generally (@code{-gnatVc}) are turned on.
+Specifying this switch enables such checks.
+This switch has no effect if the @code{-gnatVc} switch is not specified.
 @end table
 
 @geindex -gnatVf (gcc)
@@ -13052,11 +13051,18 @@ are assigned component by component.
 
 `Validity checks for floating-point values.'
 
-In the absence of this switch, validity checking occurs only for discrete
-values. If @code{-gnatVf} is specified, then validity checking also applies
+Specifying this switch enables validity checking for floating-point
+values in the same contexts where validity checking is enabled for
+other scalar values.
+In the absence of this switch, validity checking is not performed for
+floating-point values. This takes precedence over other statements about
+performing validity checking for scalar objects in various scenarios.
+One way to look at it is that if this switch is not set, then whenever
+any of the other rules in this section use the word “scalar” they
+really mean “scalar and not floating-point”.
+If @code{-gnatVf} is specified, then validity checking also applies
 for floating-point values, and NaNs and infinities are considered invalid,
-as well as out of range values for constrained types. Note that this means
-that standard IEEE infinity mode is not allowed. The exact contexts
+as well as out-of-range values for constrained types. The exact contexts
 in which floating-point values are checked depends on the setting of other
 options. For example, @code{-gnatVif} or @code{-gnatVfi}
 (the order does not matter) specifies that floating-point parameters of mode
@@ -13119,7 +13125,8 @@ is used, it cancels any other @code{-gnatV} previously issued.
 
 `Validity checks for operator and attribute operands.'
 
-Arguments for predefined operators and attributes are validity checked.
+Scalar arguments for predefined operators and for attributes are
+validity checked.
 This includes all operators in package @code{Standard},
 the shift operators defined as intrinsic in package @code{Interfaces}
 and operands for attributes such as @code{Pos}. Checks are also made
@@ -13137,14 +13144,15 @@ also made on explicit ranges using @code{..} (e.g., slices, loops etc).
 
 `Validity checks for parameters.'
 
-This controls the treatment of parameters within a subprogram (as opposed
-to @code{-gnatVi} and @code{-gnatVm} which control validity testing
-of parameters on a call. If either of these call options is used, then
-normally an assumption is made within a subprogram that the input arguments
-have been validity checking at the point of call, and do not need checking
-again within a subprogram). If @code{-gnatVp} is set, then this assumption
-is not made, and parameters are not assumed to be valid, so their validity
-will be checked (or rechecked) within the subprogram.
+This controls the treatment of formal parameters within a subprogram (as
+opposed to @code{-gnatVi} and @code{-gnatVm}, which control validity
+testing of actual parameters of a call). If either of these call options is
+specified, then normally an assumption is made within a subprogram that
+the validity of any incoming formal parameters of the corresponding mode(s)
+has already been checked at the point of call and does not need rechecking.
+If @code{-gnatVp} is set, then this assumption is not made and so their
+validity may be checked (or rechecked) within the subprogram. If neither of
+the two call-related options is specified, then this switch has no effect.
 @end table
 
 @geindex -gnatVr (gcc)
@@ -13156,7 +13164,7 @@ will be checked (or rechecked) within the subprogram.
 
 `Validity checks for function returns.'
 
-The expression in @code{return} statements in functions is validity
+The expression in simple @code{return} statements in functions is validity
 checked.
 @end table
 
@@ -13169,9 +13177,10 @@ checked.
 
 `Validity checks for subscripts.'
 
-All subscripts expressions are checked for validity, whether they appear
-on the right side or left side (in default mode only left side subscripts
-are validity checked).
+All subscript expressions are checked for validity, whatever context
+they occur in (in default mode some subscripts are not validity checked;
+for example, validity checking may be omitted in some cases involving
+a read of a component of an array).
 @end table
 
 @geindex -gnatVt (gcc)