Introduce typedef for vCPU index.
Change-Id: I51194706edb86811487f2a22b3bda5405e605b5e
diff --git a/inc/hf/api.h b/inc/hf/api.h
index 7d6b7c0..4060075 100644
--- a/inc/hf/api.h
+++ b/inc/hf/api.h
@@ -27,7 +27,8 @@
spci_vm_count_t api_vm_get_count(void);
int64_t api_vcpu_get_count(spci_vm_id_t vm_id, const struct vcpu *current);
void api_regs_state_saved(struct vcpu *vcpu);
-struct hf_vcpu_run_return api_vcpu_run(spci_vm_id_t vm_id, uint32_t vcpu_idx,
+struct hf_vcpu_run_return api_vcpu_run(spci_vm_id_t vm_id,
+ spci_vcpu_index_t vcpu_idx,
const struct vcpu *current,
struct vcpu **next);
int64_t api_vm_configure(ipaddr_t send, ipaddr_t recv, struct vcpu *current,
@@ -47,7 +48,7 @@
int64_t api_interrupt_enable(uint32_t intid, bool enable, struct vcpu *current);
uint32_t api_interrupt_get(struct vcpu *current);
int64_t api_interrupt_inject(spci_vm_id_t target_vm_id,
- uint32_t target_vcpu_idx, uint32_t intid,
+ spci_vcpu_index_t target_vcpu_idx, uint32_t intid,
struct vcpu *current, struct vcpu **next);
int32_t api_spci_msg_send(uint32_t attributes, struct vcpu *current,