VCPU_NAME_BUFLEN
char namebuf[VCPU_NAME_BUFLEN];
(void) snprintf(namebuf, VCPU_NAME_BUFLEN, "vcpu%u", i);