The ignore marker is only used to ignore certain nodes in the TCB for the purposes of diagnostics. The marker itself has been renamed as well as the helper function to see if the marker is present. Both now indicate that the marker is specifically for diagnostics. PR Close #40071