partially annotated, fixed dereferencing of userland pointer (trivial,
since we'd just copied the entire structure).