Marking local functions: vPortSetBASEPRI ulPortRaiseBASEPRI vPortRaiseBASEPRI


Marking externally visible functions: vQueueWaitForMessageRestricted vQueueUnregisterQueue pcQueueGetName vQueueAddToRegistry xQueueIsQueueFullFromISR xQueueIsQueueEmptyFromISR ucQueueGetQueueType vQueueSetQueueNumber uxQueueGetQueueNumber vQueueDelete uxQueueMessagesWaitingFromISR uxQueueSpacesAvailable uxQueueMessagesWaiting xQueuePeekFromISR xQueueReceiveFromISR xQueuePeek xQueueSemaphoreTake xQueueReceive xQueueGiveFromISR xQueueGenericSendFromISR xQueueGenericSend xQueueCreateCountingSemaphore xQueueTakeMutexRecursive xQueueGiveMutexRecursive xQueueGetMutexHolderFromISR xQueueGetMutexHolder xQueueCreateMutex xQueueGenericCreate xQueueGenericReset


Marking externally visible variables: xQueueRegistry


Reclaiming functions:
Reclaiming variables:
Clearing address taken flags:
Symbol table:

vTaskPlaceOnEventListRestricted/62 (vTaskPlaceOnEventListRestricted) @060be700
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: vQueueWaitForMessageRestricted/41 
  Calls: 
vTaskMissedYield/61 (vTaskMissedYield) @060a6ee0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: prvUnlockQueue/33 prvUnlockQueue/33 
  Calls: 
memcpy/60 (memcpy) @060a6c40
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: prvCopyDataFromQueue/32 prvCopyDataToQueue/31 prvCopyDataToQueue/31 
  Calls: 
xTaskPriorityDisinherit/59 (xTaskPriorityDisinherit) @060a6b60
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: prvCopyDataToQueue/31 
  Calls: 
vPortFree/58 (vPortFree) @060a6540
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: vQueueDelete/26 
  Calls: 
vTaskPriorityDisinheritAfterTimeout/57 (vTaskPriorityDisinheritAfterTimeout) @0606dd20
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueueSemaphoreTake/19 
  Calls: 
xTaskPriorityInherit/56 (xTaskPriorityInherit) @0606dc40
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueueSemaphoreTake/19 
  Calls: 
pvTaskIncrementMutexHeldCount/55 (pvTaskIncrementMutexHeldCount) @0606db60
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueueSemaphoreTake/19 
  Calls: 
vPortValidateInterruptPriority/54 (vPortValidateInterruptPriority) @0606d0e0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueuePeekFromISR/22 xQueueReceiveFromISR/21 xQueueGiveFromISR/17 xQueueGenericSendFromISR/16 
  Calls: 
xTaskResumeAll/53 (xTaskResumeAll) @06013ee0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueuePeek/20 xQueuePeek/20 xQueuePeek/20 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueReceive/18 xQueueReceive/18 xQueueGenericSend/15 xQueueGenericSend/15 xQueueGenericSend/15 
  Calls: 
vTaskPlaceOnEventList/52 (vTaskPlaceOnEventList) @06013e00
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueuePeek/20 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueGenericSend/15 
  Calls: 
xTaskCheckForTimeOut/51 (xTaskCheckForTimeOut) @06013d20
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueuePeek/20 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueGenericSend/15 
  Calls: 
vTaskSuspendAll/50 (vTaskSuspendAll) @06013c40
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueuePeek/20 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueGenericSend/15 
  Calls: 
vTaskInternalSetTimeOutState/49 (vTaskInternalSetTimeOutState) @06013b60
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueuePeek/20 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueGenericSend/15 
  Calls: 
xTaskGetSchedulerState/48 (xTaskGetSchedulerState) @06013a80
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueuePeek/20 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueGenericSend/15 
  Calls: 
xTaskGetCurrentTaskHandle/47 (xTaskGetCurrentTaskHandle) @06013540
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueueTakeMutexRecursive/13 xQueueGiveMutexRecursive/12 
  Calls: 
pvPortMalloc/46 (pvPortMalloc) @06009460
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueueGenericCreate/6 
  Calls: 
vPortExitCritical/45 (vPortExitCritical) @06009e00
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: vQueueWaitForMessageRestricted/41 prvIsQueueFull/36 prvIsQueueEmpty/34 prvUnlockQueue/33 prvUnlockQueue/33 uxQueueSpacesAvailable/24 uxQueueMessagesWaiting/23 xQueuePeek/20 xQueuePeek/20 xQueuePeek/20 xQueuePeek/20 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueReceive/18 xQueueReceive/18 xQueueReceive/18 xQueueGenericSend/15 xQueueGenericSend/15 xQueueGenericSend/15 xQueueGenericSend/15 xQueueGetMutexHolder/10 xQueueGenericReset/5 
  Calls: 
vListInitialise/44 (vListInitialise) @06009d20
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: xQueueGenericReset/5 xQueueGenericReset/5 
  Calls: 
xTaskRemoveFromEventList/43 (xTaskRemoveFromEventList) @06009c40
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: prvUnlockQueue/33 prvUnlockQueue/33 xQueueReceiveFromISR/21 xQueuePeek/20 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueGiveFromISR/17 xQueueGenericSendFromISR/16 xQueueGenericSend/15 xQueueGenericReset/5 
  Calls: 
vPortEnterCritical/42 (vPortEnterCritical) @06009b60
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags:
  Called by: vQueueWaitForMessageRestricted/41 prvIsQueueFull/36 prvIsQueueEmpty/34 prvUnlockQueue/33 prvUnlockQueue/33 uxQueueSpacesAvailable/24 uxQueueMessagesWaiting/23 xQueuePeek/20 xQueuePeek/20 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueReceive/18 xQueueGenericSend/15 xQueueGenericSend/15 xQueueGetMutexHolder/10 xQueueGenericReset/5 
  Calls: 
vQueueWaitForMessageRestricted/41 (vQueueWaitForMessageRestricted) @06009620
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: prvUnlockQueue/33 vTaskPlaceOnEventListRestricted/62 vPortExitCritical/45 vPortEnterCritical/42 
vQueueUnregisterQueue/40 (vQueueUnregisterQueue) @06009380
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: xQueueRegistry/4 (read)xQueueRegistry/4 (write)xQueueRegistry/4 (write)
  Referring: 
  Availability: available
  Function flags: body
  Called by: vQueueDelete/26 
  Calls: vPortRaiseBASEPRI/1 
pcQueueGetName/39 (pcQueueGetName) @06009000
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: xQueueRegistry/4 (read)xQueueRegistry/4 (read)
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortRaiseBASEPRI/1 
vQueueAddToRegistry/38 (vQueueAddToRegistry) @060018c0
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: xQueueRegistry/4 (read)xQueueRegistry/4 (addr)xQueueRegistry/4 (read)xQueueRegistry/4 (addr)
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortRaiseBASEPRI/1 
xQueueIsQueueFullFromISR/37 (xQueueIsQueueFullFromISR) @06001e00
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortRaiseBASEPRI/1 
prvIsQueueFull/36 (prvIsQueueFull) @06001a80
  Type: function definition analyzed
  Visibility: force_output no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: xQueueGenericSend/15 
  Calls: vPortExitCritical/45 vPortEnterCritical/42 
xQueueIsQueueEmptyFromISR/35 (xQueueIsQueueEmptyFromISR) @060017e0
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortRaiseBASEPRI/1 
prvIsQueueEmpty/34 (prvIsQueueEmpty) @06001460
  Type: function definition analyzed
  Visibility: force_output no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: xQueuePeek/20 xQueuePeek/20 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueReceive/18 
  Calls: vPortExitCritical/45 vPortEnterCritical/42 
prvUnlockQueue/33 (prvUnlockQueue) @060011c0
  Type: function definition analyzed
  Visibility: force_output no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: vQueueWaitForMessageRestricted/41 xQueuePeek/20 xQueuePeek/20 xQueuePeek/20 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueReceive/18 xQueueReceive/18 xQueueGenericSend/15 xQueueGenericSend/15 xQueueGenericSend/15 
  Calls: vPortExitCritical/45 vTaskMissedYield/61 xTaskRemoveFromEventList/43 vPortEnterCritical/42 vPortExitCritical/45 vTaskMissedYield/61 xTaskRemoveFromEventList/43 vPortEnterCritical/42 
prvCopyDataFromQueue/32 (prvCopyDataFromQueue) @05ffb9a0
  Type: function definition analyzed
  Visibility: force_output no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: xQueuePeekFromISR/22 xQueueReceiveFromISR/21 xQueuePeek/20 xQueueReceive/18 
  Calls: memcpy/60 
prvCopyDataToQueue/31 (prvCopyDataToQueue) @05ffb460
  Type: function definition analyzed
  Visibility: force_output no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: xQueueGenericSendFromISR/16 xQueueGenericSend/15 
  Calls: memcpy/60 memcpy/60 xTaskPriorityDisinherit/59 
prvGetDisinheritPriorityAfterTimeout/30 (prvGetDisinheritPriorityAfterTimeout) @05ffbee0
  Type: function definition analyzed
  Visibility: force_output no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: xQueueSemaphoreTake/19 
  Calls: 
ucQueueGetQueueType/29 (ucQueueGetQueueType) @05ffbb60
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: 
vQueueSetQueueNumber/28 (vQueueSetQueueNumber) @05ffb8c0
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: 
uxQueueGetQueueNumber/27 (uxQueueGetQueueNumber) @05ffb620
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: 
vQueueDelete/26 (vQueueDelete) @05ffb380
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortFree/58 vQueueUnregisterQueue/40 vPortRaiseBASEPRI/1 
uxQueueMessagesWaitingFromISR/25 (uxQueueMessagesWaitingFromISR) @05ffb000
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortRaiseBASEPRI/1 
uxQueueSpacesAvailable/24 (uxQueueSpacesAvailable) @05ff2620
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortExitCritical/45 vPortEnterCritical/42 vPortRaiseBASEPRI/1 
uxQueueMessagesWaiting/23 (uxQueueMessagesWaiting) @05ff2d20
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortExitCritical/45 vPortEnterCritical/42 vPortRaiseBASEPRI/1 
xQueuePeekFromISR/22 (xQueuePeekFromISR) @05ff29a0
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortSetBASEPRI/3 prvCopyDataFromQueue/32 ulPortRaiseBASEPRI/2 vPortValidateInterruptPriority/54 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xQueueReceiveFromISR/21 (xQueueReceiveFromISR) @05ff2540
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortSetBASEPRI/3 vPortRaiseBASEPRI/1 xTaskRemoveFromEventList/43 prvCopyDataFromQueue/32 ulPortRaiseBASEPRI/2 vPortValidateInterruptPriority/54 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xQueuePeek/20 (xQueuePeek) @05ff20e0
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: prvIsQueueEmpty/34 xTaskResumeAll/53 prvUnlockQueue/33 xTaskResumeAll/53 prvUnlockQueue/33 xTaskResumeAll/53 prvUnlockQueue/33 vTaskPlaceOnEventList/52 prvIsQueueEmpty/34 xTaskCheckForTimeOut/51 vPortExitCritical/45 vPortEnterCritical/42 vTaskSuspendAll/50 vPortExitCritical/45 vTaskInternalSetTimeOutState/49 vPortExitCritical/45 vPortExitCritical/45 xTaskRemoveFromEventList/43 prvCopyDataFromQueue/32 vPortEnterCritical/42 vPortRaiseBASEPRI/1 xTaskGetSchedulerState/48 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xQueueSemaphoreTake/19 (xQueueSemaphoreTake) @05fe4d20
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: xQueueTakeMutexRecursive/13 
  Calls: vPortExitCritical/45 vTaskPriorityDisinheritAfterTimeout/57 prvGetDisinheritPriorityAfterTimeout/30 vPortEnterCritical/42 prvIsQueueEmpty/34 xTaskResumeAll/53 prvUnlockQueue/33 xTaskResumeAll/53 prvUnlockQueue/33 xTaskResumeAll/53 prvUnlockQueue/33 vTaskPlaceOnEventList/52 vPortExitCritical/45 xTaskPriorityInherit/56 vPortEnterCritical/42 prvIsQueueEmpty/34 xTaskCheckForTimeOut/51 vPortExitCritical/45 vPortEnterCritical/42 vTaskSuspendAll/50 vPortExitCritical/45 vTaskInternalSetTimeOutState/49 vPortExitCritical/45 vPortRaiseBASEPRI/1 vPortExitCritical/45 xTaskRemoveFromEventList/43 pvTaskIncrementMutexHeldCount/55 vPortEnterCritical/42 vPortRaiseBASEPRI/1 xTaskGetSchedulerState/48 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xQueueReceive/18 (xQueueReceive) @05fe4620
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: prvIsQueueEmpty/34 xTaskResumeAll/53 prvUnlockQueue/33 xTaskResumeAll/53 prvUnlockQueue/33 xTaskResumeAll/53 prvUnlockQueue/33 vTaskPlaceOnEventList/52 prvIsQueueEmpty/34 xTaskCheckForTimeOut/51 vPortExitCritical/45 vPortEnterCritical/42 vTaskSuspendAll/50 vPortExitCritical/45 vTaskInternalSetTimeOutState/49 vPortExitCritical/45 vPortExitCritical/45 xTaskRemoveFromEventList/43 prvCopyDataFromQueue/32 vPortEnterCritical/42 vPortRaiseBASEPRI/1 xTaskGetSchedulerState/48 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xQueueGiveFromISR/17 (xQueueGiveFromISR) @05fe4000
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortSetBASEPRI/3 vPortRaiseBASEPRI/1 xTaskRemoveFromEventList/43 ulPortRaiseBASEPRI/2 vPortValidateInterruptPriority/54 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xQueueGenericSendFromISR/16 (xQueueGenericSendFromISR) @05f8de00
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortSetBASEPRI/3 vPortRaiseBASEPRI/1 xTaskRemoveFromEventList/43 prvCopyDataToQueue/31 ulPortRaiseBASEPRI/2 vPortValidateInterruptPriority/54 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xQueueGenericSend/15 (xQueueGenericSend) @05f8d9a0
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: xQueueGiveMutexRecursive/12 prvInitialiseMutex/8 
  Calls: xTaskResumeAll/53 prvUnlockQueue/33 xTaskResumeAll/53 prvUnlockQueue/33 xTaskResumeAll/53 prvUnlockQueue/33 vTaskPlaceOnEventList/52 prvIsQueueFull/36 xTaskCheckForTimeOut/51 vPortExitCritical/45 vPortEnterCritical/42 vTaskSuspendAll/50 vPortExitCritical/45 vTaskInternalSetTimeOutState/49 vPortExitCritical/45 vPortExitCritical/45 xTaskRemoveFromEventList/43 prvCopyDataToQueue/31 vPortEnterCritical/42 vPortRaiseBASEPRI/1 xTaskGetSchedulerState/48 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xQueueCreateCountingSemaphore/14 (xQueueCreateCountingSemaphore) @05f8d2a0
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortRaiseBASEPRI/1 xQueueGenericCreate/6 
xQueueTakeMutexRecursive/13 (xQueueTakeMutexRecursive) @05f85ee0
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: xQueueSemaphoreTake/19 xTaskGetCurrentTaskHandle/47 vPortRaiseBASEPRI/1 
xQueueGiveMutexRecursive/12 (xQueueGiveMutexRecursive) @05f85540
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: xQueueGenericSend/15 xTaskGetCurrentTaskHandle/47 vPortRaiseBASEPRI/1 
xQueueGetMutexHolderFromISR/11 (xQueueGetMutexHolderFromISR) @05f85e00
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortRaiseBASEPRI/1 
xQueueGetMutexHolder/10 (xQueueGetMutexHolder) @05f85a80
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: vPortExitCritical/45 vPortEnterCritical/42 vPortRaiseBASEPRI/1 
xQueueCreateMutex/9 (xQueueCreateMutex) @05f85700
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: 
  Calls: prvInitialiseMutex/8 xQueueGenericCreate/6 
prvInitialiseMutex/8 (prvInitialiseMutex) @05f85460
  Type: function definition analyzed
  Visibility: force_output no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: xQueueCreateMutex/9 
  Calls: xQueueGenericSend/15 
prvInitialiseNewQueue/7 (prvInitialiseNewQueue) @05f851c0
  Type: function definition analyzed
  Visibility: force_output no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: xQueueGenericCreate/6 
  Calls: xQueueGenericReset/5 
xQueueGenericCreate/6 (xQueueGenericCreate) @05f9ce00
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: xQueueCreateCountingSemaphore/14 xQueueCreateMutex/9 
  Calls: vPortRaiseBASEPRI/1 prvInitialiseNewQueue/7 pvPortMalloc/46 
xQueueGenericReset/5 (xQueueGenericReset) @05f9cd20
  Type: function definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: 
  Availability: available
  Function flags: body
  Called by: prvInitialiseNewQueue/7 
  Calls: vPortRaiseBASEPRI/1 vPortExitCritical/45 vListInitialise/44 vListInitialise/44 xTaskRemoveFromEventList/43 vPortEnterCritical/42 vPortRaiseBASEPRI/1 
xQueueRegistry/4 (xQueueRegistry) @05f98630
  Type: variable definition analyzed
  Visibility: force_output externally_visible no_reorder public
  References: 
  Referring: vQueueAddToRegistry/38 (read)vQueueAddToRegistry/38 (addr)vQueueAddToRegistry/38 (read)vQueueAddToRegistry/38 (addr)pcQueueGetName/39 (read)pcQueueGetName/39 (read)vQueueUnregisterQueue/40 (read)vQueueUnregisterQueue/40 (write)vQueueUnregisterQueue/40 (write)
  Availability: available
  Varpool flags:
vPortSetBASEPRI/3 (vPortSetBASEPRI) @05f1bb60
  Type: function definition analyzed
  Visibility: no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local
  Called by: xQueuePeekFromISR/22 xQueueReceiveFromISR/21 xQueueGiveFromISR/17 xQueueGenericSendFromISR/16 
  Calls: 
ulPortRaiseBASEPRI/2 (ulPortRaiseBASEPRI) @05f1b8c0
  Type: function definition analyzed
  Visibility: no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local
  Called by: xQueuePeekFromISR/22 xQueueReceiveFromISR/21 xQueueGiveFromISR/17 xQueueGenericSendFromISR/16 
  Calls: 
vPortRaiseBASEPRI/1 (vPortRaiseBASEPRI) @05f1b540
  Type: function definition analyzed
  Visibility: no_reorder prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local
  Called by: vQueueUnregisterQueue/40 pcQueueGetName/39 vQueueAddToRegistry/38 xQueueIsQueueFullFromISR/37 xQueueIsQueueEmptyFromISR/35 vQueueDelete/26 uxQueueMessagesWaitingFromISR/25 uxQueueSpacesAvailable/24 uxQueueMessagesWaiting/23 xQueuePeekFromISR/22 xQueuePeekFromISR/22 xQueuePeekFromISR/22 xQueueReceiveFromISR/21 xQueueReceiveFromISR/21 xQueueReceiveFromISR/21 xQueuePeek/20 xQueuePeek/20 xQueuePeek/20 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueSemaphoreTake/19 xQueueReceive/18 xQueueReceive/18 xQueueReceive/18 xQueueGiveFromISR/17 xQueueGiveFromISR/17 xQueueGiveFromISR/17 xQueueGiveFromISR/17 xQueueGenericSendFromISR/16 xQueueGenericSendFromISR/16 xQueueGenericSendFromISR/16 xQueueGenericSendFromISR/16 xQueueGenericSend/15 xQueueGenericSend/15 xQueueGenericSend/15 xQueueGenericSend/15 xQueueCreateCountingSemaphore/14 xQueueTakeMutexRecursive/13 xQueueGiveMutexRecursive/12 xQueueGetMutexHolderFromISR/11 xQueueGetMutexHolder/10 xQueueGenericCreate/6 xQueueGenericReset/5 xQueueGenericReset/5 
  Calls: 
vQueueWaitForMessageRestricted (struct QueueDefinition * xQueue, TickType_t xTicksToWait, const BaseType_t xWaitIndefinitely)
{
  struct Queue_t * const pxQueue;

  <bb 2> :
  pxQueue = xQueue;
  vPortEnterCritical ();
  _1 = pxQueue->cRxLock;
  if (_1 == -1)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  pxQueue->cRxLock = 0;

  <bb 4> :
  _2 = pxQueue->cTxLock;
  if (_2 == -1)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  pxQueue->cTxLock = 0;

  <bb 6> :
  vPortExitCritical ();
  _3 = pxQueue->uxMessagesWaiting;
  if (_3 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  _4 = &pxQueue->xTasksWaitingToReceive;
  vTaskPlaceOnEventListRestricted (_4, xTicksToWait, xWaitIndefinitely);

  <bb 8> :
  prvUnlockQueue (pxQueue);
  return;

}


vQueueUnregisterQueue (struct QueueDefinition * xQueue)
{
  UBaseType_t ux;

  <bb 2> :
  if (xQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  ux = 0;
  goto <bb 9>; [INV]

  <bb 6> :
  _1 = xQueueRegistry[ux].xHandle;
  if (xQueue == _1)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  xQueueRegistry[ux].pcQueueName = 0B;
  xQueueRegistry[ux].xHandle = 0B;
  goto <bb 10>; [INV]

  <bb 8> :
  ux = ux + 1;

  <bb 9> :
  if (ux <= 1)
    goto <bb 6>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 10> :
  return;

}


pcQueueGetName (struct QueueDefinition * xQueue)
{
  const char * pcReturn;
  UBaseType_t ux;
  const char * D.7264;

  <bb 2> :
  pcReturn = 0B;
  if (xQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  ux = 0;
  goto <bb 9>; [INV]

  <bb 6> :
  _1 = xQueueRegistry[ux].xHandle;
  if (xQueue == _1)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  pcReturn = xQueueRegistry[ux].pcQueueName;
  goto <bb 10>; [INV]

  <bb 8> :
  ux = ux + 1;

  <bb 9> :
  if (ux <= 1)
    goto <bb 6>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 10> :
  D.7264 = pcReturn;

  <bb 11> :
<L8>:
  return D.7264;

}


vQueueAddToRegistry (struct QueueDefinition * xQueue, const char * pcQueueName)
{
  struct QueueRegistryItem_t * pxEntryToWrite;
  UBaseType_t ux;

  <bb 2> :
  if (xQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  pxEntryToWrite = 0B;
  if (pcQueueName != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 6> :
  ux = 0;
  goto <bb 13>; [INV]

  <bb 7> :
  _1 = xQueueRegistry[ux].xHandle;
  if (xQueue == _1)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  pxEntryToWrite = &xQueueRegistry[ux];
  goto <bb 14>; [INV]

  <bb 9> :
  if (pxEntryToWrite == 0B)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  _2 = xQueueRegistry[ux].pcQueueName;
  if (_2 == 0B)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  pxEntryToWrite = &xQueueRegistry[ux];

  <bb 12> :
  ux = ux + 1;

  <bb 13> :
  if (ux <= 1)
    goto <bb 7>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 14> :
  if (pxEntryToWrite != 0B)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  pxEntryToWrite->pcQueueName = pcQueueName;
  pxEntryToWrite->xHandle = xQueue;

  <bb 16> :
  return;

}


xQueueIsQueueFullFromISR (struct QueueDefinition * const xQueue)
{
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  BaseType_t D.7245;

  <bb 2> :
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  _1 = pxQueue->uxMessagesWaiting;
  _2 = pxQueue->uxLength;
  if (_1 == _2)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  xReturn = 1;
  goto <bb 8>; [INV]

  <bb 7> :
  xReturn = 0;

  <bb 8> :
  D.7245 = xReturn;

  <bb 9> :
<L6>:
  return D.7245;

}


prvIsQueueFull (const struct Queue_t * pxQueue)
{
  BaseType_t xReturn;
  BaseType_t D.7238;

  <bb 2> :
  vPortEnterCritical ();
  _1 = pxQueue->uxMessagesWaiting;
  _2 = pxQueue->uxLength;
  if (_1 == _2)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  xReturn = 1;
  goto <bb 5>; [INV]

  <bb 4> :
  xReturn = 0;

  <bb 5> :
  vPortExitCritical ();
  D.7238 = xReturn;

  <bb 6> :
<L3>:
  return D.7238;

}


xQueueIsQueueEmptyFromISR (struct QueueDefinition * const xQueue)
{
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  BaseType_t D.7233;

  <bb 2> :
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  _1 = pxQueue->uxMessagesWaiting;
  if (_1 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  xReturn = 1;
  goto <bb 8>; [INV]

  <bb 7> :
  xReturn = 0;

  <bb 8> :
  D.7233 = xReturn;

  <bb 9> :
<L6>:
  return D.7233;

}


prvIsQueueEmpty (const struct Queue_t * pxQueue)
{
  BaseType_t xReturn;
  BaseType_t D.7226;

  <bb 2> :
  vPortEnterCritical ();
  _1 = pxQueue->uxMessagesWaiting;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  xReturn = 1;
  goto <bb 5>; [INV]

  <bb 4> :
  xReturn = 0;

  <bb 5> :
  vPortExitCritical ();
  D.7226 = xReturn;

  <bb 6> :
<L3>:
  return D.7226;

}


prvUnlockQueue (struct Queue_t * const pxQueue)
{
  int8_t cRxLock;
  int8_t cTxLock;

  <bb 2> :
  vPortEnterCritical ();
  cTxLock = pxQueue->cTxLock;
  goto <bb 8>; [INV]

  <bb 3> :
  _1 = pxQueue->xTasksWaitingToReceive.uxNumberOfItems;
  if (_1 != 0)
    goto <bb 4>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 4> :
  _2 = &pxQueue->xTasksWaitingToReceive;
  _3 = xTaskRemoveFromEventList (_2);
  if (_3 != 0)
    goto <bb 5>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 5> :
  vTaskMissedYield ();
  goto <bb 7>; [INV]

  <bb 6> :
  goto <bb 9>; [INV]

  <bb 7> :
  cTxLock.28_4 = (unsigned char) cTxLock;
  _5 = cTxLock.28_4 + 255;
  cTxLock = (int8_t) _5;

  <bb 8> :
  if (cTxLock > 0)
    goto <bb 3>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 9> :
  pxQueue->cTxLock = -1;
  vPortExitCritical ();
  vPortEnterCritical ();
  cRxLock = pxQueue->cRxLock;
  goto <bb 15>; [INV]

  <bb 10> :
  _6 = pxQueue->xTasksWaitingToSend.uxNumberOfItems;
  if (_6 != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 11> :
  _7 = &pxQueue->xTasksWaitingToSend;
  _8 = xTaskRemoveFromEventList (_7);
  if (_8 != 0)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  vTaskMissedYield ();

  <bb 13> :
  cRxLock.29_9 = (unsigned char) cRxLock;
  _10 = cRxLock.29_9 + 255;
  cRxLock = (int8_t) _10;
  goto <bb 15>; [INV]

  <bb 14> :
  goto <bb 16>; [INV]

  <bb 15> :
  if (cRxLock > 0)
    goto <bb 10>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 16> :
  pxQueue->cRxLock = -1;
  vPortExitCritical ();
  return;

}


prvCopyDataFromQueue (struct Queue_t * const pxQueue, void * const pvBuffer)
{
  <bb 2> :
  _1 = pxQueue->uxItemSize;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 3> :
  _2 = pxQueue->u.xQueue.pcReadFrom;
  _3 = pxQueue->uxItemSize;
  _4 = _2 + _3;
  pxQueue->u.xQueue.pcReadFrom = _4;
  _5 = pxQueue->u.xQueue.pcReadFrom;
  _6 = pxQueue->u.xQueue.pcTail;
  if (_5 >= _6)
    goto <bb 4>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 4> :
  _7 = pxQueue->pcHead;
  pxQueue->u.xQueue.pcReadFrom = _7;

  <bb 5> :
  _8 = pxQueue->u.xQueue.pcReadFrom;
  _9 = pxQueue->uxItemSize;
  memcpy (pvBuffer, _8, _9);

  <bb 6> :
  return;

}


prvCopyDataToQueue (struct Queue_t * const pxQueue, const void * pvItemToQueue, const BaseType_t xPosition)
{
  UBaseType_t uxMessagesWaiting;
  BaseType_t xReturn;
  BaseType_t D.7204;

  <bb 2> :
  xReturn = 0;
  uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  _1 = pxQueue->uxItemSize;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  _2 = pxQueue->pcHead;
  if (_2 == 0B)
    goto <bb 4>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 4> :
  _3 = pxQueue->u.xSemaphore.xMutexHolder;
  xReturn = xTaskPriorityDisinherit (_3);
  pxQueue->u.xSemaphore.xMutexHolder = 0B;
  goto <bb 13>; [INV]

  <bb 5> :
  if (xPosition == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  _4 = pxQueue->pcWriteTo;
  _5 = pxQueue->uxItemSize;
  memcpy (_4, pvItemToQueue, _5);
  _6 = pxQueue->pcWriteTo;
  _7 = pxQueue->uxItemSize;
  _8 = _6 + _7;
  pxQueue->pcWriteTo = _8;
  _9 = pxQueue->pcWriteTo;
  _10 = pxQueue->u.xQueue.pcTail;
  if (_9 >= _10)
    goto <bb 7>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 7> :
  _11 = pxQueue->pcHead;
  pxQueue->pcWriteTo = _11;
  goto <bb 13>; [INV]

  <bb 8> :
  _12 = pxQueue->u.xQueue.pcReadFrom;
  _13 = pxQueue->uxItemSize;
  memcpy (_12, pvItemToQueue, _13);
  _14 = pxQueue->u.xQueue.pcReadFrom;
  _15 = pxQueue->uxItemSize;
  _16 = -_15;
  _17 = _14 + _16;
  pxQueue->u.xQueue.pcReadFrom = _17;
  _18 = pxQueue->u.xQueue.pcReadFrom;
  _19 = pxQueue->pcHead;
  if (_18 < _19)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  _20 = pxQueue->u.xQueue.pcTail;
  _21 = pxQueue->uxItemSize;
  _22 = -_21;
  _23 = _20 + _22;
  pxQueue->u.xQueue.pcReadFrom = _23;

  <bb 10> :
  if (xPosition == 2)
    goto <bb 11>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 11> :
  if (uxMessagesWaiting != 0)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  uxMessagesWaiting = uxMessagesWaiting + 4294967295;

  <bb 13> :
  _24 = uxMessagesWaiting + 1;
  pxQueue->uxMessagesWaiting = _24;
  D.7204 = xReturn;

  <bb 14> :
<L21>:
  return D.7204;

}


prvGetDisinheritPriorityAfterTimeout (const struct Queue_t * const pxQueue)
{
  UBaseType_t uxHighestPriorityOfWaitingTasks;
  UBaseType_t D.7181;

  <bb 2> :
  _1 = pxQueue->xTasksWaitingToReceive.uxNumberOfItems;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  _2 = pxQueue->xTasksWaitingToReceive.xListEnd.pxNext;
  _3 = _2->xItemValue;
  uxHighestPriorityOfWaitingTasks = 5 - _3;
  goto <bb 5>; [INV]

  <bb 4> :
  uxHighestPriorityOfWaitingTasks = 0;

  <bb 5> :
  D.7181 = uxHighestPriorityOfWaitingTasks;

  <bb 6> :
<L3>:
  return D.7181;

}


ucQueueGetQueueType (struct QueueDefinition * xQueue)
{
  uint8_t D.7176;

  <bb 2> :
  D.7176 = MEM[(struct Queue_t *)xQueue].ucQueueType;

  <bb 3> :
<L0>:
  return D.7176;

}


vQueueSetQueueNumber (struct QueueDefinition * xQueue, UBaseType_t uxQueueNumber)
{
  <bb 2> :
  MEM[(struct Queue_t *)xQueue].uxQueueNumber = uxQueueNumber;
  return;

}


uxQueueGetQueueNumber (struct QueueDefinition * xQueue)
{
  UBaseType_t D.7174;

  <bb 2> :
  D.7174 = MEM[(struct Queue_t *)xQueue].uxQueueNumber;

  <bb 3> :
<L0>:
  return D.7174;

}


vQueueDelete (struct QueueDefinition * xQueue)
{
  struct Queue_t * const pxQueue;

  <bb 2> :
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  vQueueUnregisterQueue (pxQueue);
  vPortFree (pxQueue);
  return;

}


uxQueueMessagesWaitingFromISR (struct QueueDefinition * const xQueue)
{
  struct Queue_t * const pxQueue;
  UBaseType_t uxReturn;
  UBaseType_t D.7170;

  <bb 2> :
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  uxReturn = pxQueue->uxMessagesWaiting;
  D.7170 = uxReturn;

  <bb 6> :
<L3>:
  return D.7170;

}


uxQueueSpacesAvailable (struct QueueDefinition * const xQueue)
{
  struct Queue_t * const pxQueue;
  UBaseType_t uxReturn;
  UBaseType_t D.7166;

  <bb 2> :
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  vPortEnterCritical ();
  _1 = pxQueue->uxLength;
  _2 = pxQueue->uxMessagesWaiting;
  uxReturn = _1 - _2;
  vPortExitCritical ();
  D.7166 = uxReturn;

  <bb 6> :
<L3>:
  return D.7166;

}


uxQueueMessagesWaiting (struct QueueDefinition * const xQueue)
{
  UBaseType_t uxReturn;
  UBaseType_t D.7162;

  <bb 2> :
  if (xQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  vPortEnterCritical ();
  uxReturn = MEM[(struct Queue_t *)xQueue].uxMessagesWaiting;
  vPortExitCritical ();
  D.7162 = uxReturn;

  <bb 6> :
<L3>:
  return D.7162;

}


xQueuePeekFromISR (struct QueueDefinition * xQueue, void * const pvBuffer)
{
  struct Queue_t * const pxQueue;
  int8_t * pcOriginalReadPosition;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  BaseType_t D.7158;
  int iftmp.27;

  <bb 2> :
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  if (pvBuffer != 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 6> :
  _1 = pxQueue->uxItemSize;
  if (_1 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  iftmp.27 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.27 = 0;

  <bb 9> :
  if (iftmp.27 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

  <bb 11> :
  goto <bb 11>; [INV]

  <bb 12> :
  _2 = pxQueue->uxItemSize;
  if (_2 == 0)
    goto <bb 13>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 13> :
  vPortRaiseBASEPRI ();

  <bb 14> :
  goto <bb 14>; [INV]

  <bb 15> :
  vPortValidateInterruptPriority ();
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  _3 = pxQueue->uxMessagesWaiting;
  if (_3 != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  pcOriginalReadPosition = pxQueue->u.xQueue.pcReadFrom;
  prvCopyDataFromQueue (pxQueue, pvBuffer);
  pxQueue->u.xQueue.pcReadFrom = pcOriginalReadPosition;
  xReturn = 1;
  goto <bb 18>; [INV]

  <bb 17> :
  xReturn = 0;

  <bb 18> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.7158 = xReturn;

  <bb 19> :
<L16>:
  return D.7158;

}


xQueueReceiveFromISR (struct QueueDefinition * xQueue, void * const pvBuffer, BaseType_t * const pxHigherPriorityTaskWoken)
{
  const int8_t cRxLock;
  const UBaseType_t uxMessagesWaiting;
  struct Queue_t * const pxQueue;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  BaseType_t D.7142;
  int iftmp.25;

  <bb 2> :
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  if (pvBuffer != 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 6> :
  _1 = pxQueue->uxItemSize;
  if (_1 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  iftmp.25 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.25 = 0;

  <bb 9> :
  if (iftmp.25 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

  <bb 11> :
  goto <bb 11>; [INV]

  <bb 12> :
  vPortValidateInterruptPriority ();
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  if (uxMessagesWaiting != 0)
    goto <bb 13>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 13> :
  cRxLock = pxQueue->cRxLock;
  prvCopyDataFromQueue (pxQueue, pvBuffer);
  _2 = uxMessagesWaiting + 4294967295;
  pxQueue->uxMessagesWaiting = _2;
  if (cRxLock == -1)
    goto <bb 14>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 14> :
  _3 = pxQueue->xTasksWaitingToSend.uxNumberOfItems;
  if (_3 != 0)
    goto <bb 15>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 15> :
  _4 = &pxQueue->xTasksWaitingToSend;
  _5 = xTaskRemoveFromEventList (_4);
  if (_5 != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 16> :
  if (pxHigherPriorityTaskWoken != 0B)
    goto <bb 17>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 17> :
  *pxHigherPriorityTaskWoken = 1;
  goto <bb 22>; [INV]

  <bb 18> :
  if (cRxLock == 127)
    goto <bb 19>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 19> :
  vPortRaiseBASEPRI ();

  <bb 20> :
  goto <bb 20>; [INV]

  <bb 21> :
  cRxLock.26_6 = (unsigned char) cRxLock;
  _7 = cRxLock.26_6 + 1;
  _8 = (signed char) _7;
  pxQueue->cRxLock = _8;

  <bb 22> :
  xReturn = 1;
  goto <bb 24>; [INV]

  <bb 23> :
  xReturn = 0;

  <bb 24> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.7142 = xReturn;

  <bb 25> :
<L28>:
  return D.7142;

}


xQueuePeek (struct QueueDefinition * xQueue, void * const pvBuffer, TickType_t xTicksToWait)
{
  const UBaseType_t uxMessagesWaiting;
  struct Queue_t * const pxQueue;
  int8_t * pcOriginalReadPosition;
  struct TimeOut_t xTimeOut;
  BaseType_t xEntryTimeSet;
  BaseType_t D.7093;
  int iftmp.21;
  int iftmp.20;

  <bb 2> :
  xEntryTimeSet = 0;
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  if (pvBuffer != 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 6> :
  _1 = pxQueue->uxItemSize;
  if (_1 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  iftmp.20 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.20 = 0;

  <bb 9> :
  if (iftmp.20 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

  <bb 11> :
  goto <bb 11>; [INV]

  <bb 12> :
  _2 = xTaskGetSchedulerState ();
  if (_2 != 0)
    goto <bb 14>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 13> :
  xTicksToWait.22_3 = xTicksToWait;
  if (xTicksToWait.22_3 == 0)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  iftmp.21 = 1;
  goto <bb 16>; [INV]

  <bb 15> :
  iftmp.21 = 0;

  <bb 16> :
  if (iftmp.21 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 17> :
  vPortRaiseBASEPRI ();

  <bb 18> :
  goto <bb 18>; [INV]

  <bb 19> :
  vPortEnterCritical ();
  uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  if (uxMessagesWaiting != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 20> :
  pcOriginalReadPosition = pxQueue->u.xQueue.pcReadFrom;
  prvCopyDataFromQueue (pxQueue, pvBuffer);
  pxQueue->u.xQueue.pcReadFrom = pcOriginalReadPosition;
  _4 = pxQueue->xTasksWaitingToReceive.uxNumberOfItems;
  if (_4 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 21> :
  _5 = &pxQueue->xTasksWaitingToReceive;
  _6 = xTaskRemoveFromEventList (_5);
  if (_6 != 0)
    goto <bb 22>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 22> :
  _7 = 3758157060B;
  *_7 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");

  <bb 23> :
  vPortExitCritical ();
  D.7093 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

  <bb 24> :
  xTicksToWait.23_8 = xTicksToWait;
  if (xTicksToWait.23_8 == 0)
    goto <bb 25>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 25> :
  vPortExitCritical ();
  D.7093 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

  <bb 26> :
  if (xEntryTimeSet == 0)
    goto <bb 27>; [INV]
  else
    goto <bb 28>; [INV]

  <bb 27> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet = 1;

  <bb 28> :
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _9 = pxQueue->cRxLock;
  if (_9 == -1)
    goto <bb 29>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 29> :
  pxQueue->cRxLock = 0;

  <bb 30> :
  _10 = pxQueue->cTxLock;
  if (_10 == -1)
    goto <bb 31>; [INV]
  else
    goto <bb 32>; [INV]

  <bb 31> :
  pxQueue->cTxLock = 0;

  <bb 32> :
  vPortExitCritical ();
  _11 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_11 == 0)
    goto <bb 33>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 33> :
  _12 = prvIsQueueEmpty (pxQueue);
  if (_12 != 0)
    goto <bb 34>; [INV]
  else
    goto <bb 36>; [INV]

  <bb 34> :
  _13 = &pxQueue->xTasksWaitingToReceive;
  xTicksToWait.24_14 = xTicksToWait;
  vTaskPlaceOnEventList (_13, xTicksToWait.24_14);
  prvUnlockQueue (pxQueue);
  _15 = xTaskResumeAll ();
  if (_15 == 0)
    goto <bb 35>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 35> :
  _16 = 3758157060B;
  *_16 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 39>; [INV]

  <bb 36> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  goto <bb 39>; [INV]

  <bb 37> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  _17 = prvIsQueueEmpty (pxQueue);
  if (_17 != 0)
    goto <bb 38>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 38> :
  D.7093 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

  <bb 39> :
  goto <bb 19>; [INV]

  <bb 40> :
  xTimeOut = {CLOBBER};

  <bb 41> :
<L47>:
  return D.7093;

}


xQueueSemaphoreTake (struct QueueDefinition * xQueue, TickType_t xTicksToWait)
{
  UBaseType_t uxHighestWaitingPriority;
  const UBaseType_t uxSemaphoreCount;
  BaseType_t xInheritanceOccurred;
  struct Queue_t * const pxQueue;
  struct TimeOut_t xTimeOut;
  BaseType_t xEntryTimeSet;
  BaseType_t D.7039;
  int iftmp.16;

  <bb 2> :
  xEntryTimeSet = 0;
  pxQueue = xQueue;
  xInheritanceOccurred = 0;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  _1 = pxQueue->uxItemSize;
  if (_1 != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  vPortRaiseBASEPRI ();

  <bb 7> :
  goto <bb 7>; [INV]

  <bb 8> :
  _2 = xTaskGetSchedulerState ();
  if (_2 != 0)
    goto <bb 10>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 9> :
  xTicksToWait.17_3 = xTicksToWait;
  if (xTicksToWait.17_3 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  iftmp.16 = 1;
  goto <bb 12>; [INV]

  <bb 11> :
  iftmp.16 = 0;

  <bb 12> :
  if (iftmp.16 == 0)
    goto <bb 13>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 13> :
  vPortRaiseBASEPRI ();

  <bb 14> :
  goto <bb 14>; [INV]

  <bb 15> :
  vPortEnterCritical ();
  uxSemaphoreCount = pxQueue->uxMessagesWaiting;
  if (uxSemaphoreCount != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 16> :
  _4 = uxSemaphoreCount + 4294967295;
  pxQueue->uxMessagesWaiting = _4;
  _5 = pxQueue->pcHead;
  if (_5 == 0B)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  _6 = pvTaskIncrementMutexHeldCount ();
  pxQueue->u.xSemaphore.xMutexHolder = _6;

  <bb 18> :
  _7 = pxQueue->xTasksWaitingToSend.uxNumberOfItems;
  if (_7 != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 19> :
  _8 = &pxQueue->xTasksWaitingToSend;
  _9 = xTaskRemoveFromEventList (_8);
  if (_9 != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 20> :
  _10 = 3758157060B;
  *_10 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");

  <bb 21> :
  vPortExitCritical ();
  D.7039 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 45>; [INV]

  <bb 22> :
  xTicksToWait.18_11 = xTicksToWait;
  if (xTicksToWait.18_11 == 0)
    goto <bb 23>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 23> :
  if (xInheritanceOccurred != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 24> :
  vPortRaiseBASEPRI ();

  <bb 25> :
  goto <bb 25>; [INV]

  <bb 26> :
  vPortExitCritical ();
  D.7039 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 45>; [INV]

  <bb 27> :
  if (xEntryTimeSet == 0)
    goto <bb 28>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 28> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet = 1;

  <bb 29> :
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _12 = pxQueue->cRxLock;
  if (_12 == -1)
    goto <bb 30>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 30> :
  pxQueue->cRxLock = 0;

  <bb 31> :
  _13 = pxQueue->cTxLock;
  if (_13 == -1)
    goto <bb 32>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 32> :
  pxQueue->cTxLock = 0;

  <bb 33> :
  vPortExitCritical ();
  _14 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_14 == 0)
    goto <bb 34>; [INV]
  else
    goto <bb 40>; [INV]

  <bb 34> :
  _15 = prvIsQueueEmpty (pxQueue);
  if (_15 != 0)
    goto <bb 35>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 35> :
  _16 = pxQueue->pcHead;
  if (_16 == 0B)
    goto <bb 36>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 36> :
  vPortEnterCritical ();
  _17 = pxQueue->u.xSemaphore.xMutexHolder;
  xInheritanceOccurred = xTaskPriorityInherit (_17);
  vPortExitCritical ();

  <bb 37> :
  _18 = &pxQueue->xTasksWaitingToReceive;
  xTicksToWait.19_19 = xTicksToWait;
  vTaskPlaceOnEventList (_18, xTicksToWait.19_19);
  prvUnlockQueue (pxQueue);
  _20 = xTaskResumeAll ();
  if (_20 == 0)
    goto <bb 38>; [INV]
  else
    goto <bb 44>; [INV]

  <bb 38> :
  _21 = 3758157060B;
  *_21 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 44>; [INV]

  <bb 39> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  goto <bb 44>; [INV]

  <bb 40> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  _22 = prvIsQueueEmpty (pxQueue);
  if (_22 != 0)
    goto <bb 41>; [INV]
  else
    goto <bb 44>; [INV]

  <bb 41> :
  if (xInheritanceOccurred != 0)
    goto <bb 42>; [INV]
  else
    goto <bb 43>; [INV]

  <bb 42> :
  vPortEnterCritical ();
  uxHighestWaitingPriority = prvGetDisinheritPriorityAfterTimeout (pxQueue);
  _23 = pxQueue->u.xSemaphore.xMutexHolder;
  vTaskPriorityDisinheritAfterTimeout (_23, uxHighestWaitingPriority);
  vPortExitCritical ();

  <bb 43> :
  D.7039 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 45>; [INV]

  <bb 44> :
  goto <bb 15>; [INV]

  <bb 45> :
  xTimeOut = {CLOBBER};

  <bb 46> :
<L54>:
  return D.7039;

}


xQueueReceive (struct QueueDefinition * xQueue, void * const pvBuffer, TickType_t xTicksToWait)
{
  const UBaseType_t uxMessagesWaiting;
  struct Queue_t * const pxQueue;
  struct TimeOut_t xTimeOut;
  BaseType_t xEntryTimeSet;
  BaseType_t D.6994;
  int iftmp.12;
  int iftmp.11;

  <bb 2> :
  xEntryTimeSet = 0;
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  if (pvBuffer != 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 6> :
  _1 = pxQueue->uxItemSize;
  if (_1 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  iftmp.11 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.11 = 0;

  <bb 9> :
  if (iftmp.11 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

  <bb 11> :
  goto <bb 11>; [INV]

  <bb 12> :
  _2 = xTaskGetSchedulerState ();
  if (_2 != 0)
    goto <bb 14>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 13> :
  xTicksToWait.13_3 = xTicksToWait;
  if (xTicksToWait.13_3 == 0)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  iftmp.12 = 1;
  goto <bb 16>; [INV]

  <bb 15> :
  iftmp.12 = 0;

  <bb 16> :
  if (iftmp.12 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 17> :
  vPortRaiseBASEPRI ();

  <bb 18> :
  goto <bb 18>; [INV]

  <bb 19> :
  vPortEnterCritical ();
  uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  if (uxMessagesWaiting != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 20> :
  prvCopyDataFromQueue (pxQueue, pvBuffer);
  _4 = uxMessagesWaiting + 4294967295;
  pxQueue->uxMessagesWaiting = _4;
  _5 = pxQueue->xTasksWaitingToSend.uxNumberOfItems;
  if (_5 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 21> :
  _6 = &pxQueue->xTasksWaitingToSend;
  _7 = xTaskRemoveFromEventList (_6);
  if (_7 != 0)
    goto <bb 22>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 22> :
  _8 = 3758157060B;
  *_8 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");

  <bb 23> :
  vPortExitCritical ();
  D.6994 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

  <bb 24> :
  xTicksToWait.14_9 = xTicksToWait;
  if (xTicksToWait.14_9 == 0)
    goto <bb 25>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 25> :
  vPortExitCritical ();
  D.6994 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

  <bb 26> :
  if (xEntryTimeSet == 0)
    goto <bb 27>; [INV]
  else
    goto <bb 28>; [INV]

  <bb 27> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet = 1;

  <bb 28> :
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _10 = pxQueue->cRxLock;
  if (_10 == -1)
    goto <bb 29>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 29> :
  pxQueue->cRxLock = 0;

  <bb 30> :
  _11 = pxQueue->cTxLock;
  if (_11 == -1)
    goto <bb 31>; [INV]
  else
    goto <bb 32>; [INV]

  <bb 31> :
  pxQueue->cTxLock = 0;

  <bb 32> :
  vPortExitCritical ();
  _12 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_12 == 0)
    goto <bb 33>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 33> :
  _13 = prvIsQueueEmpty (pxQueue);
  if (_13 != 0)
    goto <bb 34>; [INV]
  else
    goto <bb 36>; [INV]

  <bb 34> :
  _14 = &pxQueue->xTasksWaitingToReceive;
  xTicksToWait.15_15 = xTicksToWait;
  vTaskPlaceOnEventList (_14, xTicksToWait.15_15);
  prvUnlockQueue (pxQueue);
  _16 = xTaskResumeAll ();
  if (_16 == 0)
    goto <bb 35>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 35> :
  _17 = 3758157060B;
  *_17 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 39>; [INV]

  <bb 36> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  goto <bb 39>; [INV]

  <bb 37> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  _18 = prvIsQueueEmpty (pxQueue);
  if (_18 != 0)
    goto <bb 38>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 38> :
  D.6994 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

  <bb 39> :
  goto <bb 19>; [INV]

  <bb 40> :
  xTimeOut = {CLOBBER};

  <bb 41> :
<L47>:
  return D.6994;

}


xQueueGiveFromISR (struct QueueDefinition * xQueue, BaseType_t * const pxHigherPriorityTaskWoken)
{
  const int8_t cTxLock;
  const UBaseType_t uxMessagesWaiting;
  struct Queue_t * const pxQueue;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  BaseType_t D.6968;
  int iftmp.9;

  <bb 2> :
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  _1 = pxQueue->uxItemSize;
  if (_1 != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  vPortRaiseBASEPRI ();

  <bb 7> :
  goto <bb 7>; [INV]

  <bb 8> :
  _2 = pxQueue->pcHead;
  if (_2 != 0B)
    goto <bb 10>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 9> :
  _3 = pxQueue->u.xSemaphore.xMutexHolder;
  if (_3 == 0B)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  iftmp.9 = 1;
  goto <bb 12>; [INV]

  <bb 11> :
  iftmp.9 = 0;

  <bb 12> :
  if (iftmp.9 == 0)
    goto <bb 13>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 13> :
  vPortRaiseBASEPRI ();

  <bb 14> :
  goto <bb 14>; [INV]

  <bb 15> :
  vPortValidateInterruptPriority ();
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  _4 = pxQueue->uxLength;
  if (uxMessagesWaiting < _4)
    goto <bb 16>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 16> :
  cTxLock = pxQueue->cTxLock;
  _5 = uxMessagesWaiting + 1;
  pxQueue->uxMessagesWaiting = _5;
  if (cTxLock == -1)
    goto <bb 17>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 17> :
  _6 = pxQueue->xTasksWaitingToReceive.uxNumberOfItems;
  if (_6 != 0)
    goto <bb 18>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 18> :
  _7 = &pxQueue->xTasksWaitingToReceive;
  _8 = xTaskRemoveFromEventList (_7);
  if (_8 != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 19> :
  if (pxHigherPriorityTaskWoken != 0B)
    goto <bb 20>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 20> :
  *pxHigherPriorityTaskWoken = 1;
  goto <bb 25>; [INV]

  <bb 21> :
  if (cTxLock == 127)
    goto <bb 22>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 22> :
  vPortRaiseBASEPRI ();

  <bb 23> :
  goto <bb 23>; [INV]

  <bb 24> :
  cTxLock.10_9 = (unsigned char) cTxLock;
  _10 = cTxLock.10_9 + 1;
  _11 = (signed char) _10;
  pxQueue->cTxLock = _11;

  <bb 25> :
  xReturn = 1;
  goto <bb 27>; [INV]

  <bb 26> :
  xReturn = 0;

  <bb 27> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.6968 = xReturn;

  <bb 28> :
<L31>:
  return D.6968;

}


xQueueGenericSendFromISR (struct QueueDefinition * xQueue, const void * const pvItemToQueue, BaseType_t * const pxHigherPriorityTaskWoken, const BaseType_t xCopyPosition)
{
  const UBaseType_t uxPreviousMessagesWaiting;
  const int8_t cTxLock;
  struct Queue_t * const pxQueue;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  BaseType_t D.6936;
  int iftmp.7;
  int iftmp.6;

  <bb 2> :
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  if (pvItemToQueue != 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 6> :
  _1 = pxQueue->uxItemSize;
  if (_1 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  iftmp.6 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.6 = 0;

  <bb 9> :
  if (iftmp.6 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

  <bb 11> :
  goto <bb 11>; [INV]

  <bb 12> :
  if (xCopyPosition != 2)
    goto <bb 14>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 13> :
  _2 = pxQueue->uxLength;
  if (_2 == 1)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  iftmp.7 = 1;
  goto <bb 16>; [INV]

  <bb 15> :
  iftmp.7 = 0;

  <bb 16> :
  if (iftmp.7 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 17> :
  vPortRaiseBASEPRI ();

  <bb 18> :
  goto <bb 18>; [INV]

  <bb 19> :
  vPortValidateInterruptPriority ();
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  _3 = pxQueue->uxMessagesWaiting;
  _4 = pxQueue->uxLength;
  if (_3 < _4)
    goto <bb 21>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 20> :
  if (xCopyPosition == 2)
    goto <bb 21>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 21> :
  cTxLock = pxQueue->cTxLock;
  uxPreviousMessagesWaiting = pxQueue->uxMessagesWaiting;
  prvCopyDataToQueue (pxQueue, pvItemToQueue, xCopyPosition);
  if (cTxLock == -1)
    goto <bb 22>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 22> :
  _5 = pxQueue->xTasksWaitingToReceive.uxNumberOfItems;
  if (_5 != 0)
    goto <bb 23>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 23> :
  _6 = &pxQueue->xTasksWaitingToReceive;
  _7 = xTaskRemoveFromEventList (_6);
  if (_7 != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 24> :
  if (pxHigherPriorityTaskWoken != 0B)
    goto <bb 25>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 25> :
  *pxHigherPriorityTaskWoken = 1;
  goto <bb 30>; [INV]

  <bb 26> :
  if (cTxLock == 127)
    goto <bb 27>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 27> :
  vPortRaiseBASEPRI ();

  <bb 28> :
  goto <bb 28>; [INV]

  <bb 29> :
  cTxLock.8_8 = (unsigned char) cTxLock;
  _9 = cTxLock.8_8 + 1;
  _10 = (signed char) _9;
  pxQueue->cTxLock = _10;

  <bb 30> :
  xReturn = 1;
  goto <bb 32>; [INV]

  <bb 31> :
  xReturn = 0;

  <bb 32> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.6936 = xReturn;

  <bb 33> :
<L36>:
  return D.6936;

}


xQueueGenericSend (struct QueueDefinition * xQueue, const void * const pvItemToQueue, TickType_t xTicksToWait, const BaseType_t xCopyPosition)
{
  struct Queue_t * const pxQueue;
  struct TimeOut_t xTimeOut;
  BaseType_t xYieldRequired;
  BaseType_t xEntryTimeSet;
  BaseType_t D.6882;
  int iftmp.2;
  int iftmp.1;
  int iftmp.0;

  <bb 2> :
  xEntryTimeSet = 0;
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  if (pvItemToQueue != 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 6> :
  _1 = pxQueue->uxItemSize;
  if (_1 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  iftmp.0 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.0 = 0;

  <bb 9> :
  if (iftmp.0 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

  <bb 11> :
  goto <bb 11>; [INV]

  <bb 12> :
  if (xCopyPosition != 2)
    goto <bb 14>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 13> :
  _2 = pxQueue->uxLength;
  if (_2 == 1)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  iftmp.1 = 1;
  goto <bb 16>; [INV]

  <bb 15> :
  iftmp.1 = 0;

  <bb 16> :
  if (iftmp.1 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 17> :
  vPortRaiseBASEPRI ();

  <bb 18> :
  goto <bb 18>; [INV]

  <bb 19> :
  _3 = xTaskGetSchedulerState ();
  if (_3 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 20> :
  xTicksToWait.3_4 = xTicksToWait;
  if (xTicksToWait.3_4 == 0)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  iftmp.2 = 1;
  goto <bb 23>; [INV]

  <bb 22> :
  iftmp.2 = 0;

  <bb 23> :
  if (iftmp.2 == 0)
    goto <bb 24>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 24> :
  vPortRaiseBASEPRI ();

  <bb 25> :
  goto <bb 25>; [INV]

  <bb 26> :
  vPortEnterCritical ();
  _5 = pxQueue->uxMessagesWaiting;
  _6 = pxQueue->uxLength;
  if (_5 < _6)
    goto <bb 28>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 27> :
  if (xCopyPosition == 2)
    goto <bb 28>; [INV]
  else
    goto <bb 34>; [INV]

  <bb 28> :
  xYieldRequired = prvCopyDataToQueue (pxQueue, pvItemToQueue, xCopyPosition);
  _7 = pxQueue->xTasksWaitingToReceive.uxNumberOfItems;
  if (_7 != 0)
    goto <bb 29>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 29> :
  _8 = &pxQueue->xTasksWaitingToReceive;
  _9 = xTaskRemoveFromEventList (_8);
  if (_9 != 0)
    goto <bb 30>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 30> :
  _10 = 3758157060B;
  *_10 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 33>; [INV]

  <bb 31> :
  if (xYieldRequired != 0)
    goto <bb 32>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 32> :
  _11 = 3758157060B;
  *_11 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");

  <bb 33> :
  vPortExitCritical ();
  D.6882 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 49>; [INV]

  <bb 34> :
  xTicksToWait.4_12 = xTicksToWait;
  if (xTicksToWait.4_12 == 0)
    goto <bb 35>; [INV]
  else
    goto <bb 36>; [INV]

  <bb 35> :
  vPortExitCritical ();
  D.6882 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 49>; [INV]

  <bb 36> :
  if (xEntryTimeSet == 0)
    goto <bb 37>; [INV]
  else
    goto <bb 38>; [INV]

  <bb 37> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet = 1;

  <bb 38> :
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _13 = pxQueue->cRxLock;
  if (_13 == -1)
    goto <bb 39>; [INV]
  else
    goto <bb 40>; [INV]

  <bb 39> :
  pxQueue->cRxLock = 0;

  <bb 40> :
  _14 = pxQueue->cTxLock;
  if (_14 == -1)
    goto <bb 41>; [INV]
  else
    goto <bb 42>; [INV]

  <bb 41> :
  pxQueue->cTxLock = 0;

  <bb 42> :
  vPortExitCritical ();
  _15 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_15 == 0)
    goto <bb 43>; [INV]
  else
    goto <bb 47>; [INV]

  <bb 43> :
  _16 = prvIsQueueFull (pxQueue);
  if (_16 != 0)
    goto <bb 44>; [INV]
  else
    goto <bb 46>; [INV]

  <bb 44> :
  _17 = &pxQueue->xTasksWaitingToSend;
  xTicksToWait.5_18 = xTicksToWait;
  vTaskPlaceOnEventList (_17, xTicksToWait.5_18);
  prvUnlockQueue (pxQueue);
  _19 = xTaskResumeAll ();
  if (_19 == 0)
    goto <bb 45>; [INV]
  else
    goto <bb 48>; [INV]

  <bb 45> :
  _20 = 3758157060B;
  *_20 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 48>; [INV]

  <bb 46> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  goto <bb 48>; [INV]

  <bb 47> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  D.6882 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 49>; [INV]

  <bb 48> :
  goto <bb 26>; [INV]

  <bb 49> :
  xTimeOut = {CLOBBER};

  <bb 50> :
<L55>:
  return D.6882;

}


xQueueCreateCountingSemaphore (const UBaseType_t uxMaxCount, const UBaseType_t uxInitialCount)
{
  struct QueueDefinition * xHandle;
  struct QueueDefinition * D.6845;

  <bb 2> :
  xHandle = 0B;
  if (uxMaxCount != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 3> :
  if (uxInitialCount <= uxMaxCount)
    goto <bb 4>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 4> :
  xHandle = xQueueGenericCreate (uxMaxCount, 0, 2);
  if (xHandle != 0B)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  MEM[(struct Queue_t *)xHandle].uxMessagesWaiting = uxInitialCount;

  <bb 6> :
  goto <bb 10>; [INV]

  <bb 7> :
  if (xHandle == 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 8> :
  vPortRaiseBASEPRI ();

  <bb 9> :
  goto <bb 9>; [INV]

  <bb 10> :
  D.6845 = xHandle;

  <bb 11> :
<L10>:
  return D.6845;

}


xQueueTakeMutexRecursive (struct QueueDefinition * xMutex, TickType_t xTicksToWait)
{
  struct Queue_t * const pxMutex;
  BaseType_t xReturn;
  BaseType_t D.6834;

  <bb 2> :
  pxMutex = xMutex;
  if (pxMutex == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  _1 = pxMutex->u.xSemaphore.xMutexHolder;
  _2 = xTaskGetCurrentTaskHandle ();
  if (_1 == _2)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  _3 = pxMutex->u.xSemaphore.uxRecursiveCallCount;
  _4 = _3 + 1;
  pxMutex->u.xSemaphore.uxRecursiveCallCount = _4;
  xReturn = 1;
  goto <bb 9>; [INV]

  <bb 7> :
  xReturn = xQueueSemaphoreTake (pxMutex, xTicksToWait);
  if (xReturn != 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  _5 = pxMutex->u.xSemaphore.uxRecursiveCallCount;
  _6 = _5 + 1;
  pxMutex->u.xSemaphore.uxRecursiveCallCount = _6;

  <bb 9> :
  D.6834 = xReturn;

  <bb 10> :
<L9>:
  return D.6834;

}


xQueueGiveMutexRecursive (struct QueueDefinition * xMutex)
{
  struct Queue_t * const pxMutex;
  BaseType_t xReturn;
  BaseType_t D.6824;

  <bb 2> :
  pxMutex = xMutex;
  if (pxMutex == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  _1 = pxMutex->u.xSemaphore.xMutexHolder;
  _2 = xTaskGetCurrentTaskHandle ();
  if (_1 == _2)
    goto <bb 6>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 6> :
  _3 = pxMutex->u.xSemaphore.uxRecursiveCallCount;
  _4 = _3 + 4294967295;
  pxMutex->u.xSemaphore.uxRecursiveCallCount = _4;
  _5 = pxMutex->u.xSemaphore.uxRecursiveCallCount;
  if (_5 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  xQueueGenericSend (pxMutex, 0B, 0, 0);

  <bb 8> :
  xReturn = 1;
  goto <bb 10>; [INV]

  <bb 9> :
  xReturn = 0;

  <bb 10> :
  D.6824 = xReturn;

  <bb 11> :
<L9>:
  return D.6824;

}


xQueueGetMutexHolderFromISR (struct QueueDefinition * xSemaphore)
{
  struct tskTaskControlBlock * pxReturn;
  struct tskTaskControlBlock * D.6814;

  <bb 2> :
  if (xSemaphore == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  _1 = MEM[(struct Queue_t *)xSemaphore].pcHead;
  if (_1 == 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  pxReturn = MEM[(struct Queue_t *)xSemaphore].u.xSemaphore.xMutexHolder;
  goto <bb 8>; [INV]

  <bb 7> :
  pxReturn = 0B;

  <bb 8> :
  D.6814 = pxReturn;

  <bb 9> :
<L6>:
  return D.6814;

}


xQueueGetMutexHolder (struct QueueDefinition * xSemaphore)
{
  struct Queue_t * const pxSemaphore;
  struct tskTaskControlBlock * pxReturn;
  struct tskTaskControlBlock * D.6807;

  <bb 2> :
  pxSemaphore = xSemaphore;
  if (xSemaphore == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  vPortEnterCritical ();
  _1 = pxSemaphore->pcHead;
  if (_1 == 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  pxReturn = pxSemaphore->u.xSemaphore.xMutexHolder;
  goto <bb 8>; [INV]

  <bb 7> :
  pxReturn = 0B;

  <bb 8> :
  vPortExitCritical ();
  D.6807 = pxReturn;

  <bb 9> :
<L6>:
  return D.6807;

}


xQueueCreateMutex (const uint8_t ucQueueType)
{
  const UBaseType_t uxMutexSize;
  const UBaseType_t uxMutexLength;
  struct QueueDefinition * xNewQueue;
  struct QueueDefinition * D.6800;

  <bb 2> :
  uxMutexLength = 1;
  uxMutexSize = 0;
  xNewQueue = xQueueGenericCreate (uxMutexLength, uxMutexSize, ucQueueType);
  prvInitialiseMutex (xNewQueue);
  D.6800 = xNewQueue;

  <bb 3> :
<L0>:
  return D.6800;

}


prvInitialiseMutex (struct Queue_t * pxNewQueue)
{
  <bb 2> :
  if (pxNewQueue != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  pxNewQueue->u.xSemaphore.xMutexHolder = 0B;
  pxNewQueue->pcHead = 0B;
  pxNewQueue->u.xSemaphore.uxRecursiveCallCount = 0;
  xQueueGenericSend (pxNewQueue, 0B, 0, 0);

  <bb 4> :
  return;

}


prvInitialiseNewQueue (const UBaseType_t uxQueueLength, const UBaseType_t uxItemSize, uint8_t * pucQueueStorage, const uint8_t ucQueueType, struct Queue_t * pxNewQueue)
{
  <bb 2> :
  if (uxItemSize == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  pxNewQueue->pcHead = pxNewQueue;
  goto <bb 5>; [INV]

  <bb 4> :
  pxNewQueue->pcHead = pucQueueStorage;

  <bb 5> :
  pxNewQueue->uxLength = uxQueueLength;
  pxNewQueue->uxItemSize = uxItemSize;
  xQueueGenericReset (pxNewQueue, 1);
  pxNewQueue->ucQueueType = ucQueueType;
  return;

}


xQueueGenericCreate (const UBaseType_t uxQueueLength, const UBaseType_t uxItemSize, const uint8_t ucQueueType)
{
  uint8_t * pucQueueStorage;
  size_t xQueueSizeInBytes;
  struct Queue_t * pxNewQueue;
  struct QueueDefinition * D.6792;

  <bb 2> :
  pxNewQueue = 0B;
  if (uxQueueLength != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 3> :
  _1 = .MUL_OVERFLOW (uxItemSize, uxQueueLength);
  _2 = IMAGPART_EXPR <_1>;
  if (_2 == 0)
    goto <bb 4>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 4> :
  _3 = uxQueueLength * uxItemSize;
  if (_3 <= 4294967215)
    goto <bb 5>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 5> :
  xQueueSizeInBytes = uxQueueLength * uxItemSize;
  _4 = xQueueSizeInBytes + 80;
  pxNewQueue = pvPortMalloc (_4);
  if (pxNewQueue != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  pucQueueStorage = pxNewQueue;
  pucQueueStorage = pucQueueStorage + 80;
  prvInitialiseNewQueue (uxQueueLength, uxItemSize, pucQueueStorage, ucQueueType, pxNewQueue);

  <bb 7> :
  goto <bb 11>; [INV]

  <bb 8> :
  if (pxNewQueue == 0B)
    goto <bb 9>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 9> :
  vPortRaiseBASEPRI ();

  <bb 10> :
  goto <bb 10>; [INV]

  <bb 11> :
  D.6792 = pxNewQueue;

  <bb 12> :
<L11>:
  return D.6792;

}


xQueueGenericReset (struct QueueDefinition * xQueue, BaseType_t xNewQueue)
{
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  BaseType_t D.6780;

  <bb 2> :
  xReturn = 1;
  pxQueue = xQueue;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

  <bb 4> :
  goto <bb 4>; [INV]

  <bb 5> :
  if (pxQueue != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 6> :
  _1 = pxQueue->uxLength;
  if (_1 != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 7> :
  _3 = pxQueue->uxItemSize;
  _4 = pxQueue->uxLength;
  _2 = .MUL_OVERFLOW (_3, _4);
  _5 = IMAGPART_EXPR <_2>;
  if (_5 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 8> :
  vPortEnterCritical ();
  _6 = pxQueue->pcHead;
  _7 = pxQueue->uxLength;
  _8 = pxQueue->uxItemSize;
  _9 = _7 * _8;
  _10 = _6 + _9;
  pxQueue->u.xQueue.pcTail = _10;
  pxQueue->uxMessagesWaiting = 0;
  _11 = pxQueue->pcHead;
  pxQueue->pcWriteTo = _11;
  _12 = pxQueue->pcHead;
  _13 = pxQueue->uxLength;
  _14 = _13 + 4294967295;
  _15 = pxQueue->uxItemSize;
  _16 = _14 * _15;
  _17 = _12 + _16;
  pxQueue->u.xQueue.pcReadFrom = _17;
  pxQueue->cRxLock = -1;
  pxQueue->cTxLock = -1;
  if (xNewQueue == 0)
    goto <bb 9>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 9> :
  _18 = pxQueue->xTasksWaitingToSend.uxNumberOfItems;
  if (_18 != 0)
    goto <bb 10>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 10> :
  _19 = &pxQueue->xTasksWaitingToSend;
  _20 = xTaskRemoveFromEventList (_19);
  if (_20 != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 11> :
  _21 = 3758157060B;
  *_21 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 13>; [INV]

  <bb 12> :
  _22 = &pxQueue->xTasksWaitingToSend;
  vListInitialise (_22);
  _23 = &pxQueue->xTasksWaitingToReceive;
  vListInitialise (_23);

  <bb 13> :
  vPortExitCritical ();
  goto <bb 15>; [INV]

  <bb 14> :
  xReturn = 0;

  <bb 15> :
  if (xReturn == 0)
    goto <bb 16>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 16> :
  vPortRaiseBASEPRI ();

  <bb 17> :
  goto <bb 17>; [INV]

  <bb 18> :
  D.6780 = xReturn;

  <bb 19> :
<L20>:
  return D.6780;

}


__attribute__((always_inline))
vPortSetBASEPRI (uint32_t ulNewMaskValue)
{
  <bb 2> :
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue : "memory");
  return;

}


__attribute__((always_inline))
ulPortRaiseBASEPRI ()
{
  uint32_t ulNewBASEPRI;
  uint32_t ulOriginalBASEPRI;
  uint32_t D.6938;

  <bb 2> :
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI, "=r" ulNewBASEPRI : "i" 16 : "memory");
  D.6938 = ulOriginalBASEPRI;

  <bb 3> :
<L0>:
  return D.6938;

}


__attribute__((always_inline))
vPortRaiseBASEPRI ()
{
  uint32_t ulNewBASEPRI;

  <bb 2> :
  __asm__ __volatile__("	mov %0, %1												
	msr basepri, %0											
	isb														
	dsb														
" : "=r" ulNewBASEPRI : "i" 16 : "memory");
  return;

}