Validity Checking (GNAT User’s Guide for Native Platforms)

#### 4.3.6 Validity Checking ¶

The Ada Reference Manual defines the concept of invalid values (see RM 13.9.1). The primary source of invalid values is uninitialized variables. A scalar variable that is left uninitialized may contain an invalid value; the concept of invalid does not apply to access or composite types.

It is an error to read an invalid value, but the RM does not require run-time checks to detect such errors, except for some minimal checking to prevent erroneous execution (i.e. unpredictable behavior). This corresponds to the `-gnatVd` switch below, which is the default. For example, by default, if the expression of a case statement is invalid, it will raise Constraint_Error rather than causing a wild jump, and if an array index on the left-hand side of an assignment is invalid, it will raise Constraint_Error rather than overwriting an arbitrary memory location.

The `-gnatVa` may be used to enable additional validity checks, which are not required by the RM. These checks are often very expensive (which is why the RM does not require them). These checks are useful in tracking down uninitialized variables, but they are not usually recommended for production builds, and in particular we do not recommend using these extra validity checking options in combination with optimization, since this can confuse the optimizer. If performance is a consideration, leading to the need to optimize, then the validity checking options should not be used.

The other `-gnatV`x'` switches below allow finer-grained control; you can enable whichever validity checks you desire. However, for most debugging purposes, `-gnatVa` is sufficient, and the default `-gnatVd` (i.e. standard Ada behavior) is usually sufficient for non-debugging use.

The `-gnatB` switch tells the compiler to assume that all values are valid (that is, within their declared subtype range) except in the context of a use of the Valid attribute. This means the compiler can generate more efficient code, since the range of values is better known at compile time. However, an uninitialized variable can cause wild jumps and memory corruption in this mode.

The `-gnatV`x'` switch allows control over the validity checking mode as described below. The `x` argument is a string of letters that indicate validity checks that are performed or not performed in addition to the default checks required by Ada as described above.

`-gnatVa`

  ‘All validity checks.’

  All validity checks are turned on. That is, `-gnatVa` is equivalent to `gnatVcdefimoprst`.

`-gnatVc`

  ‘Validity checks for copies.’

  The right-hand side of assignments, and the (explicit) initializing values of object declarations are validity checked.

`-gnatVd`

  ‘Default (RM) validity checks.’

  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 `-gnatVD`. They are turned on by default. If `-gnatVD` is specified, a subsequent switch `-gnatVd` will leave the checks turned on. Switch `-gnatVD` should be used only if you are sure that all such expressions have valid values. If you use this switch and invalid values are present, then the program is erroneous, and wild jumps or memory overwriting may occur.

`-gnatVe`

  ‘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 (`-gnatVc`) are turned on. Specifying this switch enables such checks. This switch has no effect if the `-gnatVc` switch is not specified.

`-gnatVf`

  ‘Validity checks for floating-point values.’

  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 `-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. The exact contexts in which floating-point values are checked depends on the setting of other options. For example, `-gnatVif` or `-gnatVfi` (the order does not matter) specifies that floating-point parameters of mode `in` should be validity checked.

`-gnatVi`

  ‘Validity checks for ‘‘in‘‘ mode parameters.’

  Arguments for parameters of mode `in` are validity checked in function and procedure calls at the point of call.

`-gnatVm`

  ‘Validity checks for ‘‘in out‘‘ mode parameters.’

  Arguments for parameters of mode `in out` are validity checked in procedure calls at the point of call. The `'m'` here stands for modify, since this concerns parameters that can be modified by the call. Note that there is no specific option to test `out` parameters, but any reference within the subprogram will be tested in the usual manner, and if an invalid value is copied back, any reference to it will be subject to validity checking.

`-gnatVn`

  ‘No validity checks.’

  This switch turns off all validity checking, including the default checking for case statements and left hand side subscripts. Note that the use of the switch `-gnatp` suppresses all run-time checks, including validity checks, and thus implies `-gnatVn`. When this switch is used, it cancels any other `-gnatV` previously issued.

`-gnatVo`

  ‘Validity checks for operator and attribute operands.’

  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 on individual component values for composite comparisons, and on the expressions in type conversions and qualified expressions. Checks are also made on explicit ranges using `..` (e.g., slices, loops etc).

`-gnatVp`

  ‘Validity checks for parameters.’

  This controls the treatment of formal parameters within a subprogram (as opposed to `-gnatVi` and `-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 `-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.

`-gnatVr`

  ‘Validity checks for function returns.’

  The expression in simple `return` statements in functions is validity checked.

`-gnatVs`

  ‘Validity checks for subscripts.’

  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).

`-gnatVt`

  ‘Validity checks for tests.’

  Expressions used as conditions in `if`, `while` or `exit` statements are checked, as well as guard expressions in entry calls.

The `-gnatV` switch may be followed by a string of letters to turn on a series of validity checking options. For example, `-gnatVcr` specifies that in addition to the default validity checking, copies and function return expressions are to be validity checked. In order to make it easier to specify the desired combination of effects, the upper case letters `CDFIMORST` may be used to turn off the corresponding lower case option. Thus `-gnatVaM` turns on all validity checking options except for checking of `in out` parameters.

The specification of additional validity checking generates extra code (and in the case of `-gnatVa` the code expansion can be substantial). However, these additional checks can be very useful in detecting uninitialized variables, incorrect use of unchecked conversion, and other errors leading to invalid values. The use of pragma `Initialize_Scalars` is useful in conjunction with the extra validity checking, since this ensures that wherever possible uninitialized variables have invalid values.

See also the pragma `Validity_Checks` which allows modification of the validity checking mode at the program source level, and also allows for temporary disabling of validity checks.