Closed krypt-n closed 7 years ago
Hi krypt-n. Divergence is, indeed, the right behaviour: A method with a loop bounded by an input has an infinite number of feasible paths, and if you do not bound the symbolic execution JBSE will run indefinitely in an attempt to explore all of them. Probably you are expecting JBSE to stop at the first assertion violation, but this is not the default behaviour for JBSE. You can set exploration bounds for your example with the setDepthScope
and setCountScope
methods of the RunParameters
class. For instance, if you want to see all executions with a number of loop iterations between 0 and 79, you must setDepthScope(80)
.
Thank you, that's exactly the option I'm looking for.
If you don't mind another question:
class Test {
int[] array;
public void check() {
for (int a : array) {
ass3rt(a != 17);
}
}
}
I'd like to define the initial heap-shape such that states where array == null
or array.length != 4
are not considered, but the actual contents of array
are symbolic variables. I already tried assume
ing or ass3rt
ing these constrains, but there were still traces with different array sizes in the output. What would be the preferred way of doing that?
You should assume(array != null && array.length == 4)
at the beginning of check()
. With these assumptions symbolic execution explores 7 traces, of which 2 violate assumptions (one with path condition array == null
and one with path condition array != null && array.length != 4
), 4 violate the assertion (the first with path condition a[0] == 17
, the second a[0] != 17 && a[1] == 17
, and so on) and 1 is safe (with path condition a[0] != 17 && a[1] != 17 && a[2] != 17 && a[3] != 17
).
Thanks again.
JBSE seems to run indefinitely for this (relatively) simple method. An input of
x = 17
should should lead to a violated assertion.Is there a way to configure jbse to handle that method?