From 32c9c3defebd4304b82768b82f441875c68e8e9c Mon Sep 17 00:00:00 2001 From: Ivan Velickovic Date: Tue, 3 Sep 2024 20:10:42 +1000 Subject: [PATCH] Fix prints in error messages Signed-off-by: Ivan Velickovic --- libmicrokit/include/microkit.h | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 39cff2f1..3b16aded 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -149,7 +149,7 @@ static inline void microkit_vcpu_restart(microkit_child vcpu, seL4_Word entry_po ); if (err != seL4_NoError) { - microkit_dbg_puts("microkit_vm_restart: error writing registers\n"); + microkit_dbg_puts("microkit_vcpu_restart: error writing registers\n"); microkit_internal_crash(err); } } @@ -159,7 +159,7 @@ static inline void microkit_vcpu_stop(microkit_child vcpu) seL4_Error err; err = seL4_TCB_Suspend(BASE_VM_TCB_CAP + vcpu); if (err != seL4_NoError) { - microkit_dbg_puts("microkit_vm_stop: error suspending TCB\n"); + microkit_dbg_puts("microkit_vcpu_stop: error suspending TCB\n"); microkit_internal_crash(err); } } @@ -170,7 +170,7 @@ static inline void microkit_vcpu_arm_inject_irq(microkit_child vcpu, seL4_Uint16 seL4_Error err; err = seL4_ARM_VCPU_InjectIRQ(BASE_VCPU_CAP + vcpu, irq, priority, group, index); if (err != seL4_NoError) { - microkit_dbg_puts("microkit_arm_vcpu_inject_irq: error injecting IRQ\n"); + microkit_dbg_puts("microkit_vcpu_arm_inject_irq: error injecting IRQ\n"); microkit_internal_crash(err); } } @@ -180,7 +180,7 @@ static inline void microkit_vcpu_arm_ack_vppi(microkit_child vcpu, seL4_Word irq seL4_Error err; err = seL4_ARM_VCPU_AckVPPI(BASE_VCPU_CAP + vcpu, irq); if (err != seL4_NoError) { - microkit_dbg_puts("microkit_arm_vcpu_ack_vppi: error acking VPPI\n"); + microkit_dbg_puts("microkit_vcpu_arm_ack_vppi: error acking VPPI\n"); microkit_internal_crash(err); } } @@ -190,7 +190,7 @@ static inline seL4_Word microkit_vcpu_arm_read_reg(microkit_child vcpu, seL4_Wor seL4_ARM_VCPU_ReadRegs_t ret; ret = seL4_ARM_VCPU_ReadRegs(BASE_VCPU_CAP + vcpu, reg); if (ret.error != seL4_NoError) { - microkit_dbg_puts("microkit_arm_vcpu_read_reg: error reading vCPU register\n"); + microkit_dbg_puts("microkit_vcpu_arm_read_reg: error reading vCPU register\n"); microkit_internal_crash(ret.error); } @@ -202,7 +202,7 @@ static inline void microkit_vcpu_arm_write_reg(microkit_child vcpu, seL4_Word re seL4_Error err; err = seL4_ARM_VCPU_WriteRegs(BASE_VCPU_CAP + vcpu, reg, value); if (err != seL4_NoError) { - microkit_dbg_puts("microkit_arm_vcpu_write_reg: error writing vCPU register\n"); + microkit_dbg_puts("microkit_vcpu_arm_write_reg: error writing vCPU register\n"); microkit_internal_crash(err); } }