Potentially dead code in obj_ut_print_attrs?

[kent-mcleod]

It appears that the linked block of debug code doesn't do anything because the enabling condition of the for-loop implies that the inner if condition is always false I think. Is anyone else able to confirm or provide a counter example? https://github.com/seL4/seL4/blob/0792eebc0abfc4d1c6f9e9ec1d2ac5b85fd27185/src/machine/capdl.c#L142-L157

[Indanz]

Agreed. Second check in isMDBParentOf() is:

    if (!sameRegionAs(cte_a->cap, cte_b->cap)) {
        return false;
    }

I think the intention was if (sameRegionAs(slot->cap, nextPtr->cap)), which is superfluous. But fixing that would change the output and everyone using is used to the current code, so what to do?

[kent-mcleod]

But I think that the print statement is unreachable currently?

[Indanz]

Indeed, that's what I meant with "agreed".

[kent-mcleod]

Oh I think I misinterpreted your next point about changing it changing output.

[Indanz]

If we fix the code so it does what's intended, it will also print out info about all objects allocated from the UT. Which can be very useful, but it's probably not what anyone currently expects. But will it cause "Oh, that's nice" or "Oh, that's confusing".

Currently all caps of a TCB's CNode are printed by SysDebugSnapshot. If the TCB has caps to the UT derived objects, it will print out info twice if we fix this and remove the if-check.

As a separate issue, why wouldn't the debug prints be allowed on the root task? That is, why not just check for the idle task and removing root_or_idle_tcb()?