253c253,256
< uint32_t getMPIDR(ArmSystem *arm_sys, ThreadContext *tc);
---
> /** This helper function is either returing the value of
> * MPIDR_EL1 (by calling getMPIDR), or it is issuing a read
> * to VMPIDR_EL2 (as it happens in virtualized systems) */
> MiscReg readMPIDR(ArmSystem *arm_sys, ThreadContext *tc);
254a258,260
> /** This helper function is returing the value of MPIDR_EL1 */
> MiscReg getMPIDR(ArmSystem *arm_sys, ThreadContext *tc);
>