Closed jstolarek closed 7 years ago
This seems to be fixed, but we get another error in the test suite. A minimal example is:
let y = ref 0 in
let t = trace (
(y := 42);; !y) in
bwdSlice (t, 42)
which yields an exception due to attempting to take the LUB of 0 and 42. However, for some reason
let t = trace (
let y = ref 0 in
(y := 42);; !y) in
bwdSlice (t, 42)
works and does the right thing. So it may be that the problem is not in the slicing code but somewhere else.
Ah, I see. In Eval, we are recording the initial store in VTrace, then we are using it as the final store in bwdSlice. That's wrong - we should record the final store, and use it (if at all) to check that any reference-based slicing criteria respect the original result values. The initial store for backward slicing should be empty (unless we add an operator that allows us to give a reference label and part of its value as an initial slicing criterion).
Right, that's how I understood the rules. Sorry about that.
@jamescheney reports:
If I do:
then the slice I get leaves out one of the components: