/*
* Update current counter by 1 to indicate that the thread entered or left a
* blocking state caused by a poll(). If the counter's value is not an even
/*
* Update current counter by 1 to indicate that the thread entered or left a
* blocking state caused by a poll(). If the counter's value is not an even
*/
static inline void health_poll_entry(void)
{
/* Code MUST be in code execution state which is an even number. */
*/
static inline void health_poll_entry(void)
{
/* Code MUST be in code execution state which is an even number. */
* is raised.
*/
static inline void health_poll_exit(void)
{
/* Code MUST be in poll execution state which is an odd number. */
* is raised.
*/
static inline void health_poll_exit(void)
{
/* Code MUST be in poll execution state which is an odd number. */