unwind

Set an upper bound for the number of times Diffblue Cover will iterate through loops in the code.

Description

Test generation is based on analysis that relies on unwinding loops in the code. The unwind parameter sets an upper bound to the number of unwindings we perform.

Usage

If the maximum unwind is set to 5, then no test can be created for the following method:

public static int func() {
  int sum = 0;
  for (int i = 0; i < 5; i++) {
    sum++;
  }
  return sum;
}

We cannot produce a test here because one unwinding is performed to enter the loop, and five unwindings are needed inside it. You would need to set unwind to at least six.

Note that this also applies to loops that are hidden in the Java Library implementation such as in ArrayList.contains().

The complexity of the computation scales exponentially with the unwind parameter. Try to avoid setting this parameter too high, otherwise your analysis may not be successful.

phases:
-
  cbmcArguments:
    unwind: 6

Defaults

Phase Default
1 2
2 4
3 16

results matching ""

    No results matching ""