Lines Matching refs:badge
35 static inline void ntfn_set_active(notification_t *ntfnPtr, word_t badge)
38 notification_ptr_set_ntfnMsgIdentifier(ntfnPtr, badge);
76 void sendSignal(notification_t *ntfnPtr, word_t badge)
87 setRegister(tcb, badgeRegister, badge);
95 ntfn_set_active(ntfnPtr, badge);
101 setRegister(tcb, badgeRegister, badge);
116 ntfn_set_active(ntfnPtr, badge);
119 ntfn_set_active(ntfnPtr, badge);
143 setRegister(dest, badgeRegister, badge);
154 badge2 |= badge;
254 word_t badge;
257 badge = notification_ptr_get_ntfnMsgIdentifier(ntfnPtr);
258 setRegister(tcb, badgeRegister, badge);