A TCB object has two objects inside it, the cnode object and the 'actual tcb object'. For simplicity of verification we would like the tcb_t portion of the object to also be size aligned instead of just just being offset by the size of the cnode.