On Wed, Jan 24, 2024 at 6:13 PM Leonid Meyerovich <leo...@trustedst.com> wrote:
>
> My root task (root thread created by kernel) checks for fault from the
> other threads, which are created in root thread with badged fault_ep
>
> seL4_Word badge;
> seL4_MessageInfo_t messageInfo = seL4_NBRecv(init_objects.fault_cap,
> &badge);
> if (seL4_MessageInfo_get_label(messageInfo) != seL4_Fault_NullFault )
> {
> process_fault(messageInfo, badge);
> }
>
> Normally I don't have any faults, but every time I have
> seL4_MessageInfo_get_label(messageInfo) == 4, which is not in
> seL4_Fault_tag enumeration type
>
> enum seL4_Fault_tag {
> seL4_Fault_NullFault = 0,
> seL4_Fault_CapFault = 1,
> seL4_Fault_UnknownSyscall = 2,
> seL4_Fault_UserException = 3,
> seL4_Fault_VMFault = 5,
> seL4_Fault_VGICMaintenance = 6,
> seL4_Fault_VCPUFault = 7,
> seL4_Fault_VPPIEvent = 8
> };
>
> Could somebody explain?
I can't really explain it, but I wanted to note the DebugException
appears to typically have tag 4,
IIUC the above `enum seL4_Fault_tag` appears to be generated by the
following with non-mcs + arm hypervisor support,
https://github.com/seL4/seL4/blob/5df69647820f4517378f0e3d4af7347560f8c791/libsel4/arch_include/arm/sel4/arch/shared_types.bf#L16
I wouldn't think though it has `CONFIG_HARDWARE_DEBUG_API` configured
otherwise shouldn't `DebugExpetion` show up in that tag enum.
> Thanks,
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
