Lines Matching refs:badge
31 #include "../badge.h"
58 /*! @brief Checks whether a badge is an PID badge.
59 @param badge The badge to check.
60 @return true if the badge is an PID badge, false otherwise.
63 dispatcher_badge_PID(seL4_Word badge)
65 return (badge >= PID_BADGE_BASE && badge < PID_BADGE_END);
68 /*! @brief Checks whether a badge is a client liveliness badge.
69 @param badge The badge to check.
70 @return true if the badge is a liveliness badge, false otherwise.
73 dispatcher_badge_liveness(seL4_Word badge)
75 return (badge >= PID_LIVENESS_BADGE_BASE && badge < PID_LIVENESS_BADGE_END);
78 /*! @brief Checks whether a given badge is a ram dataspace.
79 @param badge The badge to check.
80 @return true if the given badge is a valid ram dataspace ID, false otherwise.
83 dispatcher_badge_dspace(seL4_Word badge)
85 return (badge >= RAM_DATASPACE_BADGE_BASE && badge < RAM_DATASPACE_BADGE_END);
88 /*! @brief Checks whether a given badge is a window.
89 @param badge The badge to check.
90 @return true if the given badge is a valid windowID, false otherwise.
93 dispatcher_badge_window(seL4_Word badge)
95 return (badge >= W_BADGE_BASE && badge < W_BADGE_END);