| 31 | #define taskEXIT_CRITICAL() clearInterruptMask( pxQueue ) |
| 32 | |
| 33 | static BaseType_t prvIsQueueEmpty( const Queue_t * pxQueue ) |
| 34 | /*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/ |
| 35 | /*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr);@*/ |
| 36 | { |
| 37 | BaseType_t xReturn; |
| 38 | |
| 39 | taskENTER_CRITICAL(); |
| 40 | /*@assert queue(pxQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ |
| 41 | { |
| 42 | if( pxQueue->uxMessagesWaiting == ( UBaseType_t ) 0 ) |
| 43 | { |
| 44 | xReturn = pdTRUE; |
| 45 | } |
| 46 | else |
| 47 | { |
| 48 | xReturn = pdFALSE; |
| 49 | } |
| 50 | } |
| 51 | /*@close queue(pxQueue, Storage, N, M, W, R, K, is_locked, abs);@*/ |
| 52 | taskEXIT_CRITICAL(); |
| 53 | |
| 54 | return xReturn; |
| 55 | } |
| 56 | |
| 57 | /* *INDENT-ON* */ |
no outgoing calls
no test coverage detected