SECOND_UCNA_ADDR
printf("Injecting second UCNA at %#x.\n", SECOND_UCNA_ADDR);
inject_ucna(params->vcpu, SECOND_UCNA_ADDR);
TEST_ASSERT(*params->p_ucna_addr2 == SECOND_UCNA_ADDR,