A pointer dereferenceable before a gc.relocate should be dereferenceable
after a gc.relocate, because the gc might not kick in, making the
gc.relocate a noop in some cases (and hence the invariant should hold in
all cases).
Details
Details
Diff Detail
Diff Detail
Event Timeline
Comment Actions
While your reasoning in the opening comment is faulty, the actual code LGTM.
You can't reason only about what happens when GC doesn't trigger to infer a property of the potentially relocated value. You need to reason about what happens in both cases: relocation and non-relocation.
Side note (mostly for my own later reference): I could see a theoretically GC like thing which changed dereferenceability on collection, but no practical collector I know of does so. As such, I don't see a point in controlling this via a flag at this time.