FIRST_UCNA_ADDR
printf("Injecting first UCNA at %#x.\n", FIRST_UCNA_ADDR);
inject_ucna(params->vcpu, FIRST_UCNA_ADDR);
TEST_ASSERT(*params->p_i_ucna_addr == FIRST_UCNA_ADDR,
TEST_ASSERT(*params->p_ucna_addr == FIRST_UCNA_ADDR,