Side effects outside early return paths, needs to void on the return paths.

[sohah]

We have a problem in populating the side effects for fields, and I am assuming the same will happen for the arrays, when an early return happens on one path. In particular, running the following code with JR mode 3, raises an assert exception, while on plain SPF no assertions are violated.

class Something{

int sideEffect = 0;
private int testERInline(boolean a, int x) {
        int z = 0;
        if (a) z = testingER1(a, x);
        assert !(a && x > 2) || this.sideEffect == 0;
        return z;
    }

    private int testingER1(boolean a, int x) {
        int z = 1;
        if (x > 2) {
            z = x + 1;
            return z;
        }
        z++;
        this.sideEffect = 5;

        return z;
    }
}

The problem is with the sideEffect field update in testingER1 method. There the side effect should be guarded by the fact that the early return did not happen. Since the field transformation happens after the early return removal, it does not account for the fact that the side effect should be void in case of early returns happening.

I ran the above code with jpf configuration

veritestingMode=3
symbolic.dp=z3bitvectorinc
listener =.symbc.VeritestingListener,gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener

or with the following listener

listener =.symbc.SymbolicListener,gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener