NaNs (-check-nan)

The verification does not produce a check on the operation.

For instance, in the following code, there is no Invalid operation on floats check.

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}

The verification produces a check on the operation. The check determines if the result of the operation is NaN when the operands themselves are not NaN. For instance, the check flags the operation val1 + val2 only if the result can be NaN when both val1 and val2 are not NaN. The verification does not terminate the execution thread that produces NaN.

If the verification detects an operation that produces NaN as the only possible result on all execution paths and the operands themselves are never NaN, the check is red. If the operation can potentially result in NaN, the check is orange.

For instance, in the following code, there is a nonblocking Invalid operation on floats check for NaN.

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}

Even though the Invalid operation on floats check on the - operation is red, the verification continues. For instance, a green Non-initialized local variable check appears on y in the return statement.

The verification produces a check on the operation and terminates the execution thread that produces NaN.

If the check is red, the verification does not continue for the remaining code in the same scope as the check. If the check is orange, the verification continues but removes from consideration the variable values that produced a NaN.

For instance, in the following code, there is a blocking Invalid operation on floats check for NaN.

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}

The verification stops because the Invalid operation on floats check on the - operation is red. For instance, a Non-initialized local variable check does not appear on y in the return statement.

The Invalid operation on floats check for NaN also appears on the / operation and is green.