Introduce typedef for vCPU index.
Change-Id: I51194706edb86811487f2a22b3bda5405e605b5e
diff --git a/inc/hf/cpu.h b/inc/hf/cpu.h
index d0a5466..d370830 100644
--- a/inc/hf/cpu.h
+++ b/inc/hf/cpu.h
@@ -132,7 +132,7 @@
void vcpu_unlock(struct vcpu_locked *locked);
void vcpu_init(struct vcpu *vcpu, struct vm *vm);
void vcpu_on(struct vcpu_locked vcpu, ipaddr_t entry, uintreg_t arg);
-size_t vcpu_index(const struct vcpu *vcpu);
+spci_vcpu_index_t vcpu_index(const struct vcpu *vcpu);
bool vcpu_is_off(struct vcpu_locked vcpu);
bool vcpu_secondary_reset_and_start(struct vcpu *vcpu, ipaddr_t entry,
uintreg_t arg);