Order of Code Prover Run-Time Checks

If multiple checks are performed on the same operation, Code Prover performs them in a specific order. The order of checks is important only if one of the checks is not green. If a check is red, the subsequent checks are not performed. If a check is orange, the subsequent checks are performed for a reduced set of values. For details, see Code Prover Analysis Following Red and Orange Checks.

A simple example is the order of checks on a pointer dereference. Code Prover first checks if the pointer is initialized and then checks if the pointer points to a valid location. The check Illegally dereferenced pointer follows the check Non-initialized local variable.

The order of checks can be nontrivial if one of the operands in a binary operation is a floating-point variable. Code Prover checks the operation in this order:

1. Invalid operation on floats: If you enable the option to consider non-finite floats, this check determines if the operation can result in NaN.

2. Overflow: This check determines if the result overflows.

   If you enable the option to consider non-finite floats, this check determines if the operation can result in infinities.

3. Subnormal float: If you enable the subnormal detection mode, this check determines if the operation can result in subnormal values.

For instance, suppose you enable options to forbid infinities, NaNs and subnormal results. In this example, the operation y = x + 0; is checked for all three issues. The operation appears red but consists of three checks: an orange Invalid operation on floats, an orange Overflow, and a red Subnormal float check.

#include <float.h>
#include <assert.h>

double input();

int main() {
  double x = input();
  double y;
  assert (x != x || x > DBL_MAX  || (x > 0. && x < DBL_MIN));
  y = x + 0.;
  return 0;
}

At the + operation, x can have three groups of values: x is NaN, x > DBL_MAX, and x > 0. && x < DBL_MIN.

The checks are performed in this order:

1. Invalid operation on floats: The check is orange because one execution path considers that x can be NaN.

   For the next checks, this path is not considered.

2. Overflow: The check is orange because one group of execution paths considers that x > DBL_MAX. For this group of paths, the + operation can result in infinity.

   For the next check, this group of paths is not considered.

3. Subnormal float: On the remaining group of execution paths, x > 0. && x < DBL_MIN. All values of x cause subnormal results. Therefore, this check is red.

The message on the Result Details pane reflects this reduction in paths. The message for the Subnormal float check states (when finite) to show that infinite values were removed from consideration.

The values for the left and right operands reflect all values before the operation, and not the reduced set of values. Therefore, the left operand still shows Inf and NaN even though these values were not considered for the check.

Related Topics

• Code Prover Analysis Following Red and Orange Checks