BLE/Debug_FLASH/FreeRTOS/Source/tasks.c.016i.visibility

Marking local functions: prvAddCurrentTaskToDelayedList prvWriteNameToBuffer prvResetNextTaskUnblockTime prvDeleteTCB prvTaskCheckFreeStackSpace prvListTasksWithinSingleList prvCheckTasksWaitingTermination prvInitialiseTaskLists prvSearchForNameWithinSingleList prvTaskIsTaskSuspended prvAddNewTaskToReadyList prvInitialiseNewTask vPortSetBASEPRI ulPortRaiseBASEPRI vPortRaiseBASEPRI


Marking externally visible functions: ulTaskGenericNotifyValueClear xTaskGenericNotifyStateClear vTaskGenericNotifyGiveFromISR xTaskGenericNotifyFromISR xTaskGenericNotify xTaskGenericNotifyWait ulTaskGenericNotifyTake pvTaskIncrementMutexHeldCount uxTaskResetEventItemValue vTaskList vTaskPriorityDisinheritAfterTimeout xTaskPriorityDisinherit xTaskPriorityInherit xTaskGetSchedulerState xTaskGetCurrentTaskHandle uxTaskGetStackHighWaterMark vTaskGetInfo vTaskSetTaskNumber uxTaskGetTaskNumber vTaskMissedYield xTaskCheckForTimeOut vTaskInternalSetTimeOutState vTaskSetTimeOutState vTaskRemoveFromUnorderedEventList xTaskRemoveFromEventList vTaskPlaceOnEventListRestricted vTaskPlaceOnUnorderedEventList vTaskPlaceOnEventList vTaskSwitchContext xTaskIncrementTick xTaskAbortDelay xTaskCatchUpTicks uxTaskGetSystemState xTaskGetHandle pcTaskGetName uxTaskGetNumberOfTasks xTaskGetTickCountFromISR xTaskGetTickCount xTaskResumeAll vTaskSuspendAll vTaskEndScheduler vTaskStartScheduler xTaskResumeFromISR vTaskResume vTaskSuspend vTaskPrioritySet uxTaskPriorityGetFromISR uxTaskPriorityGet eTaskGetState vTaskDelay xTaskDelayUntil vTaskDelete xTaskCreate


Marking externally visible variables: uxTopUsedPriority pxCurrentTCB


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

strcpy/112 (strcpy) @06243000
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: prvWriteNameToBuffer/83 
  Calls: 
sprintf/111 (sprintf) @06221ee0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskList/84 
  Calls: 
strlen/110 (strlen) @061c69a0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: prvWriteNameToBuffer/83 vTaskList/84 xTaskGetHandle/52 
  Calls: 
vPortEndScheduler/109 (vPortEndScheduler) @061c6000
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskEndScheduler/44 
  Calls: 
xPortStartScheduler/108 (xPortStartScheduler) @0260ac40
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskStartScheduler/43 
  Calls: 
xTimerCreateTimerTask/107 (xTimerCreateTimerTask) @0260ab60
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskStartScheduler/43 
  Calls: 
vPortValidateInterruptPriority/106 (vPortValidateInterruptPriority) @025f3e00
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskGenericNotifyGiveFromISR/91 xTaskGenericNotifyFromISR/90 xTaskGetTickCountFromISR/48 xTaskResumeFromISR/42 uxTaskPriorityGetFromISR/37 
  Calls: 
vListInsert/105 (vListInsert) @025f37e0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskPlaceOnEventList/58 prvAddCurrentTaskToDelayedList/94 prvAddCurrentTaskToDelayedList/94 
  Calls: 
vListInsertEnd/104 (vListInsertEnd) @025f30e0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: xTaskResumeFromISR/42 vTaskSuspend/39 vTaskDelete/32 
  Calls: 
uxListRemove/103 (uxListRemove) @025f3000
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskPriorityDisinheritAfterTimeout/82 xTaskPriorityDisinherit/81 xTaskPriorityInherit/80 xTaskAbortDelay/55 xTaskAbortDelay/55 prvCheckTasksWaitingTermination/71 xTaskResumeFromISR/42 vTaskResume/41 vTaskSuspend/39 vTaskSuspend/39 vTaskPrioritySet/38 prvAddCurrentTaskToDelayedList/94 vTaskDelete/32 vTaskDelete/32 
  Calls: 
vListInitialise/102 (vListInitialise) @061a6ee0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: prvInitialiseTaskLists/70 prvInitialiseTaskLists/70 prvInitialiseTaskLists/70 prvInitialiseTaskLists/70 prvInitialiseTaskLists/70 prvInitialiseTaskLists/70 
  Calls: 
vPortExitCritical/101 (vPortExitCritical) @061a6d20
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: ulTaskGenericNotifyValueClear/93 xTaskGenericNotifyStateClear/92 xTaskGenericNotify/89 xTaskGenericNotifyWait/88 xTaskGenericNotifyWait/88 ulTaskGenericNotifyTake/87 ulTaskGenericNotifyTake/87 xTaskCheckForTimeOut/65 vTaskSetTimeOutState/63 xTaskAbortDelay/55 xTaskResumeAll/46 prvCheckTasksWaitingTermination/71 vTaskResume/41 vTaskSuspend/39 vTaskSuspend/39 vTaskPrioritySet/38 uxTaskPriorityGet/36 eTaskGetState/35 vTaskDelete/32 prvAddNewTaskToReadyList/31 
  Calls: 
vPortEnterCritical/100 (vPortEnterCritical) @061a6b60
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: ulTaskGenericNotifyValueClear/93 xTaskGenericNotifyStateClear/92 xTaskGenericNotify/89 xTaskGenericNotifyWait/88 xTaskGenericNotifyWait/88 ulTaskGenericNotifyTake/87 ulTaskGenericNotifyTake/87 xTaskCheckForTimeOut/65 vTaskSetTimeOutState/63 xTaskAbortDelay/55 xTaskResumeAll/46 prvCheckTasksWaitingTermination/71 vTaskResume/41 vTaskSuspend/39 vTaskSuspend/39 vTaskPrioritySet/38 uxTaskPriorityGet/36 eTaskGetState/35 vTaskDelete/32 prvAddNewTaskToReadyList/31 
  Calls: 
pxPortInitialiseStack/99 (pxPortInitialiseStack) @061a68c0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: prvInitialiseNewTask/30 
  Calls: 
vListInitialiseItem/98 (vListInitialiseItem) @061a67e0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: prvInitialiseNewTask/30 prvInitialiseNewTask/30 
  Calls: 
memset/97 (memset) @061a6700
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: prvInitialiseNewTask/30 prvInitialiseNewTask/30 prvInitialiseNewTask/30 
  Calls: 
vPortFree/96 (vPortFree) @061a6540
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskList/84 prvDeleteTCB/76 prvDeleteTCB/76 xTaskCreate/29 
  Calls: 
pvPortMalloc/95 (pvPortMalloc) @061a6460
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskList/84 xTaskCreate/29 xTaskCreate/29 
  Calls: 
prvAddCurrentTaskToDelayedList/94 (prvAddCurrentTaskToDelayedList) @061a6000
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: xTickCount/18 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)xSuspendedTaskList/16 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)xSuspendedTaskList/16 (addr)xSuspendedTaskList/16 (read)xSuspendedTaskList/16 (write)pxCurrentTCB/7 (read)pxOverflowDelayedTaskList/12 (read)pxCurrentTCB/7 (read)pxDelayedTaskList/11 (read)pxCurrentTCB/7 (read)xNextTaskUnblockTime/25 (read)xNextTaskUnblockTime/25 (write)
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: xTaskGenericNotifyWait/88 ulTaskGenericNotifyTake/87 vTaskPlaceOnEventListRestricted/60 vTaskPlaceOnUnorderedEventList/59 vTaskPlaceOnEventList/58 vTaskDelay/34 xTaskDelayUntil/33 
  Calls: vListInsert/105 vListInsert/105 uxListRemove/103 
ulTaskGenericNotifyValueClear/93 (ulTaskGenericNotifyValueClear) @0616c540
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortExitCritical/101 vPortEnterCritical/100 
xTaskGenericNotifyStateClear/92 (xTaskGenericNotifyStateClear) @0616cd20
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortExitCritical/101 vPortEnterCritical/100 vPortRaiseBASEPRI/1 
vTaskGenericNotifyGiveFromISR/91 (vTaskGenericNotifyGiveFromISR) @0616c8c0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)xPendingReadyList/13 (read)xPendingReadyList/13 (addr)xPendingReadyList/13 (read)xPendingReadyList/13 (write)pxCurrentTCB/7 (read)xYieldPending/22 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortSetBASEPRI/3 vPortRaiseBASEPRI/1 ulPortRaiseBASEPRI/2 vPortValidateInterruptPriority/106 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xTaskGenericNotifyFromISR/90 (xTaskGenericNotifyFromISR) @0616c460
  Type: function definition analyzed
  Visibility: externally_visible public
  References: xTickCount/18 (read)uxSchedulerSuspended/28 (read)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)xPendingReadyList/13 (read)xPendingReadyList/13 (addr)xPendingReadyList/13 (read)xPendingReadyList/13 (write)pxCurrentTCB/7 (read)xYieldPending/22 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortSetBASEPRI/3 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 ulPortRaiseBASEPRI/2 vPortValidateInterruptPriority/106 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xTaskGenericNotify/89 (xTaskGenericNotify) @0615ee00
  Type: function definition analyzed
  Visibility: externally_visible public
  References: xTickCount/18 (read)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortExitCritical/101 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 vPortEnterCritical/100 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xTaskGenericNotifyWait/88 (xTaskGenericNotifyWait) @0615ed20
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortExitCritical/101 vPortEnterCritical/100 vPortExitCritical/101 prvAddCurrentTaskToDelayedList/94 vPortEnterCritical/100 vPortRaiseBASEPRI/1 
ulTaskGenericNotifyTake/87 (ulTaskGenericNotifyTake) @0615e8c0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortExitCritical/101 vPortEnterCritical/100 vPortExitCritical/101 prvAddCurrentTaskToDelayedList/94 vPortEnterCritical/100 vPortRaiseBASEPRI/1 
pvTaskIncrementMutexHeldCount/86 (pvTaskIncrementMutexHeldCount) @0615e460
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
uxTaskResetEventItemValue/85 (uxTaskResetEventItemValue) @0615e1c0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
vTaskList/84 (vTaskList) @0613fc40
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxCurrentNumberOfTasks/17 (read)uxCurrentNumberOfTasks/17 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortFree/96 strlen/110 sprintf/111 prvWriteNameToBuffer/83 uxTaskGetSystemState/53 pvPortMalloc/95 
prvWriteNameToBuffer/83 (prvWriteNameToBuffer) @0613f540
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: vTaskList/84 
  Calls: strlen/110 strcpy/112 
vTaskPriorityDisinheritAfterTimeout/82 (vTaskPriorityDisinheritAfterTimeout) @0613f000
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)pxReadyTasksLists/8 (addr)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: uxListRemove/103 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xTaskPriorityDisinherit/81 (xTaskPriorityDisinherit) @0613fb60
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: uxListRemove/103 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xTaskPriorityInherit/80 (xTaskPriorityInherit) @0613f700
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxReadyTasksLists/8 (addr)pxCurrentTCB/7 (read)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: uxListRemove/103 
xTaskGetSchedulerState/79 (xTaskGetSchedulerState) @0613f460
  Type: function definition analyzed
  Visibility: externally_visible public
  References: xSchedulerRunning/20 (read)uxSchedulerSuspended/28 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
xTaskGetCurrentTaskHandle/78 (xTaskGetCurrentTaskHandle) @0613f1c0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
prvResetNextTaskUnblockTime/77 (prvResetNextTaskUnblockTime) @06133c40
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: pxDelayedTaskList/11 (read)xNextTaskUnblockTime/25 (write)pxDelayedTaskList/11 (read)xNextTaskUnblockTime/25 (write)
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: xTaskIncrementTick/56 xTaskResumeAll/46 vTaskSuspend/39 vTaskDelete/32 
  Calls: 
prvDeleteTCB/76 (prvDeleteTCB) @06133380
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: prvCheckTasksWaitingTermination/71 vTaskDelete/32 
  Calls: vPortFree/96 vPortFree/96 
uxTaskGetStackHighWaterMark/75 (uxTaskGetStackHighWaterMark) @06133ee0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: prvTaskCheckFreeStackSpace/74 
prvTaskCheckFreeStackSpace/74 (prvTaskCheckFreeStackSpace) @06133b60
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: uxTaskGetStackHighWaterMark/75 vTaskGetInfo/72 
  Calls: 
prvListTasksWithinSingleList/73 (prvListTasksWithinSingleList) @061338c0
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: uxTaskGetSystemState/53 uxTaskGetSystemState/53 uxTaskGetSystemState/53 uxTaskGetSystemState/53 uxTaskGetSystemState/53 
  Calls: vTaskGetInfo/72 
vTaskGetInfo/72 (vTaskGetInfo) @06133620
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: prvListTasksWithinSingleList/73 
  Calls: prvTaskCheckFreeStackSpace/74 eTaskGetState/35 xTaskResumeAll/46 vTaskSuspendAll/45 
prvCheckTasksWaitingTermination/71 (prvCheckTasksWaitingTermination) @061332a0
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: xTasksWaitingTermination/14 (read)uxCurrentNumberOfTasks/17 (read)uxCurrentNumberOfTasks/17 (write)uxDeletedTasksWaitingCleanUp/15 (read)uxDeletedTasksWaitingCleanUp/15 (write)uxDeletedTasksWaitingCleanUp/15 (read)
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: prvIdleTask/69 
  Calls: prvDeleteTCB/76 vPortExitCritical/101 uxListRemove/103 vPortEnterCritical/100 
prvInitialiseTaskLists/70 (prvInitialiseTaskLists) @0612fee0
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: pxReadyTasksLists/8 (addr)xDelayedTaskList1/9 (addr)xDelayedTaskList2/10 (addr)xPendingReadyList/13 (addr)xTasksWaitingTermination/14 (addr)xSuspendedTaskList/16 (addr)pxDelayedTaskList/11 (write)xDelayedTaskList1/9 (addr)pxOverflowDelayedTaskList/12 (write)xDelayedTaskList2/10 (addr)
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: prvAddNewTaskToReadyList/31 
  Calls: vListInitialise/102 vListInitialise/102 vListInitialise/102 vListInitialise/102 vListInitialise/102 vListInitialise/102 
prvIdleTask/69 (prvIdleTask) @0612f9a0
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  Address is taken.
  References: pxReadyTasksLists/8 (read)
  Referring: vTaskStartScheduler/43 (addr)
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: prvCheckTasksWaitingTermination/71 
vTaskSetTaskNumber/68 (vTaskSetTaskNumber) @0612fe00
  Type: function definition analyzed
  Visibility: externally_visible public
  References: 
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
uxTaskGetTaskNumber/67 (uxTaskGetTaskNumber) @0612fb60
  Type: function definition analyzed
  Visibility: externally_visible public
  References: 
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
vTaskMissedYield/66 (vTaskMissedYield) @0612f8c0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: xYieldPending/22 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
xTaskCheckForTimeOut/65 (xTaskCheckForTimeOut) @0612f620
  Type: function definition analyzed
  Visibility: externally_visible public
  References: xTickCount/18 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)xNumOfOverflows/23 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortExitCritical/101 vTaskInternalSetTimeOutState/64 vPortEnterCritical/100 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
vTaskInternalSetTimeOutState/64 (vTaskInternalSetTimeOutState) @0612f1c0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: xNumOfOverflows/23 (read)xTickCount/18 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: xTaskCheckForTimeOut/65 
  Calls: 
vTaskSetTimeOutState/63 (vTaskSetTimeOutState) @06092b60
  Type: function definition analyzed
  Visibility: externally_visible public
  References: xNumOfOverflows/23 (read)xTickCount/18 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortExitCritical/101 vPortEnterCritical/100 vPortRaiseBASEPRI/1 
vTaskRemoveFromUnorderedEventList/62 (vTaskRemoveFromUnorderedEventList) @06092ee0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)pxCurrentTCB/7 (read)xYieldPending/22 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
xTaskRemoveFromEventList/61 (xTaskRemoveFromEventList) @06092a80
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)xPendingReadyList/13 (read)xPendingReadyList/13 (addr)xPendingReadyList/13 (read)xPendingReadyList/13 (write)pxCurrentTCB/7 (read)xYieldPending/22 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortRaiseBASEPRI/1 
vTaskPlaceOnEventListRestricted/60 (vTaskPlaceOnEventListRestricted) @06092620
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: prvAddCurrentTaskToDelayedList/94 vPortRaiseBASEPRI/1 
vTaskPlaceOnUnorderedEventList/59 (vTaskPlaceOnUnorderedEventList) @060922a0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: prvAddCurrentTaskToDelayedList/94 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
vTaskPlaceOnEventList/58 (vTaskPlaceOnEventList) @06082a80
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: prvAddCurrentTaskToDelayedList/94 vListInsert/105 vPortRaiseBASEPRI/1 
vTaskSwitchContext/57 (vTaskSwitchContext) @06082e00
  Type: function definition analyzed
  Visibility: force_output externally_visible public
  References: uxSchedulerSuspended/28 (read)xYieldPending/22 (write)xYieldPending/22 (write)uxTopReadyPriority/19 (read)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxCurrentTCB/7 (write)uxTopReadyPriority/19 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: vTaskSuspend/39 
  Calls: vPortRaiseBASEPRI/1 
xTaskIncrementTick/56 (xTaskIncrementTick) @060829a0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)xTickCount/18 (read)xTickCount/18 (write)pxDelayedTaskList/11 (read)pxDelayedTaskList/11 (read)pxOverflowDelayedTaskList/12 (read)pxDelayedTaskList/11 (write)pxOverflowDelayedTaskList/12 (write)xNumOfOverflows/23 (read)xNumOfOverflows/23 (write)xNextTaskUnblockTime/25 (read)pxDelayedTaskList/11 (read)xNextTaskUnblockTime/25 (write)pxDelayedTaskList/11 (read)xNextTaskUnblockTime/25 (write)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxReadyTasksLists/8 (read)xYieldPending/22 (read)xPendedTicks/21 (read)xPendedTicks/21 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: xTaskResumeAll/46 
  Calls: prvResetNextTaskUnblockTime/77 vPortRaiseBASEPRI/1 
xTaskAbortDelay/55 (xTaskAbortDelay) @06082380
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)pxCurrentTCB/7 (read)xYieldPending/22 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: xTaskResumeAll/46 vPortExitCritical/101 uxListRemove/103 vPortEnterCritical/100 uxListRemove/103 eTaskGetState/35 vTaskSuspendAll/45 vPortRaiseBASEPRI/1 
xTaskCatchUpTicks/54 (xTaskCatchUpTicks) @06082000
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)xPendedTicks/21 (read)xPendedTicks/21 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: xTaskResumeAll/46 vTaskSuspendAll/45 vPortRaiseBASEPRI/1 
uxTaskGetSystemState/53 (uxTaskGetSystemState) @060777e0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxCurrentNumberOfTasks/17 (read)pxReadyTasksLists/8 (addr)pxDelayedTaskList/11 (read)pxOverflowDelayedTaskList/12 (read)xTasksWaitingTermination/14 (addr)xSuspendedTaskList/16 (addr)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: vTaskList/84 
  Calls: xTaskResumeAll/46 prvListTasksWithinSingleList/73 prvListTasksWithinSingleList/73 prvListTasksWithinSingleList/73 prvListTasksWithinSingleList/73 prvListTasksWithinSingleList/73 vTaskSuspendAll/45 
xTaskGetHandle/52 (xTaskGetHandle) @060772a0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxReadyTasksLists/8 (addr)pxDelayedTaskList/11 (read)pxOverflowDelayedTaskList/12 (read)xSuspendedTaskList/16 (addr)xTasksWaitingTermination/14 (addr)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: xTaskResumeAll/46 prvSearchForNameWithinSingleList/51 prvSearchForNameWithinSingleList/51 prvSearchForNameWithinSingleList/51 prvSearchForNameWithinSingleList/51 prvSearchForNameWithinSingleList/51 vTaskSuspendAll/45 vPortRaiseBASEPRI/1 strlen/110 
prvSearchForNameWithinSingleList/51 (prvSearchForNameWithinSingleList) @06077e00
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: xTaskGetHandle/52 xTaskGetHandle/52 xTaskGetHandle/52 xTaskGetHandle/52 xTaskGetHandle/52 
  Calls: 
pcTaskGetName/50 (pcTaskGetName) @06077b60
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortRaiseBASEPRI/1 
uxTaskGetNumberOfTasks/49 (uxTaskGetNumberOfTasks) @06077700
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxCurrentNumberOfTasks/17 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
xTaskGetTickCountFromISR/48 (xTaskGetTickCountFromISR) @06077460
  Type: function definition analyzed
  Visibility: externally_visible public
  References: xTickCount/18 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortValidateInterruptPriority/106 
xTaskGetTickCount/47 (xTaskGetTickCount) @060771c0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: xTickCount/18 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
xTaskResumeAll/46 (xTaskResumeAll) @06060e00
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)uxSchedulerSuspended/28 (read)uxSchedulerSuspended/28 (write)uxSchedulerSuspended/28 (read)uxCurrentNumberOfTasks/17 (read)xPendingReadyList/13 (read)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)pxCurrentTCB/7 (read)xYieldPending/22 (write)xPendingReadyList/13 (read)xPendedTicks/21 (read)xYieldPending/22 (write)xPendedTicks/21 (write)xYieldPending/22 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: vTaskGetInfo/72 xTaskAbortDelay/55 xTaskCatchUpTicks/54 uxTaskGetSystemState/53 xTaskGetHandle/52 vTaskDelay/34 xTaskDelayUntil/33 
  Calls: vPortExitCritical/101 xTaskIncrementTick/56 prvResetNextTaskUnblockTime/77 vPortEnterCritical/100 vPortRaiseBASEPRI/1 
vTaskSuspendAll/45 (vTaskSuspendAll) @06060d20
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)uxSchedulerSuspended/28 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: vTaskGetInfo/72 xTaskAbortDelay/55 xTaskCatchUpTicks/54 uxTaskGetSystemState/53 xTaskGetHandle/52 vTaskDelay/34 xTaskDelayUntil/33 
  Calls: 
vTaskEndScheduler/44 (vTaskEndScheduler) @06060a80
  Type: function definition analyzed
  Visibility: externally_visible public
  References: xSchedulerRunning/20 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortEndScheduler/109 vPortRaiseBASEPRI/1 
vTaskStartScheduler/43 (vTaskStartScheduler) @060607e0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: prvIdleTask/69 (addr)xIdleTaskHandle/26 (addr)xNextTaskUnblockTime/25 (write)xSchedulerRunning/20 (write)xTickCount/18 (write)uxTopUsedPriority/27 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortRaiseBASEPRI/1 xPortStartScheduler/108 vPortRaiseBASEPRI/1 xTimerCreateTimerTask/107 xTaskCreate/29 
xTaskResumeFromISR/42 (xTaskResumeFromISR) @06060540
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)pxCurrentTCB/7 (read)xYieldPending/22 (write)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)xPendingReadyList/13 (addr)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortSetBASEPRI/3 vListInsertEnd/104 uxListRemove/103 prvTaskIsTaskSuspended/40 ulPortRaiseBASEPRI/2 vPortValidateInterruptPriority/106 vPortRaiseBASEPRI/1 
vTaskResume/41 (vTaskResume) @060601c0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortExitCritical/101 uxListRemove/103 prvTaskIsTaskSuspended/40 vPortEnterCritical/100 vPortRaiseBASEPRI/1 
prvTaskIsTaskSuspended/40 (prvTaskIsTaskSuspended) @060529a0
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: xSuspendedTaskList/16 (addr)xPendingReadyList/13 (addr)
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: xTaskResumeFromISR/42 vTaskResume/41 
  Calls: vPortRaiseBASEPRI/1 
vTaskSuspend/39 (vTaskSuspend) @06052e00
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)xSuspendedTaskList/16 (addr)xSchedulerRunning/20 (read)pxCurrentTCB/7 (read)xSchedulerRunning/20 (read)uxSchedulerSuspended/28 (read)xSuspendedTaskList/16 (read)uxCurrentNumberOfTasks/17 (read)pxCurrentTCB/7 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vTaskSwitchContext/57 vPortRaiseBASEPRI/1 vPortExitCritical/101 prvResetNextTaskUnblockTime/77 vPortEnterCritical/100 vPortExitCritical/101 vListInsertEnd/104 uxListRemove/103 uxListRemove/103 vPortEnterCritical/100 
vTaskPrioritySet/38 (vTaskPrioritySet) @060528c0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (read)pxReadyTasksLists/8 (addr)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortExitCritical/101 uxListRemove/103 vPortEnterCritical/100 vPortRaiseBASEPRI/1 
uxTaskPriorityGetFromISR/37 (uxTaskPriorityGetFromISR) @06052380
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortSetBASEPRI/3 ulPortRaiseBASEPRI/2 vPortValidateInterruptPriority/106 
uxTaskPriorityGet/36 (uxTaskPriorityGet) @06052000
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortExitCritical/101 vPortEnterCritical/100 
eTaskGetState/35 (eTaskGetState) @0603d2a0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)pxDelayedTaskList/11 (read)pxOverflowDelayedTaskList/12 (read)xSuspendedTaskList/16 (addr)xTasksWaitingTermination/14 (addr)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: vTaskGetInfo/72 xTaskAbortDelay/55 
  Calls: vPortExitCritical/101 vPortEnterCritical/100 vPortRaiseBASEPRI/1 
vTaskDelay/34 (vTaskDelay) @0603dc40
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: xTaskResumeAll/46 prvAddCurrentTaskToDelayedList/94 vTaskSuspendAll/45 vPortRaiseBASEPRI/1 
xTaskDelayUntil/33 (xTaskDelayUntil) @0603d7e0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: uxSchedulerSuspended/28 (read)xTickCount/18 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: xTaskResumeAll/46 prvAddCurrentTaskToDelayedList/94 vTaskSuspendAll/45 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 
vTaskDelete/32 (vTaskDelete) @0603d1c0
  Type: function definition analyzed
  Visibility: externally_visible public
  References: pxCurrentTCB/7 (read)uxTaskNumber/24 (read)uxTaskNumber/24 (write)pxCurrentTCB/7 (read)xTasksWaitingTermination/14 (addr)uxDeletedTasksWaitingCleanUp/15 (read)uxDeletedTasksWaitingCleanUp/15 (write)uxCurrentNumberOfTasks/17 (read)uxCurrentNumberOfTasks/17 (write)xSchedulerRunning/20 (read)pxCurrentTCB/7 (read)uxSchedulerSuspended/28 (read)
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: vPortRaiseBASEPRI/1 vPortExitCritical/101 prvResetNextTaskUnblockTime/77 prvDeleteTCB/76 vListInsertEnd/104 uxListRemove/103 uxListRemove/103 vPortEnterCritical/100 
prvAddNewTaskToReadyList/31 (prvAddNewTaskToReadyList) @0602b540
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: uxCurrentNumberOfTasks/17 (read)uxCurrentNumberOfTasks/17 (write)pxCurrentTCB/7 (read)pxCurrentTCB/7 (write)uxCurrentNumberOfTasks/17 (read)xSchedulerRunning/20 (read)pxCurrentTCB/7 (read)pxCurrentTCB/7 (write)uxTaskNumber/24 (read)uxTaskNumber/24 (write)uxTaskNumber/24 (read)uxTopReadyPriority/19 (read)uxTopReadyPriority/19 (write)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (addr)pxReadyTasksLists/8 (read)pxReadyTasksLists/8 (write)xSchedulerRunning/20 (read)pxCurrentTCB/7 (read)
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: xTaskCreate/29 
  Calls: vPortExitCritical/101 prvInitialiseTaskLists/70 vPortEnterCritical/100 
prvInitialiseNewTask/30 (prvInitialiseNewTask) @0602bc40
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: xTaskCreate/29 
  Calls: pxPortInitialiseStack/99 memset/97 memset/97 vListInitialiseItem/98 vListInitialiseItem/98 vPortRaiseBASEPRI/1 vPortRaiseBASEPRI/1 memset/97 
xTaskCreate/29 (xTaskCreate) @0602b700
  Type: function definition analyzed
  Visibility: externally_visible public
  References: 
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: vTaskStartScheduler/43 
  Calls: prvAddNewTaskToReadyList/31 prvInitialiseNewTask/30 vPortFree/96 pvPortMalloc/95 pvPortMalloc/95 
uxSchedulerSuspended/28 (uxSchedulerSuspended) @060235a0
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: vTaskDelete/32 (read)xTaskDelayUntil/33 (read)vTaskDelay/34 (read)vTaskSuspend/39 (read)xTaskResumeFromISR/42 (read)vTaskSuspendAll/45 (read)vTaskSuspendAll/45 (write)xTaskResumeAll/46 (read)xTaskResumeAll/46 (read)xTaskResumeAll/46 (write)xTaskResumeAll/46 (read)xTaskCatchUpTicks/54 (read)xTaskIncrementTick/56 (read)vTaskSwitchContext/57 (read)vTaskPlaceOnUnorderedEventList/59 (read)xTaskRemoveFromEventList/61 (read)vTaskRemoveFromUnorderedEventList/62 (read)xTaskGetSchedulerState/79 (read)xTaskGenericNotifyFromISR/90 (read)vTaskGenericNotifyGiveFromISR/91 (read)
  Availability: available
  Varpool flags: initialized
uxTopUsedPriority/27 (uxTopUsedPriority) @06023510
  Type: variable definition analyzed
  Visibility: force_output externally_visible public
  References: 
  Referring: vTaskStartScheduler/43 (read)
  Availability: available
  Varpool flags: initialized read-only
xIdleTaskHandle/26 (xIdleTaskHandle) @06023480
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: vTaskStartScheduler/43 (addr)
  Availability: available
  Varpool flags: initialized
xNextTaskUnblockTime/25 (xNextTaskUnblockTime) @060233f0
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: prvResetNextTaskUnblockTime/77 (write)prvResetNextTaskUnblockTime/77 (write)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (write)vTaskStartScheduler/43 (write)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (write)xTaskIncrementTick/56 (write)
  Availability: available
  Varpool flags: initialized
uxTaskNumber/24 (uxTaskNumber) @06023360
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: prvAddNewTaskToReadyList/31 (read)prvAddNewTaskToReadyList/31 (write)prvAddNewTaskToReadyList/31 (read)vTaskDelete/32 (read)vTaskDelete/32 (write)
  Availability: available
  Varpool flags: initialized
xNumOfOverflows/23 (xNumOfOverflows) @06023318
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (write)vTaskSetTimeOutState/63 (read)vTaskInternalSetTimeOutState/64 (read)xTaskCheckForTimeOut/65 (read)
  Availability: available
  Varpool flags: initialized
xYieldPending/22 (xYieldPending) @060232d0
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: xTaskResumeFromISR/42 (write)xTaskResumeAll/46 (write)xTaskResumeAll/46 (write)xTaskResumeAll/46 (read)xTaskAbortDelay/55 (write)xTaskIncrementTick/56 (read)vTaskSwitchContext/57 (write)vTaskSwitchContext/57 (write)xTaskRemoveFromEventList/61 (write)vTaskRemoveFromUnorderedEventList/62 (write)vTaskMissedYield/66 (write)xTaskGenericNotifyFromISR/90 (write)vTaskGenericNotifyGiveFromISR/91 (write)
  Availability: available
  Varpool flags: initialized
xPendedTicks/21 (xPendedTicks) @06023240
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: xTaskResumeAll/46 (read)xTaskResumeAll/46 (write)xTaskCatchUpTicks/54 (read)xTaskCatchUpTicks/54 (write)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (write)
  Availability: available
  Varpool flags: initialized
xSchedulerRunning/20 (xSchedulerRunning) @060231b0
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: prvAddNewTaskToReadyList/31 (read)prvAddNewTaskToReadyList/31 (read)vTaskDelete/32 (read)vTaskSuspend/39 (read)vTaskSuspend/39 (read)vTaskStartScheduler/43 (write)vTaskEndScheduler/44 (write)xTaskGetSchedulerState/79 (read)
  Availability: available
  Varpool flags: initialized
uxTopReadyPriority/19 (uxTopReadyPriority) @06023120
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: prvAddNewTaskToReadyList/31 (read)prvAddNewTaskToReadyList/31 (write)vTaskPrioritySet/38 (read)vTaskPrioritySet/38 (write)vTaskResume/41 (read)vTaskResume/41 (write)xTaskResumeFromISR/42 (read)xTaskResumeFromISR/42 (write)xTaskResumeAll/46 (read)xTaskResumeAll/46 (write)xTaskAbortDelay/55 (read)xTaskAbortDelay/55 (write)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (write)vTaskSwitchContext/57 (read)vTaskSwitchContext/57 (write)xTaskRemoveFromEventList/61 (read)xTaskRemoveFromEventList/61 (write)vTaskRemoveFromUnorderedEventList/62 (read)vTaskRemoveFromUnorderedEventList/62 (write)xTaskPriorityInherit/80 (read)xTaskPriorityInherit/80 (write)xTaskPriorityDisinherit/81 (read)xTaskPriorityDisinherit/81 (write)vTaskPriorityDisinheritAfterTimeout/82 (read)vTaskPriorityDisinheritAfterTimeout/82 (write)xTaskGenericNotify/89 (read)xTaskGenericNotify/89 (write)xTaskGenericNotifyFromISR/90 (read)xTaskGenericNotifyFromISR/90 (write)vTaskGenericNotifyGiveFromISR/91 (read)vTaskGenericNotifyGiveFromISR/91 (write)
  Availability: available
  Varpool flags: initialized
xTickCount/18 (xTickCount) @060230d8
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: xTaskDelayUntil/33 (read)prvAddCurrentTaskToDelayedList/94 (read)vTaskStartScheduler/43 (write)xTaskGetTickCount/47 (read)xTaskGetTickCountFromISR/48 (read)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (write)vTaskSetTimeOutState/63 (read)vTaskInternalSetTimeOutState/64 (read)xTaskCheckForTimeOut/65 (read)xTaskGenericNotify/89 (read)xTaskGenericNotifyFromISR/90 (read)
  Availability: available
  Varpool flags: initialized
uxCurrentNumberOfTasks/17 (uxCurrentNumberOfTasks) @06023090
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: prvAddNewTaskToReadyList/31 (read)prvAddNewTaskToReadyList/31 (write)prvAddNewTaskToReadyList/31 (read)vTaskDelete/32 (read)vTaskDelete/32 (write)vTaskSuspend/39 (read)prvCheckTasksWaitingTermination/71 (read)prvCheckTasksWaitingTermination/71 (write)xTaskResumeAll/46 (read)uxTaskGetNumberOfTasks/49 (read)uxTaskGetSystemState/53 (read)vTaskList/84 (read)vTaskList/84 (read)
  Availability: available
  Varpool flags: initialized
xSuspendedTaskList/16 (xSuspendedTaskList) @0601ff78
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: prvInitialiseTaskLists/70 (addr)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (addr)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (write)eTaskGetState/35 (addr)vTaskSuspend/39 (addr)vTaskSuspend/39 (read)prvTaskIsTaskSuspended/40 (addr)xTaskGetHandle/52 (addr)uxTaskGetSystemState/53 (addr)
  Availability: available
  Varpool flags:
uxDeletedTasksWaitingCleanUp/15 (uxDeletedTasksWaitingCleanUp) @0601fee8
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: vTaskDelete/32 (read)vTaskDelete/32 (write)prvCheckTasksWaitingTermination/71 (read)prvCheckTasksWaitingTermination/71 (write)prvCheckTasksWaitingTermination/71 (read)
  Availability: available
  Varpool flags: initialized
xTasksWaitingTermination/14 (xTasksWaitingTermination) @0601fe58
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: prvInitialiseTaskLists/70 (addr)vTaskDelete/32 (addr)eTaskGetState/35 (addr)prvCheckTasksWaitingTermination/71 (read)xTaskGetHandle/52 (addr)uxTaskGetSystemState/53 (addr)
  Availability: available
  Varpool flags:
xPendingReadyList/13 (xPendingReadyList) @0601fdc8
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: prvInitialiseTaskLists/70 (addr)prvTaskIsTaskSuspended/40 (addr)xTaskResumeFromISR/42 (addr)xTaskResumeAll/46 (read)xTaskResumeAll/46 (read)xTaskRemoveFromEventList/61 (read)xTaskRemoveFromEventList/61 (addr)xTaskRemoveFromEventList/61 (read)xTaskRemoveFromEventList/61 (write)xTaskGenericNotifyFromISR/90 (read)xTaskGenericNotifyFromISR/90 (addr)xTaskGenericNotifyFromISR/90 (read)xTaskGenericNotifyFromISR/90 (write)vTaskGenericNotifyGiveFromISR/91 (read)vTaskGenericNotifyGiveFromISR/91 (addr)vTaskGenericNotifyGiveFromISR/91 (read)vTaskGenericNotifyGiveFromISR/91 (write)
  Availability: available
  Varpool flags:
pxOverflowDelayedTaskList/12 (pxOverflowDelayedTaskList) @0601fd38
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: prvInitialiseTaskLists/70 (write)prvAddCurrentTaskToDelayedList/94 (read)eTaskGetState/35 (read)xTaskGetHandle/52 (read)uxTaskGetSystemState/53 (read)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (write)
  Availability: available
  Varpool flags:
pxDelayedTaskList/11 (pxDelayedTaskList) @0601fcf0
  Type: variable definition analyzed
  Visibility: force_output prevailing_def_ironly
  References: 
  Referring: prvInitialiseTaskLists/70 (write)prvResetNextTaskUnblockTime/77 (read)prvResetNextTaskUnblockTime/77 (read)prvAddCurrentTaskToDelayedList/94 (read)eTaskGetState/35 (read)xTaskGetHandle/52 (read)uxTaskGetSystemState/53 (read)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (write)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (read)
  Availability: available
  Varpool flags:
xDelayedTaskList2/10 (xDelayedTaskList2) @0601fca8
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: prvInitialiseTaskLists/70 (addr)prvInitialiseTaskLists/70 (addr)
  Availability: available
  Varpool flags:
xDelayedTaskList1/9 (xDelayedTaskList1) @0601fc18
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: prvInitialiseTaskLists/70 (addr)prvInitialiseTaskLists/70 (addr)
  Availability: available
  Varpool flags:
pxReadyTasksLists/8 (pxReadyTasksLists) @0601fb88
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: prvAddNewTaskToReadyList/31 (read)prvAddNewTaskToReadyList/31 (addr)prvAddNewTaskToReadyList/31 (read)prvAddNewTaskToReadyList/31 (write)prvInitialiseTaskLists/70 (addr)vTaskPrioritySet/38 (addr)vTaskPrioritySet/38 (read)vTaskPrioritySet/38 (addr)vTaskPrioritySet/38 (read)vTaskPrioritySet/38 (write)vTaskResume/41 (read)vTaskResume/41 (addr)vTaskResume/41 (read)vTaskResume/41 (write)xTaskResumeFromISR/42 (read)xTaskResumeFromISR/42 (addr)xTaskResumeFromISR/42 (read)xTaskResumeFromISR/42 (write)prvIdleTask/69 (read)xTaskResumeAll/46 (read)xTaskResumeAll/46 (addr)xTaskResumeAll/46 (read)xTaskResumeAll/46 (write)xTaskGetHandle/52 (addr)uxTaskGetSystemState/53 (addr)xTaskAbortDelay/55 (read)xTaskAbortDelay/55 (addr)xTaskAbortDelay/55 (read)xTaskAbortDelay/55 (write)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (addr)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (write)xTaskIncrementTick/56 (read)vTaskSwitchContext/57 (read)vTaskSwitchContext/57 (addr)xTaskRemoveFromEventList/61 (read)xTaskRemoveFromEventList/61 (addr)xTaskRemoveFromEventList/61 (read)xTaskRemoveFromEventList/61 (write)vTaskRemoveFromUnorderedEventList/62 (read)vTaskRemoveFromUnorderedEventList/62 (addr)vTaskRemoveFromUnorderedEventList/62 (read)vTaskRemoveFromUnorderedEventList/62 (write)xTaskPriorityInherit/80 (addr)xTaskPriorityInherit/80 (read)xTaskPriorityInherit/80 (addr)xTaskPriorityInherit/80 (read)xTaskPriorityInherit/80 (write)xTaskPriorityDisinherit/81 (read)xTaskPriorityDisinherit/81 (addr)xTaskPriorityDisinherit/81 (read)xTaskPriorityDisinherit/81 (write)vTaskPriorityDisinheritAfterTimeout/82 (addr)vTaskPriorityDisinheritAfterTimeout/82 (read)vTaskPriorityDisinheritAfterTimeout/82 (addr)vTaskPriorityDisinheritAfterTimeout/82 (read)vTaskPriorityDisinheritAfterTimeout/82 (write)xTaskGenericNotify/89 (read)xTaskGenericNotify/89 (addr)xTaskGenericNotify/89 (read)xTaskGenericNotify/89 (write)xTaskGenericNotifyFromISR/90 (read)xTaskGenericNotifyFromISR/90 (addr)xTaskGenericNotifyFromISR/90 (read)xTaskGenericNotifyFromISR/90 (write)vTaskGenericNotifyGiveFromISR/91 (read)vTaskGenericNotifyGiveFromISR/91 (addr)vTaskGenericNotifyGiveFromISR/91 (read)vTaskGenericNotifyGiveFromISR/91 (write)
  Availability: available
  Varpool flags:
pxCurrentTCB/7 (pxCurrentTCB) @0601fb40
  Type: variable definition analyzed
  Visibility: force_output externally_visible public
  References: 
  Referring: prvAddNewTaskToReadyList/31 (read)prvAddNewTaskToReadyList/31 (write)prvAddNewTaskToReadyList/31 (read)prvAddNewTaskToReadyList/31 (write)prvAddNewTaskToReadyList/31 (read)vTaskDelete/32 (read)vTaskDelete/32 (read)vTaskDelete/32 (read)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (read)prvAddCurrentTaskToDelayedList/94 (read)eTaskGetState/35 (read)uxTaskPriorityGet/36 (read)uxTaskPriorityGetFromISR/37 (read)vTaskPrioritySet/38 (read)vTaskPrioritySet/38 (read)vTaskPrioritySet/38 (read)vTaskPrioritySet/38 (read)vTaskSuspend/39 (read)vTaskSuspend/39 (read)vTaskSuspend/39 (write)vTaskResume/41 (read)vTaskResume/41 (read)xTaskResumeFromISR/42 (read)xTaskResumeAll/46 (read)pcTaskGetName/50 (read)xTaskAbortDelay/55 (read)xTaskIncrementTick/56 (read)xTaskIncrementTick/56 (read)vTaskSwitchContext/57 (write)vTaskPlaceOnEventList/58 (read)vTaskPlaceOnUnorderedEventList/59 (read)vTaskPlaceOnUnorderedEventList/59 (read)vTaskPlaceOnUnorderedEventList/59 (read)vTaskPlaceOnUnorderedEventList/59 (read)vTaskPlaceOnUnorderedEventList/59 (read)vTaskPlaceOnUnorderedEventList/59 (read)vTaskPlaceOnEventListRestricted/60 (read)vTaskPlaceOnEventListRestricted/60 (read)vTaskPlaceOnEventListRestricted/60 (read)vTaskPlaceOnEventListRestricted/60 (read)vTaskPlaceOnEventListRestricted/60 (read)xTaskRemoveFromEventList/61 (read)vTaskRemoveFromUnorderedEventList/62 (read)xTaskCheckForTimeOut/65 (read)xTaskCheckForTimeOut/65 (read)vTaskGetInfo/72 (read)vTaskGetInfo/72 (read)uxTaskGetStackHighWaterMark/75 (read)xTaskGetCurrentTaskHandle/78 (read)xTaskPriorityInherit/80 (read)xTaskPriorityInherit/80 (read)xTaskPriorityInherit/80 (read)xTaskPriorityInherit/80 (read)xTaskPriorityInherit/80 (read)xTaskPriorityDisinherit/81 (read)vTaskPriorityDisinheritAfterTimeout/82 (read)uxTaskResetEventItemValue/85 (read)uxTaskResetEventItemValue/85 (read)uxTaskResetEventItemValue/85 (read)pvTaskIncrementMutexHeldCount/86 (read)pvTaskIncrementMutexHeldCount/86 (read)pvTaskIncrementMutexHeldCount/86 (read)ulTaskGenericNotifyTake/87 (read)ulTaskGenericNotifyTake/87 (read)ulTaskGenericNotifyTake/87 (read)ulTaskGenericNotifyTake/87 (read)ulTaskGenericNotifyTake/87 (read)ulTaskGenericNotifyTake/87 (read)xTaskGenericNotifyWait/88 (read)xTaskGenericNotifyWait/88 (read)xTaskGenericNotifyWait/88 (read)xTaskGenericNotifyWait/88 (read)xTaskGenericNotifyWait/88 (read)xTaskGenericNotifyWait/88 (read)xTaskGenericNotifyWait/88 (read)xTaskGenericNotify/89 (read)xTaskGenericNotifyFromISR/90 (read)vTaskGenericNotifyGiveFromISR/91 (read)xTaskGenericNotifyStateClear/92 (read)ulTaskGenericNotifyValueClear/93 (read)
  Availability: available
  Varpool flags: initialized
vPortSetBASEPRI/3 (vPortSetBASEPRI) @05f48b60
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: vTaskGenericNotifyGiveFromISR/91 xTaskGenericNotifyFromISR/90 xTaskResumeFromISR/42 uxTaskPriorityGetFromISR/37 
  Calls: 
ulPortRaiseBASEPRI/2 (ulPortRaiseBASEPRI) @05f488c0
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: vTaskGenericNotifyGiveFromISR/91 xTaskGenericNotifyFromISR/90 xTaskResumeFromISR/42 uxTaskPriorityGetFromISR/37 
  Calls: 
vPortRaiseBASEPRI/1 (vPortRaiseBASEPRI) @05f48540
  Type: function definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: 
  Availability: local
  Function flags: body local optimize_size
  Called by: xTaskGenericNotifyStateClear/92 vTaskGenericNotifyGiveFromISR/91 vTaskGenericNotifyGiveFromISR/91 vTaskGenericNotifyGiveFromISR/91 xTaskGenericNotifyFromISR/90 xTaskGenericNotifyFromISR/90 xTaskGenericNotifyFromISR/90 xTaskGenericNotifyFromISR/90 xTaskGenericNotify/89 xTaskGenericNotify/89 xTaskGenericNotify/89 xTaskGenericNotify/89 xTaskGenericNotifyWait/88 ulTaskGenericNotifyTake/87 vTaskPriorityDisinheritAfterTimeout/82 vTaskPriorityDisinheritAfterTimeout/82 xTaskPriorityDisinherit/81 xTaskPriorityDisinherit/81 xTaskCheckForTimeOut/65 xTaskCheckForTimeOut/65 vTaskSetTimeOutState/63 vTaskRemoveFromUnorderedEventList/62 vTaskRemoveFromUnorderedEventList/62 xTaskRemoveFromEventList/61 vTaskPlaceOnEventListRestricted/60 vTaskPlaceOnUnorderedEventList/59 vTaskPlaceOnUnorderedEventList/59 vTaskPlaceOnEventList/58 vTaskSwitchContext/57 xTaskIncrementTick/56 xTaskAbortDelay/55 xTaskCatchUpTicks/54 xTaskGetHandle/52 pcTaskGetName/50 xTaskResumeAll/46 vTaskEndScheduler/44 vTaskStartScheduler/43 vTaskStartScheduler/43 xTaskResumeFromISR/42 prvTaskIsTaskSuspended/40 vTaskResume/41 vTaskSuspend/39 vTaskPrioritySet/38 eTaskGetState/35 vTaskDelay/34 xTaskDelayUntil/33 xTaskDelayUntil/33 xTaskDelayUntil/33 vTaskDelete/32 prvInitialiseNewTask/30 prvInitialiseNewTask/30 
  Calls: 
prvAddCurrentTaskToDelayedList (TickType_t xTicksToWait, const BaseType_t xCanBlockIndefinitely)
{
  struct ListItem_t * const pxIndex;
  const TickType_t xConstTickCount;
  TickType_t xTimeToWake;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xConstTickCount = xTickCount;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.23_1 = pxCurrentTCB;
  pxCurrentTCB.23_1->ucDelayAborted = 0;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.24_2 = pxCurrentTCB;
  _3 = &pxCurrentTCB.24_2->xStateListItem;
  _4 = uxListRemove (_3);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTicksToWait == 4294967295)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  if (xCanBlockIndefinitely != 0)
    goto <bb 4>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  pxIndex = xSuspendedTaskList.pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.25_5 = pxCurrentTCB;
  pxCurrentTCB.25_5->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.26_6 = pxCurrentTCB;
  _7 = pxIndex->pxPrevious;
  pxCurrentTCB.26_6->xStateListItem.pxPrevious = _7;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.27_8 = pxCurrentTCB;
  _9 = pxIndex->pxPrevious;
  _10 = &pxCurrentTCB.27_8->xStateListItem;
  _9->pxNext = _10;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.28_11 = pxCurrentTCB;
  _12 = &pxCurrentTCB.28_11->xStateListItem;
  pxIndex->pxPrevious = _12;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.29_13 = pxCurrentTCB;
  pxCurrentTCB.29_13->xStateListItem.pvContainer = &xSuspendedTaskList;
  # DEBUG BEGIN_STMT
  _14 = xSuspendedTaskList.uxNumberOfItems;
  _15 = _14 + 1;
  xSuspendedTaskList.uxNumberOfItems = _15;
  # DEBUG BEGIN_STMT
  goto <bb 9>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  xTimeToWake = xConstTickCount + xTicksToWait;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.30_16 = pxCurrentTCB;
  pxCurrentTCB.30_16->xStateListItem.xItemValue = xTimeToWake;
  # DEBUG BEGIN_STMT
  if (xTimeToWake < xConstTickCount)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxOverflowDelayedTaskList.31_17 = pxOverflowDelayedTaskList;
  pxCurrentTCB.32_18 = pxCurrentTCB;
  _19 = &pxCurrentTCB.32_18->xStateListItem;
  vListInsert (pxOverflowDelayedTaskList.31_17, _19);
  goto <bb 9>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  pxDelayedTaskList.33_20 = pxDelayedTaskList;
  pxCurrentTCB.34_21 = pxCurrentTCB;
  _22 = &pxCurrentTCB.34_21->xStateListItem;
  vListInsert (pxDelayedTaskList.33_20, _22);
  # DEBUG BEGIN_STMT
  xNextTaskUnblockTime.35_23 = xNextTaskUnblockTime;
  if (xTimeToWake < xNextTaskUnblockTime.35_23)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  xNextTaskUnblockTime = xTimeToWake;

  <bb 9> :
  # DEBUG BEGIN_STMT
  return;

}


ulTaskGenericNotifyValueClear (struct tskTaskControlBlock * xTask, UBaseType_t uxIndexToClear, uint32_t ulBitsToClear)
{
  uint32_t ulReturn;
  struct TCB_t * pxTCB;
  uint32_t D.8233;
  struct TCB_t * iftmp.164;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTask == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  iftmp.164 = pxCurrentTCB;
  goto <bb 5>; [INV]

  <bb 4> :
  iftmp.164 = xTask;

  <bb 5> :
  pxTCB = iftmp.164;
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  ulReturn = pxTCB->ulNotifiedValue[uxIndexToClear];
  # DEBUG BEGIN_STMT
  _1 = pxTCB->ulNotifiedValue[uxIndexToClear];
  _2 = ~ulBitsToClear;
  _3 = _1 & _2;
  pxTCB->ulNotifiedValue[uxIndexToClear] = _3;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  D.8233 = ulReturn;
  return D.8233;

}


xTaskGenericNotifyStateClear (struct tskTaskControlBlock * xTask, UBaseType_t uxIndexToClear)
{
  BaseType_t xReturn;
  struct TCB_t * pxTCB;
  BaseType_t D.8227;
  struct TCB_t * iftmp.163;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (uxIndexToClear != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTask == 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  iftmp.163 = pxCurrentTCB;
  goto <bb 8>; [INV]

  <bb 7> :
  iftmp.163 = xTask;

  <bb 8> :
  pxTCB = iftmp.163;
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _1 = pxTCB->ucNotifyState[uxIndexToClear];
  if (_1 == 2)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxTCB->ucNotifyState[uxIndexToClear] = 0;
  # DEBUG BEGIN_STMT
  xReturn = 1;
  goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  xReturn = 0;

  <bb 11> :
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  D.8227 = xReturn;
  return D.8227;

}


vTaskGenericNotifyGiveFromISR (struct tskTaskControlBlock * xTaskToNotify, UBaseType_t uxIndexToNotify, BaseType_t * pxHigherPriorityTaskWoken)
{
  struct ListItem_t * const pxIndex;
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  UBaseType_t uxSavedInterruptStatus;
  uint8_t ucOriginalNotifyState;
  struct TCB_t * pxTCB;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTaskToNotify == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (uxIndexToNotify != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 7>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  pxTCB = xTaskToNotify;
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  # DEBUG BEGIN_STMT
  ucOriginalNotifyState = pxTCB->ucNotifyState[uxIndexToNotify];
  # DEBUG BEGIN_STMT
  pxTCB->ucNotifyState[uxIndexToNotify] = 2;
  # DEBUG BEGIN_STMT
  _1 = pxTCB->ulNotifiedValue[uxIndexToNotify];
  _2 = _1 + 1;
  pxTCB->ulNotifiedValue[uxIndexToNotify] = _2;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (ucOriginalNotifyState == 1)
    goto <bb 9>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  _3 = pxTCB->xEventListItem.pvContainer;
  if (_3 != 0B)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 11> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 11>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.160_4 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.160_4 == 0)
    goto <bb 13>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  pxList = pxTCB->xStateListItem.pvContainer;
  # DEBUG BEGIN_STMT
  _5 = pxTCB->xStateListItem.pxNext;
  _6 = pxTCB->xStateListItem.pxPrevious;
  _5->pxPrevious = _6;
  # DEBUG BEGIN_STMT
  _7 = pxTCB->xStateListItem.pxPrevious;
  _8 = pxTCB->xStateListItem.pxNext;
  _7->pxNext = _8;
  # DEBUG BEGIN_STMT
  _9 = pxList->pxIndex;
  _10 = &pxTCB->xStateListItem;
  if (_9 == _10)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  _11 = pxTCB->xStateListItem.pxPrevious;
  pxList->pxIndex = _11;

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _12 = pxList->uxNumberOfItems;
  _13 = _12 + 4294967295;
  pxList->uxNumberOfItems = _13;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _14 = pxTCB->uxPriority;
  uxTopReadyPriority.161_15 = uxTopReadyPriority;
  if (_14 > uxTopReadyPriority.161_15)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  _16 = pxTCB->uxPriority;
  uxTopReadyPriority = _16;

  <bb 17> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _17 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_17].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _18 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _18;
  # DEBUG BEGIN_STMT
  _19 = pxIndex->pxPrevious;
  _20 = &pxTCB->xStateListItem;
  _19->pxNext = _20;
  # DEBUG BEGIN_STMT
  _21 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _21;
  # DEBUG BEGIN_STMT
  _22 = pxTCB->uxPriority;
  _23 = &pxReadyTasksLists[_22];
  pxTCB->xStateListItem.pvContainer = _23;
  # DEBUG BEGIN_STMT
  _24 = pxTCB->uxPriority;
  _25 = pxReadyTasksLists[_24].uxNumberOfItems;
  _26 = _25 + 1;
  pxReadyTasksLists[_24].uxNumberOfItems = _26;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 19>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  pxIndex = xPendingReadyList.pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xEventListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _27 = pxIndex->pxPrevious;
  pxTCB->xEventListItem.pxPrevious = _27;
  # DEBUG BEGIN_STMT
  _28 = pxIndex->pxPrevious;
  _29 = &pxTCB->xEventListItem;
  _28->pxNext = _29;
  # DEBUG BEGIN_STMT
  _30 = &pxTCB->xEventListItem;
  pxIndex->pxPrevious = _30;
  # DEBUG BEGIN_STMT
  pxTCB->xEventListItem.pvContainer = &xPendingReadyList;
  # DEBUG BEGIN_STMT
  _31 = xPendingReadyList.uxNumberOfItems;
  _32 = _31 + 1;
  xPendingReadyList.uxNumberOfItems = _32;

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _33 = pxTCB->uxPriority;
  pxCurrentTCB.162_34 = pxCurrentTCB;
  _35 = pxCurrentTCB.162_34->uxPriority;
  if (_33 > _35)
    goto <bb 20>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 20> :
  # DEBUG BEGIN_STMT
  if (pxHigherPriorityTaskWoken != 0B)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  # DEBUG BEGIN_STMT
  *pxHigherPriorityTaskWoken = 1;

  <bb 22> :
  # DEBUG BEGIN_STMT
  xYieldPending = 1;

  <bb 23> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptStatus);
  return;

}


xTaskGenericNotifyFromISR (struct tskTaskControlBlock * xTaskToNotify, UBaseType_t uxIndexToNotify, uint32_t ulValue, eNotifyAction eAction, uint32_t * pulPreviousNotificationValue, BaseType_t * pxHigherPriorityTaskWoken)
{
  struct ListItem_t * const pxIndex;
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  uint8_t ucOriginalNotifyState;
  struct TCB_t * pxTCB;
  BaseType_t D.8195;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xReturn = 1;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTaskToNotify == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (uxIndexToNotify != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 7>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  pxTCB = xTaskToNotify;
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  # DEBUG BEGIN_STMT
  if (pulPreviousNotificationValue != 0B)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  _1 = pxTCB->ulNotifiedValue[uxIndexToNotify];
  *pulPreviousNotificationValue = _1;

  <bb 10> :
  # DEBUG BEGIN_STMT
  ucOriginalNotifyState = pxTCB->ucNotifyState[uxIndexToNotify];
  # DEBUG BEGIN_STMT
  pxTCB->ucNotifyState[uxIndexToNotify] = 2;
  # DEBUG BEGIN_STMT
  switch (eAction) <default: <L16> [INV], case 0: <L39> [INV], case 1: <L8> [INV], case 2: <L9> [INV], case 3: <L10> [INV], case 4: <L11> [INV]>

  <bb 11> :
<L8>:
  # DEBUG BEGIN_STMT
  _2 = pxTCB->ulNotifiedValue[uxIndexToNotify];
  _3 = ulValue | _2;
  pxTCB->ulNotifiedValue[uxIndexToNotify] = _3;
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

  <bb 12> :
<L9>:
  # DEBUG BEGIN_STMT
  _4 = pxTCB->ulNotifiedValue[uxIndexToNotify];
  _5 = _4 + 1;
  pxTCB->ulNotifiedValue[uxIndexToNotify] = _5;
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

  <bb 13> :
<L10>:
  # DEBUG BEGIN_STMT
  pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue;
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

  <bb 14> :
<L11>:
  # DEBUG BEGIN_STMT
  if (ucOriginalNotifyState != 2)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue;
  goto <bb 20>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  xReturn = 0;
  goto <bb 20>; [INV]

  <bb 17> :
<L16>:
  # DEBUG BEGIN_STMT
  xTickCount.156_6 = xTickCount;
  if (xTickCount.156_6 != 0)
    goto <bb 18>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 19>; [INV]

  <bb 20> :
<L39>:
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (ucOriginalNotifyState == 1)
    goto <bb 21>; [INV]
  else
    goto <bb 35>; [INV]

  <bb 21> :
  # DEBUG BEGIN_STMT
  _7 = pxTCB->xEventListItem.pvContainer;
  if (_7 != 0B)
    goto <bb 22>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 22> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 23> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 23>; [INV]

  <bb 24> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.157_8 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.157_8 == 0)
    goto <bb 25>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 25> :
  # DEBUG BEGIN_STMT
  pxList = pxTCB->xStateListItem.pvContainer;
  # DEBUG BEGIN_STMT
  _9 = pxTCB->xStateListItem.pxNext;
  _10 = pxTCB->xStateListItem.pxPrevious;
  _9->pxPrevious = _10;
  # DEBUG BEGIN_STMT
  _11 = pxTCB->xStateListItem.pxPrevious;
  _12 = pxTCB->xStateListItem.pxNext;
  _11->pxNext = _12;
  # DEBUG BEGIN_STMT
  _13 = pxList->pxIndex;
  _14 = &pxTCB->xStateListItem;
  if (_13 == _14)
    goto <bb 26>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 26> :
  # DEBUG BEGIN_STMT
  _15 = pxTCB->xStateListItem.pxPrevious;
  pxList->pxIndex = _15;

  <bb 27> :
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _16 = pxList->uxNumberOfItems;
  _17 = _16 + 4294967295;
  pxList->uxNumberOfItems = _17;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _18 = pxTCB->uxPriority;
  uxTopReadyPriority.158_19 = uxTopReadyPriority;
  if (_18 > uxTopReadyPriority.158_19)
    goto <bb 28>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 28> :
  # DEBUG BEGIN_STMT
  _20 = pxTCB->uxPriority;
  uxTopReadyPriority = _20;

  <bb 29> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _21 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_21].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _22 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _22;
  # DEBUG BEGIN_STMT
  _23 = pxIndex->pxPrevious;
  _24 = &pxTCB->xStateListItem;
  _23->pxNext = _24;
  # DEBUG BEGIN_STMT
  _25 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _25;
  # DEBUG BEGIN_STMT
  _26 = pxTCB->uxPriority;
  _27 = &pxReadyTasksLists[_26];
  pxTCB->xStateListItem.pvContainer = _27;
  # DEBUG BEGIN_STMT
  _28 = pxTCB->uxPriority;
  _29 = pxReadyTasksLists[_28].uxNumberOfItems;
  _30 = _29 + 1;
  pxReadyTasksLists[_28].uxNumberOfItems = _30;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 31>; [INV]

  <bb 30> :
  # DEBUG BEGIN_STMT
  pxIndex = xPendingReadyList.pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xEventListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _31 = pxIndex->pxPrevious;
  pxTCB->xEventListItem.pxPrevious = _31;
  # DEBUG BEGIN_STMT
  _32 = pxIndex->pxPrevious;
  _33 = &pxTCB->xEventListItem;
  _32->pxNext = _33;
  # DEBUG BEGIN_STMT
  _34 = &pxTCB->xEventListItem;
  pxIndex->pxPrevious = _34;
  # DEBUG BEGIN_STMT
  pxTCB->xEventListItem.pvContainer = &xPendingReadyList;
  # DEBUG BEGIN_STMT
  _35 = xPendingReadyList.uxNumberOfItems;
  _36 = _35 + 1;
  xPendingReadyList.uxNumberOfItems = _36;

  <bb 31> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _37 = pxTCB->uxPriority;
  pxCurrentTCB.159_38 = pxCurrentTCB;
  _39 = pxCurrentTCB.159_38->uxPriority;
  if (_37 > _39)
    goto <bb 32>; [INV]
  else
    goto <bb 35>; [INV]

  <bb 32> :
  # DEBUG BEGIN_STMT
  if (pxHigherPriorityTaskWoken != 0B)
    goto <bb 33>; [INV]
  else
    goto <bb 34>; [INV]

  <bb 33> :
  # DEBUG BEGIN_STMT
  *pxHigherPriorityTaskWoken = 1;

  <bb 34> :
  # DEBUG BEGIN_STMT
  xYieldPending = 1;

  <bb 35> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptStatus);
  # DEBUG BEGIN_STMT
  D.8195 = xReturn;
  return D.8195;

}


xTaskGenericNotify (struct tskTaskControlBlock * xTaskToNotify, UBaseType_t uxIndexToNotify, uint32_t ulValue, eNotifyAction eAction, uint32_t * pulPreviousNotificationValue)
{
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  uint8_t ucOriginalNotifyState;
  BaseType_t xReturn;
  struct TCB_t * pxTCB;
  BaseType_t D.8165;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xReturn = 1;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (uxIndexToNotify != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTaskToNotify == 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 7>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB = xTaskToNotify;
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  if (pulPreviousNotificationValue != 0B)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  _1 = pxTCB->ulNotifiedValue[uxIndexToNotify];
  *pulPreviousNotificationValue = _1;

  <bb 10> :
  # DEBUG BEGIN_STMT
  ucOriginalNotifyState = pxTCB->ucNotifyState[uxIndexToNotify];
  # DEBUG BEGIN_STMT
  pxTCB->ucNotifyState[uxIndexToNotify] = 2;
  # DEBUG BEGIN_STMT
  switch (eAction) <default: <L16> [INV], case 0: <L35> [INV], case 1: <L8> [INV], case 2: <L9> [INV], case 3: <L10> [INV], case 4: <L11> [INV]>

  <bb 11> :
<L8>:
  # DEBUG BEGIN_STMT
  _2 = pxTCB->ulNotifiedValue[uxIndexToNotify];
  _3 = ulValue | _2;
  pxTCB->ulNotifiedValue[uxIndexToNotify] = _3;
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

  <bb 12> :
<L9>:
  # DEBUG BEGIN_STMT
  _4 = pxTCB->ulNotifiedValue[uxIndexToNotify];
  _5 = _4 + 1;
  pxTCB->ulNotifiedValue[uxIndexToNotify] = _5;
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

  <bb 13> :
<L10>:
  # DEBUG BEGIN_STMT
  pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue;
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

  <bb 14> :
<L11>:
  # DEBUG BEGIN_STMT
  if (ucOriginalNotifyState != 2)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue;
  goto <bb 20>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  xReturn = 0;
  goto <bb 20>; [INV]

  <bb 17> :
<L16>:
  # DEBUG BEGIN_STMT
  xTickCount.153_6 = xTickCount;
  if (xTickCount.153_6 != 0)
    goto <bb 18>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 19>; [INV]

  <bb 20> :
<L35>:
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (ucOriginalNotifyState == 1)
    goto <bb 21>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 21> :
  # DEBUG BEGIN_STMT
  pxList = pxTCB->xStateListItem.pvContainer;
  # DEBUG BEGIN_STMT
  _7 = pxTCB->xStateListItem.pxNext;
  _8 = pxTCB->xStateListItem.pxPrevious;
  _7->pxPrevious = _8;
  # DEBUG BEGIN_STMT
  _9 = pxTCB->xStateListItem.pxPrevious;
  _10 = pxTCB->xStateListItem.pxNext;
  _9->pxNext = _10;
  # DEBUG BEGIN_STMT
  _11 = pxList->pxIndex;
  _12 = &pxTCB->xStateListItem;
  if (_11 == _12)
    goto <bb 22>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 22> :
  # DEBUG BEGIN_STMT
  _13 = pxTCB->xStateListItem.pxPrevious;
  pxList->pxIndex = _13;

  <bb 23> :
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _14 = pxList->uxNumberOfItems;
  _15 = _14 + 4294967295;
  pxList->uxNumberOfItems = _15;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _16 = pxTCB->uxPriority;
  uxTopReadyPriority.154_17 = uxTopReadyPriority;
  if (_16 > uxTopReadyPriority.154_17)
    goto <bb 24>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 24> :
  # DEBUG BEGIN_STMT
  _18 = pxTCB->uxPriority;
  uxTopReadyPriority = _18;

  <bb 25> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _19 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_19].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _20 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _20;
  # DEBUG BEGIN_STMT
  _21 = pxIndex->pxPrevious;
  _22 = &pxTCB->xStateListItem;
  _21->pxNext = _22;
  # DEBUG BEGIN_STMT
  _23 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _23;
  # DEBUG BEGIN_STMT
  _24 = pxTCB->uxPriority;
  _25 = &pxReadyTasksLists[_24];
  pxTCB->xStateListItem.pvContainer = _25;
  # DEBUG BEGIN_STMT
  _26 = pxTCB->uxPriority;
  _27 = pxReadyTasksLists[_26].uxNumberOfItems;
  _28 = _27 + 1;
  pxReadyTasksLists[_26].uxNumberOfItems = _28;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _29 = pxTCB->xEventListItem.pvContainer;
  if (_29 != 0B)
    goto <bb 26>; [INV]
  else
    goto <bb 28>; [INV]

  <bb 26> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 27> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 27>; [INV]

  <bb 28> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _30 = pxTCB->uxPriority;
  pxCurrentTCB.155_31 = pxCurrentTCB;
  _32 = pxCurrentTCB.155_31->uxPriority;
  if (_30 > _32)
    goto <bb 29>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 29> :
  # DEBUG BEGIN_STMT
  _33 = 3758157060B;
  *_33 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT

  <bb 30> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  D.8165 = xReturn;
  return D.8165;

}


xTaskGenericNotifyWait (UBaseType_t uxIndexToWait, uint32_t ulBitsToClearOnEntry, uint32_t ulBitsToClearOnExit, uint32_t * pulNotificationValue, TickType_t xTicksToWait)
{
  BaseType_t xReturn;
  BaseType_t D.8140;
  struct TCB_t * pxCurrentTCB.151;
  struct TCB_t * pxCurrentTCB.147;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (uxIndexToWait != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  pxCurrentTCB.146_1 = pxCurrentTCB;
  _2 = pxCurrentTCB.146_1->ucNotifyState[uxIndexToWait];
  if (_2 != 2)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.147 = pxCurrentTCB;
  _3 = pxCurrentTCB.147->ulNotifiedValue[uxIndexToWait];
  _4 = ~ulBitsToClearOnEntry;
  _5 = _3 & _4;
  pxCurrentTCB.147->ulNotifiedValue[uxIndexToWait] = _5;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.148_6 = pxCurrentTCB;
  pxCurrentTCB.148_6->ucNotifyState[uxIndexToWait] = 1;
  # DEBUG BEGIN_STMT
  if (xTicksToWait != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  prvAddCurrentTaskToDelayedList (xTicksToWait, 1);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _7 = 3758157060B;
  *_7 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (pulNotificationValue != 0B)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.149_8 = pxCurrentTCB;
  _9 = pxCurrentTCB.149_8->ulNotifiedValue[uxIndexToWait];
  *pulNotificationValue = _9;

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.150_10 = pxCurrentTCB;
  _11 = pxCurrentTCB.150_10->ucNotifyState[uxIndexToWait];
  if (_11 != 2)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  xReturn = 0;
  goto <bb 13>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.151 = pxCurrentTCB;
  _12 = pxCurrentTCB.151->ulNotifiedValue[uxIndexToWait];
  _13 = ~ulBitsToClearOnExit;
  _14 = _12 & _13;
  pxCurrentTCB.151->ulNotifiedValue[uxIndexToWait] = _14;
  # DEBUG BEGIN_STMT
  xReturn = 1;

  <bb 13> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.152_15 = pxCurrentTCB;
  pxCurrentTCB.152_15->ucNotifyState[uxIndexToWait] = 0;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  D.8140 = xReturn;
  return D.8140;

}


ulTaskGenericNotifyTake (UBaseType_t uxIndexToWait, BaseType_t xClearCountOnExit, TickType_t xTicksToWait)
{
  uint32_t ulReturn;
  uint32_t D.8123;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (uxIndexToWait != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  pxCurrentTCB.140_1 = pxCurrentTCB;
  _2 = pxCurrentTCB.140_1->ulNotifiedValue[uxIndexToWait];
  if (_2 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.141_3 = pxCurrentTCB;
  pxCurrentTCB.141_3->ucNotifyState[uxIndexToWait] = 1;
  # DEBUG BEGIN_STMT
  if (xTicksToWait != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  prvAddCurrentTaskToDelayedList (xTicksToWait, 1);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _4 = 3758157060B;
  *_4 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.142_5 = pxCurrentTCB;
  ulReturn = pxCurrentTCB.142_5->ulNotifiedValue[uxIndexToWait];
  # DEBUG BEGIN_STMT
  if (ulReturn != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  if (xClearCountOnExit != 0)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.143_6 = pxCurrentTCB;
  pxCurrentTCB.143_6->ulNotifiedValue[uxIndexToWait] = 0;
  goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.144_7 = pxCurrentTCB;
  _8 = ulReturn + 4294967295;
  pxCurrentTCB.144_7->ulNotifiedValue[uxIndexToWait] = _8;

  <bb 12> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.145_9 = pxCurrentTCB;
  pxCurrentTCB.145_9->ucNotifyState[uxIndexToWait] = 0;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  D.8123 = ulReturn;
  return D.8123;

}


pvTaskIncrementMutexHeldCount ()
{
  struct tskTaskControlBlock * D.8107;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.138_1 = pxCurrentTCB;
  if (pxCurrentTCB.138_1 != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.139_2 = pxCurrentTCB;
  _3 = pxCurrentTCB.139_2->uxMutexesHeld;
  _4 = _3 + 1;
  pxCurrentTCB.139_2->uxMutexesHeld = _4;

  <bb 4> :
  # DEBUG BEGIN_STMT
  D.8107 = pxCurrentTCB;
  return D.8107;

}


uxTaskResetEventItemValue ()
{
  TickType_t uxReturn;
  TickType_t D.8103;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.135_1 = pxCurrentTCB;
  uxReturn = pxCurrentTCB.135_1->xEventListItem.xItemValue;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.136_2 = pxCurrentTCB;
  _3 = pxCurrentTCB.136_2->uxPriority;
  pxCurrentTCB.137_4 = pxCurrentTCB;
  _5 = 5 - _3;
  pxCurrentTCB.137_4->xEventListItem.xItemValue = _5;
  # DEBUG BEGIN_STMT
  D.8103 = uxReturn;
  return D.8103;

}


vTaskList (char * pcWriteBuffer)
{
  char cStatus;
  UBaseType_t x;
  UBaseType_t uxArraySize;
  struct TaskStatus_t * pxTaskStatusArray;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  *pcWriteBuffer = 0;
  # DEBUG BEGIN_STMT
  uxArraySize = uxCurrentNumberOfTasks;
  # DEBUG BEGIN_STMT
  uxCurrentNumberOfTasks.134_1 = uxCurrentNumberOfTasks;
  _2 = uxCurrentNumberOfTasks.134_1 * 36;
  pxTaskStatusArray = pvPortMalloc (_2);
  # DEBUG BEGIN_STMT
  if (pxTaskStatusArray != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  uxArraySize = uxTaskGetSystemState (pxTaskStatusArray, uxArraySize, 0B);
  # DEBUG BEGIN_STMT
  x = 0;
  goto <bb 12>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  _3 = x * 36;
  _4 = pxTaskStatusArray + _3;
  _5 = _4->eCurrentState;
  switch (_5) <default: <L7> [INV], case 0: <L2> [INV], case 1: <L3> [INV], case 2: <L4> [INV], case 3: <L5> [INV], case 4: <L6> [INV]>

  <bb 5> :
<L2>:
  # DEBUG BEGIN_STMT
  cStatus = 88;
  # DEBUG BEGIN_STMT
  goto <bb 11>; [INV]

  <bb 6> :
<L3>:
  # DEBUG BEGIN_STMT
  cStatus = 82;
  # DEBUG BEGIN_STMT
  goto <bb 11>; [INV]

  <bb 7> :
<L4>:
  # DEBUG BEGIN_STMT
  cStatus = 66;
  # DEBUG BEGIN_STMT
  goto <bb 11>; [INV]

  <bb 8> :
<L5>:
  # DEBUG BEGIN_STMT
  cStatus = 83;
  # DEBUG BEGIN_STMT
  goto <bb 11>; [INV]

  <bb 9> :
<L6>:
  # DEBUG BEGIN_STMT
  cStatus = 68;
  # DEBUG BEGIN_STMT
  goto <bb 11>; [INV]

  <bb 10> :
<L7>:
  # DEBUG BEGIN_STMT
  cStatus = 0;
  # DEBUG BEGIN_STMT

  <bb 11> :
  # DEBUG BEGIN_STMT
  _6 = x * 36;
  _7 = pxTaskStatusArray + _6;
  _8 = _7->pcTaskName;
  pcWriteBuffer = prvWriteNameToBuffer (pcWriteBuffer, _8);
  # DEBUG BEGIN_STMT
  _9 = (int) cStatus;
  _10 = x * 36;
  _11 = pxTaskStatusArray + _10;
  _12 = _11->uxCurrentPriority;
  _13 = x * 36;
  _14 = pxTaskStatusArray + _13;
  _15 = _14->usStackHighWaterMark;
  _16 = (unsigned int) _15;
  _17 = x * 36;
  _18 = pxTaskStatusArray + _17;
  _19 = _18->xTaskNumber;
  sprintf (pcWriteBuffer, "\t%c\t%u\t%u\t%u\r\n", _9, _12, _16, _19);
  # DEBUG BEGIN_STMT
  _20 = strlen (pcWriteBuffer);
  pcWriteBuffer = pcWriteBuffer + _20;
  # DEBUG BEGIN_STMT
  x = x + 1;

  <bb 12> :
  # DEBUG BEGIN_STMT
  if (x < uxArraySize)
    goto <bb 4>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  vPortFree (pxTaskStatusArray);

  <bb 14> :
  # DEBUG BEGIN_STMT
  return;

}


prvWriteNameToBuffer (char * pcBuffer, const char * pcTaskName)
{
  size_t x;
  char * D.8101;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  strcpy (pcBuffer, pcTaskName);
  # DEBUG BEGIN_STMT
  x = strlen (pcBuffer);
  goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  _1 = pcBuffer + x;
  *_1 = 32;
  # DEBUG BEGIN_STMT
  x = x + 1;

  <bb 4> :
  # DEBUG BEGIN_STMT
  if (x <= 8)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  _2 = pcBuffer + x;
  *_2 = 0;
  # DEBUG BEGIN_STMT
  D.8101 = pcBuffer + x;
  return D.8101;

}


vTaskPriorityDisinheritAfterTimeout (struct tskTaskControlBlock * const pxMutexHolder, UBaseType_t uxHighestPriorityWaitingTask)
{
  struct ListItem_t * const pxIndex;
  const UBaseType_t uxOnlyOneMutexHeld;
  UBaseType_t uxPriorityToUse;
  UBaseType_t uxPriorityUsedOnEntry;
  struct TCB_t * const pxTCB;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxTCB = pxMutexHolder;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxOnlyOneMutexHeld = 1;
  # DEBUG BEGIN_STMT
  if (pxMutexHolder != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  _1 = pxTCB->uxMutexesHeld;
  if (_1 == 0)
    goto <bb 4>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 5>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _2 = pxTCB->uxBasePriority;
  if (uxHighestPriorityWaitingTask > _2)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  uxPriorityToUse = uxHighestPriorityWaitingTask;
  goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  uxPriorityToUse = pxTCB->uxBasePriority;

  <bb 9> :
  # DEBUG BEGIN_STMT
  _3 = pxTCB->uxPriority;
  if (uxPriorityToUse != _3)
    goto <bb 10>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  _4 = pxTCB->uxMutexesHeld;
  if (_4 == 1)
    goto <bb 11>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.132_5 = pxCurrentTCB;
  if (pxTCB == pxCurrentTCB.132_5)
    goto <bb 12>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 13> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 13>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxPriorityUsedOnEntry = pxTCB->uxPriority;
  # DEBUG BEGIN_STMT
  pxTCB->uxPriority = uxPriorityToUse;
  # DEBUG BEGIN_STMT
  _6 = pxTCB->xEventListItem.xItemValue;
  _7 = (signed int) _6;
  if (_7 >= 0)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  _8 = 5 - uxPriorityToUse;
  pxTCB->xEventListItem.xItemValue = _8;

  <bb 16> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _9 = pxTCB->xStateListItem.pvContainer;
  _10 = &pxReadyTasksLists[uxPriorityUsedOnEntry];
  if (_9 == _10)
    goto <bb 17>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  _11 = &pxTCB->xStateListItem;
  _12 = uxListRemove (_11);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _13 = pxTCB->uxPriority;
  uxTopReadyPriority.133_14 = uxTopReadyPriority;
  if (_13 > uxTopReadyPriority.133_14)
    goto <bb 18>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  _15 = pxTCB->uxPriority;
  uxTopReadyPriority = _15;

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _16 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_16].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _17 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _17;
  # DEBUG BEGIN_STMT
  _18 = pxIndex->pxPrevious;
  _19 = &pxTCB->xStateListItem;
  _18->pxNext = _19;
  # DEBUG BEGIN_STMT
  _20 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _20;
  # DEBUG BEGIN_STMT
  _21 = pxTCB->uxPriority;
  _22 = &pxReadyTasksLists[_21];
  pxTCB->xStateListItem.pvContainer = _22;
  # DEBUG BEGIN_STMT
  _23 = pxTCB->uxPriority;
  _24 = pxReadyTasksLists[_23].uxNumberOfItems;
  _25 = _24 + 1;
  pxReadyTasksLists[_23].uxNumberOfItems = _25;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT

  <bb 20> :
  # DEBUG BEGIN_STMT
  return;

}


xTaskPriorityDisinherit (struct tskTaskControlBlock * const pxMutexHolder)
{
  struct ListItem_t * const pxIndex;
  BaseType_t xReturn;
  struct TCB_t * const pxTCB;
  BaseType_t D.8069;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxTCB = pxMutexHolder;
  # DEBUG BEGIN_STMT
  xReturn = 0;
  # DEBUG BEGIN_STMT
  if (pxMutexHolder != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.130_1 = pxCurrentTCB;
  if (pxTCB != pxCurrentTCB.130_1)
    goto <bb 4>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 5>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _2 = pxTCB->uxMutexesHeld;
  if (_2 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 8>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _3 = pxTCB->uxMutexesHeld;
  _4 = _3 + 4294967295;
  pxTCB->uxMutexesHeld = _4;
  # DEBUG BEGIN_STMT
  _5 = pxTCB->uxPriority;
  _6 = pxTCB->uxBasePriority;
  if (_5 != _6)
    goto <bb 10>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  _7 = pxTCB->uxMutexesHeld;
  if (_7 == 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  _8 = &pxTCB->xStateListItem;
  _9 = uxListRemove (_8);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _10 = pxTCB->uxBasePriority;
  pxTCB->uxPriority = _10;
  # DEBUG BEGIN_STMT
  _11 = pxTCB->uxPriority;
  _12 = 5 - _11;
  pxTCB->xEventListItem.xItemValue = _12;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _13 = pxTCB->uxPriority;
  uxTopReadyPriority.131_14 = uxTopReadyPriority;
  if (_13 > uxTopReadyPriority.131_14)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  _15 = pxTCB->uxPriority;
  uxTopReadyPriority = _15;

  <bb 13> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _16 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_16].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _17 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _17;
  # DEBUG BEGIN_STMT
  _18 = pxIndex->pxPrevious;
  _19 = &pxTCB->xStateListItem;
  _18->pxNext = _19;
  # DEBUG BEGIN_STMT
  _20 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _20;
  # DEBUG BEGIN_STMT
  _21 = pxTCB->uxPriority;
  _22 = &pxReadyTasksLists[_21];
  pxTCB->xStateListItem.pvContainer = _22;
  # DEBUG BEGIN_STMT
  _23 = pxTCB->uxPriority;
  _24 = pxReadyTasksLists[_23].uxNumberOfItems;
  _25 = _24 + 1;
  pxReadyTasksLists[_23].uxNumberOfItems = _25;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xReturn = 1;

  <bb 14> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  D.8069 = xReturn;
  return D.8069;

}


xTaskPriorityInherit (struct tskTaskControlBlock * const pxMutexHolder)
{
  struct ListItem_t * const pxIndex;
  BaseType_t xReturn;
  struct TCB_t * const pxMutexHolderTCB;
  BaseType_t D.8049;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxMutexHolderTCB = pxMutexHolder;
  # DEBUG BEGIN_STMT
  xReturn = 0;
  # DEBUG BEGIN_STMT
  if (pxMutexHolder != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  _1 = pxMutexHolderTCB->uxPriority;
  pxCurrentTCB.124_2 = pxCurrentTCB;
  _3 = pxCurrentTCB.124_2->uxPriority;
  if (_1 < _3)
    goto <bb 4>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  _4 = pxMutexHolderTCB->xEventListItem.xItemValue;
  _5 = (signed int) _4;
  if (_5 >= 0)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.125_6 = pxCurrentTCB;
  _7 = pxCurrentTCB.125_6->uxPriority;
  _8 = 5 - _7;
  pxMutexHolderTCB->xEventListItem.xItemValue = _8;

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _9 = pxMutexHolderTCB->xStateListItem.pvContainer;
  _10 = pxMutexHolderTCB->uxPriority;
  _11 = &pxReadyTasksLists[_10];
  if (_9 == _11)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  _12 = &pxMutexHolderTCB->xStateListItem;
  _13 = uxListRemove (_12);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.126_14 = pxCurrentTCB;
  _15 = pxCurrentTCB.126_14->uxPriority;
  pxMutexHolderTCB->uxPriority = _15;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _16 = pxMutexHolderTCB->uxPriority;
  uxTopReadyPriority.127_17 = uxTopReadyPriority;
  if (_16 > uxTopReadyPriority.127_17)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  _18 = pxMutexHolderTCB->uxPriority;
  uxTopReadyPriority = _18;

  <bb 9> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _19 = pxMutexHolderTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_19].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxMutexHolderTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _20 = pxIndex->pxPrevious;
  pxMutexHolderTCB->xStateListItem.pxPrevious = _20;
  # DEBUG BEGIN_STMT
  _21 = pxIndex->pxPrevious;
  _22 = &pxMutexHolderTCB->xStateListItem;
  _21->pxNext = _22;
  # DEBUG BEGIN_STMT
  _23 = &pxMutexHolderTCB->xStateListItem;
  pxIndex->pxPrevious = _23;
  # DEBUG BEGIN_STMT
  _24 = pxMutexHolderTCB->uxPriority;
  _25 = &pxReadyTasksLists[_24];
  pxMutexHolderTCB->xStateListItem.pvContainer = _25;
  # DEBUG BEGIN_STMT
  _26 = pxMutexHolderTCB->uxPriority;
  _27 = pxReadyTasksLists[_26].uxNumberOfItems;
  _28 = _27 + 1;
  pxReadyTasksLists[_26].uxNumberOfItems = _28;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.128_29 = pxCurrentTCB;
  _30 = pxCurrentTCB.128_29->uxPriority;
  pxMutexHolderTCB->uxPriority = _30;

  <bb 11> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xReturn = 1;
  goto <bb 14>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  _31 = pxMutexHolderTCB->uxBasePriority;
  pxCurrentTCB.129_32 = pxCurrentTCB;
  _33 = pxCurrentTCB.129_32->uxPriority;
  if (_31 < _33)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  xReturn = 1;

  <bb 14> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  D.8049 = xReturn;
  return D.8049;

}


xTaskGetSchedulerState ()
{
  BaseType_t xReturn;
  BaseType_t D.8027;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xSchedulerRunning.122_1 = xSchedulerRunning;
  if (xSchedulerRunning.122_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  xReturn = 1;
  goto <bb 7>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.123_2 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.123_2 == 0)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  xReturn = 2;
  goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  xReturn = 0;

  <bb 7> :
  # DEBUG BEGIN_STMT
  D.8027 = xReturn;
  return D.8027;

}


xTaskGetCurrentTaskHandle ()
{
  struct tskTaskControlBlock * xReturn;
  struct tskTaskControlBlock * D.8019;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xReturn = pxCurrentTCB;
  # DEBUG BEGIN_STMT
  D.8019 = xReturn;
  return D.8019;

}


prvResetNextTaskUnblockTime ()
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  pxDelayedTaskList.20_1 = pxDelayedTaskList;
  _2 = pxDelayedTaskList.20_1->uxNumberOfItems;
  if (_2 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  xNextTaskUnblockTime = 4294967295;
  goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  pxDelayedTaskList.21_3 = pxDelayedTaskList;
  _4 = pxDelayedTaskList.21_3->xListEnd.pxNext;
  _5 = _4->xItemValue;
  xNextTaskUnblockTime = _5;

  <bb 5> :
  return;

}


prvDeleteTCB (struct TCB_t * pxTCB)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 = pxTCB->pxStack;
  vPortFree (_1);
  # DEBUG BEGIN_STMT
  vPortFree (pxTCB);
  return;

}


uxTaskGetStackHighWaterMark (struct tskTaskControlBlock * xTask)
{
  UBaseType_t uxReturn;
  uint8_t * pucEndOfStack;
  struct TCB_t * pxTCB;
  UBaseType_t D.8017;
  struct TCB_t * iftmp.121;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTask == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  iftmp.121 = pxCurrentTCB;
  goto <bb 5>; [INV]

  <bb 4> :
  iftmp.121 = xTask;

  <bb 5> :
  pxTCB = iftmp.121;
  # DEBUG BEGIN_STMT
  pucEndOfStack = pxTCB->pxStack;
  # DEBUG BEGIN_STMT
  _1 = prvTaskCheckFreeStackSpace (pucEndOfStack);
  uxReturn = (UBaseType_t) _1;
  # DEBUG BEGIN_STMT
  D.8017 = uxReturn;
  return D.8017;

}


prvTaskCheckFreeStackSpace (const uint8_t * pucStackByte)
{
  uint32_t ulCount;
  uint16_t D.8011;

  <bb 2> :
  # DEBUG BEGIN_STMT
  ulCount = 0;
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pucStackByte = pucStackByte + 1;
  # DEBUG BEGIN_STMT
  ulCount = ulCount + 1;

  <bb 4> :
  # DEBUG BEGIN_STMT
  _1 = *pucStackByte;
  if (_1 == 165)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  ulCount = ulCount / 4;
  # DEBUG BEGIN_STMT
  D.8011 = (uint16_t) ulCount;
  return D.8011;

}


prvListTasksWithinSingleList (struct TaskStatus_t * pxTaskStatusArray, struct List_t * pxList, eTaskState eState)
{
  struct List_t * const pxConstList;
  struct List_t * const pxConstList;
  UBaseType_t uxTask;
  struct TCB_t * pxFirstTCB;
  struct TCB_t * pxNextTCB;
  UBaseType_t D.7866;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxTask = 0;
  # DEBUG BEGIN_STMT
  _1 = pxList->uxNumberOfItems;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxConstList = pxList;
  # DEBUG BEGIN_STMT
  _2 = pxConstList->pxIndex;
  _3 = _2->pxNext;
  pxConstList->pxIndex = _3;
  # DEBUG BEGIN_STMT
  _4 = pxConstList->pxIndex;
  _5 = &pxConstList->xListEnd;
  if (_4 == _5)
    goto <bb 4>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  _6 = pxConstList->pxIndex;
  _7 = _6->pxNext;
  pxConstList->pxIndex = _7;

  <bb 5> :
  # DEBUG BEGIN_STMT
  _8 = pxConstList->pxIndex;
  pxFirstTCB = _8->pvOwner;

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxConstList = pxList;
  # DEBUG BEGIN_STMT
  _9 = pxConstList->pxIndex;
  _10 = _9->pxNext;
  pxConstList->pxIndex = _10;
  # DEBUG BEGIN_STMT
  _11 = pxConstList->pxIndex;
  _12 = &pxConstList->xListEnd;
  if (_11 == _12)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  _13 = pxConstList->pxIndex;
  _14 = _13->pxNext;
  pxConstList->pxIndex = _14;

  <bb 8> :
  # DEBUG BEGIN_STMT
  _15 = pxConstList->pxIndex;
  pxNextTCB = _15->pvOwner;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _16 = uxTask * 36;
  _17 = pxTaskStatusArray + _16;
  vTaskGetInfo (pxNextTCB, _17, 1, eState);
  # DEBUG BEGIN_STMT
  uxTask = uxTask + 1;
  # DEBUG BEGIN_STMT
  if (pxNextTCB != pxFirstTCB)
    goto <bb 6>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  D.7866 = uxTask;
  return D.7866;

}


vTaskGetInfo (struct tskTaskControlBlock * xTask, struct TaskStatus_t * pxTaskStatus, BaseType_t xGetFreeStackSpace, eTaskState eState)
{
  struct TCB_t * pxTCB;
  struct TCB_t * iftmp.119;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTask == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  iftmp.119 = pxCurrentTCB;
  goto <bb 5>; [INV]

  <bb 4> :
  iftmp.119 = xTask;

  <bb 5> :
  pxTCB = iftmp.119;
  # DEBUG BEGIN_STMT
  pxTaskStatus->xHandle = pxTCB;
  # DEBUG BEGIN_STMT
  _1 = &pxTCB->pcTaskName[0];
  pxTaskStatus->pcTaskName = _1;
  # DEBUG BEGIN_STMT
  _2 = pxTCB->uxPriority;
  pxTaskStatus->uxCurrentPriority = _2;
  # DEBUG BEGIN_STMT
  _3 = pxTCB->pxStack;
  pxTaskStatus->pxStackBase = _3;
  # DEBUG BEGIN_STMT
  _4 = pxTCB->uxTCBNumber;
  pxTaskStatus->xTaskNumber = _4;
  # DEBUG BEGIN_STMT
  _5 = pxTCB->uxBasePriority;
  pxTaskStatus->uxBasePriority = _5;
  # DEBUG BEGIN_STMT
  pxTaskStatus->ulRunTimeCounter = 0;
  # DEBUG BEGIN_STMT
  if (eState != 5)
    goto <bb 6>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.120_6 = pxCurrentTCB;
  if (pxTCB == pxCurrentTCB.120_6)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  pxTaskStatus->eCurrentState = 0;
  goto <bb 13>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  pxTaskStatus->eCurrentState = eState;
  # DEBUG BEGIN_STMT
  if (eState == 3)
    goto <bb 9>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  _7 = pxTCB->xEventListItem.pvContainer;
  if (_7 != 0B)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxTaskStatus->eCurrentState = 2;

  <bb 11> :
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  goto <bb 13>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  _8 = eTaskGetState (pxTCB);
  pxTaskStatus->eCurrentState = _8;

  <bb 13> :
  # DEBUG BEGIN_STMT
  if (xGetFreeStackSpace != 0)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  _9 = pxTCB->pxStack;
  _10 = prvTaskCheckFreeStackSpace (_9);
  pxTaskStatus->usStackHighWaterMark = _10;
  goto <bb 16>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxTaskStatus->usStackHighWaterMark = 0;

  <bb 16> :
  return;

}


prvCheckTasksWaitingTermination ()
{
  struct TCB_t * pxTCB;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _1 = xTasksWaitingTermination.xListEnd.pxNext;
  pxTCB = _1->pvOwner;
  # DEBUG BEGIN_STMT
  _2 = &pxTCB->xStateListItem;
  uxListRemove (_2);
  # DEBUG BEGIN_STMT
  uxCurrentNumberOfTasks.58_3 = uxCurrentNumberOfTasks;
  _4 = uxCurrentNumberOfTasks.58_3 + 4294967295;
  uxCurrentNumberOfTasks = _4;
  # DEBUG BEGIN_STMT
  uxDeletedTasksWaitingCleanUp.59_5 = uxDeletedTasksWaitingCleanUp;
  _6 = uxDeletedTasksWaitingCleanUp.59_5 + 4294967295;
  uxDeletedTasksWaitingCleanUp = _6;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  prvDeleteTCB (pxTCB);

  <bb 4> :
  # DEBUG BEGIN_STMT
  uxDeletedTasksWaitingCleanUp.60_7 = uxDeletedTasksWaitingCleanUp;
  if (uxDeletedTasksWaitingCleanUp.60_7 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 5> :
  return;

}


prvInitialiseTaskLists ()
{
  UBaseType_t uxPriority;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxPriority = 0;
  goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  _1 = &pxReadyTasksLists[uxPriority];
  vListInitialise (_1);
  # DEBUG BEGIN_STMT
  uxPriority = uxPriority + 1;

  <bb 4> :
  # DEBUG BEGIN_STMT
  if (uxPriority <= 4)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  vListInitialise (&xDelayedTaskList1);
  # DEBUG BEGIN_STMT
  vListInitialise (&xDelayedTaskList2);
  # DEBUG BEGIN_STMT
  vListInitialise (&xPendingReadyList);
  # DEBUG BEGIN_STMT
  vListInitialise (&xTasksWaitingTermination);
  # DEBUG BEGIN_STMT
  vListInitialise (&xSuspendedTaskList);
  # DEBUG BEGIN_STMT
  pxDelayedTaskList = &xDelayedTaskList1;
  # DEBUG BEGIN_STMT
  pxOverflowDelayedTaskList = &xDelayedTaskList2;
  return;

}


prvIdleTask (void * pvParameters)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  prvCheckTasksWaitingTermination ();
  # DEBUG BEGIN_STMT
  _1 = pxReadyTasksLists[0].uxNumberOfItems;
  if (_1 > 1)
    goto <bb 3>; [INV]
  else
    goto <bb 2>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  _2 = 3758157060B;
  *_2 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT
  goto <bb 2>; [INV]

}


vTaskSetTaskNumber (struct tskTaskControlBlock * xTask, const UBaseType_t uxHandle)
{
  struct TCB_t * pxTCB;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTask != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxTCB = xTask;
  # DEBUG BEGIN_STMT
  pxTCB->uxTaskNumber = uxHandle;

  <bb 4> :
  return;

}


uxTaskGetTaskNumber (struct tskTaskControlBlock * xTask)
{
  const struct TCB_t * pxTCB;
  UBaseType_t uxReturn;
  UBaseType_t D.7990;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTask != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxTCB = xTask;
  # DEBUG BEGIN_STMT
  uxReturn = pxTCB->uxTaskNumber;
  goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  uxReturn = 0;

  <bb 5> :
  # DEBUG BEGIN_STMT
  D.7990 = uxReturn;
  return D.7990;

}


vTaskMissedYield ()
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  xYieldPending = 1;
  return;

}


xTaskCheckForTimeOut (struct TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait)
{
  const TickType_t xElapsedTime;
  const TickType_t xConstTickCount;
  BaseType_t xReturn;
  BaseType_t D.7985;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (pxTimeOut == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (pxTicksToWait == 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 7>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  xConstTickCount = xTickCount;
  # DEBUG BEGIN_STMT
  _1 = pxTimeOut->xTimeOnEntering;
  xElapsedTime = xConstTickCount - _1;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.116_2 = pxCurrentTCB;
  _3 = pxCurrentTCB.116_2->ucDelayAborted;
  if (_3 != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.117_4 = pxCurrentTCB;
  pxCurrentTCB.117_4->ucDelayAborted = 0;
  # DEBUG BEGIN_STMT
  xReturn = 1;
  goto <bb 18>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  _5 = *pxTicksToWait;
  if (_5 == 4294967295)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  xReturn = 0;
  goto <bb 18>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  _6 = pxTimeOut->xOverflowCount;
  xNumOfOverflows.118_7 = xNumOfOverflows;
  if (_6 != xNumOfOverflows.118_7)
    goto <bb 13>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 13> :
  _8 = pxTimeOut->xTimeOnEntering;
  if (xConstTickCount >= _8)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  xReturn = 1;
  # DEBUG BEGIN_STMT
  *pxTicksToWait = 0;
  goto <bb 18>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  _9 = *pxTicksToWait;
  if (xElapsedTime < _9)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  _10 = *pxTicksToWait;
  _11 = _10 - xElapsedTime;
  *pxTicksToWait = _11;
  # DEBUG BEGIN_STMT
  vTaskInternalSetTimeOutState (pxTimeOut);
  # DEBUG BEGIN_STMT
  xReturn = 0;
  goto <bb 18>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  *pxTicksToWait = 0;
  # DEBUG BEGIN_STMT
  xReturn = 1;

  <bb 18> :
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  D.7985 = xReturn;
  return D.7985;

}


vTaskInternalSetTimeOutState (struct TimeOut_t * const pxTimeOut)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  xNumOfOverflows.114_1 = xNumOfOverflows;
  pxTimeOut->xOverflowCount = xNumOfOverflows.114_1;
  # DEBUG BEGIN_STMT
  xTickCount.115_2 = xTickCount;
  pxTimeOut->xTimeOnEntering = xTickCount.115_2;
  return;

}


vTaskSetTimeOutState (struct TimeOut_t * const pxTimeOut)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  if (pxTimeOut == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  xNumOfOverflows.112_1 = xNumOfOverflows;
  pxTimeOut->xOverflowCount = xNumOfOverflows.112_1;
  # DEBUG BEGIN_STMT
  xTickCount.113_2 = xTickCount;
  pxTimeOut->xTimeOnEntering = xTickCount.113_2;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  return;

}


vTaskRemoveFromUnorderedEventList (struct ListItem_t * pxEventListItem, const TickType_t xItemValue)
{
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  struct List_t * const pxList;
  struct TCB_t * pxUnblockedTCB;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.109_1 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.109_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _2 = xItemValue | 2147483648;
  pxEventListItem->xItemValue = _2;
  # DEBUG BEGIN_STMT
  pxUnblockedTCB = pxEventListItem->pvOwner;
  # DEBUG BEGIN_STMT
  if (pxUnblockedTCB == 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 7>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxList = pxEventListItem->pvContainer;
  # DEBUG BEGIN_STMT
  _3 = pxEventListItem->pxNext;
  _4 = pxEventListItem->pxPrevious;
  _3->pxPrevious = _4;
  # DEBUG BEGIN_STMT
  _5 = pxEventListItem->pxPrevious;
  _6 = pxEventListItem->pxNext;
  _5->pxNext = _6;
  # DEBUG BEGIN_STMT
  _7 = pxList->pxIndex;
  if (pxEventListItem == _7)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  _8 = pxEventListItem->pxPrevious;
  pxList->pxIndex = _8;

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxEventListItem->pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _9 = pxList->uxNumberOfItems;
  _10 = _9 + 4294967295;
  pxList->uxNumberOfItems = _10;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxList = pxUnblockedTCB->xStateListItem.pvContainer;
  # DEBUG BEGIN_STMT
  _11 = pxUnblockedTCB->xStateListItem.pxNext;
  _12 = pxUnblockedTCB->xStateListItem.pxPrevious;
  _11->pxPrevious = _12;
  # DEBUG BEGIN_STMT
  _13 = pxUnblockedTCB->xStateListItem.pxPrevious;
  _14 = pxUnblockedTCB->xStateListItem.pxNext;
  _13->pxNext = _14;
  # DEBUG BEGIN_STMT
  _15 = pxList->pxIndex;
  _16 = &pxUnblockedTCB->xStateListItem;
  if (_15 == _16)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  _17 = pxUnblockedTCB->xStateListItem.pxPrevious;
  pxList->pxIndex = _17;

  <bb 12> :
  # DEBUG BEGIN_STMT
  pxUnblockedTCB->xStateListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _18 = pxList->uxNumberOfItems;
  _19 = _18 + 4294967295;
  pxList->uxNumberOfItems = _19;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _20 = pxUnblockedTCB->uxPriority;
  uxTopReadyPriority.110_21 = uxTopReadyPriority;
  if (_20 > uxTopReadyPriority.110_21)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  _22 = pxUnblockedTCB->uxPriority;
  uxTopReadyPriority = _22;

  <bb 14> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _23 = pxUnblockedTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_23].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxUnblockedTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _24 = pxIndex->pxPrevious;
  pxUnblockedTCB->xStateListItem.pxPrevious = _24;
  # DEBUG BEGIN_STMT
  _25 = pxIndex->pxPrevious;
  _26 = &pxUnblockedTCB->xStateListItem;
  _25->pxNext = _26;
  # DEBUG BEGIN_STMT
  _27 = &pxUnblockedTCB->xStateListItem;
  pxIndex->pxPrevious = _27;
  # DEBUG BEGIN_STMT
  _28 = pxUnblockedTCB->uxPriority;
  _29 = &pxReadyTasksLists[_28];
  pxUnblockedTCB->xStateListItem.pvContainer = _29;
  # DEBUG BEGIN_STMT
  _30 = pxUnblockedTCB->uxPriority;
  _31 = pxReadyTasksLists[_30].uxNumberOfItems;
  _32 = _31 + 1;
  pxReadyTasksLists[_30].uxNumberOfItems = _32;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _33 = pxUnblockedTCB->uxPriority;
  pxCurrentTCB.111_34 = pxCurrentTCB;
  _35 = pxCurrentTCB.111_34->uxPriority;
  if (_33 > _35)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  xYieldPending = 1;

  <bb 16> :
  return;

}


xTaskRemoveFromEventList (const struct List_t * const pxEventList)
{
  struct ListItem_t * const pxIndex;
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  struct List_t * const pxList;
  BaseType_t xReturn;
  struct TCB_t * pxUnblockedTCB;
  BaseType_t D.7952;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 = pxEventList->xListEnd.pxNext;
  pxUnblockedTCB = _1->pvOwner;
  # DEBUG BEGIN_STMT
  if (pxUnblockedTCB == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxList = pxUnblockedTCB->xEventListItem.pvContainer;
  # DEBUG BEGIN_STMT
  _2 = pxUnblockedTCB->xEventListItem.pxNext;
  _3 = pxUnblockedTCB->xEventListItem.pxPrevious;
  _2->pxPrevious = _3;
  # DEBUG BEGIN_STMT
  _4 = pxUnblockedTCB->xEventListItem.pxPrevious;
  _5 = pxUnblockedTCB->xEventListItem.pxNext;
  _4->pxNext = _5;
  # DEBUG BEGIN_STMT
  _6 = pxList->pxIndex;
  _7 = &pxUnblockedTCB->xEventListItem;
  if (_6 == _7)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  _8 = pxUnblockedTCB->xEventListItem.pxPrevious;
  pxList->pxIndex = _8;

  <bb 7> :
  # DEBUG BEGIN_STMT
  pxUnblockedTCB->xEventListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _9 = pxList->uxNumberOfItems;
  _10 = _9 + 4294967295;
  pxList->uxNumberOfItems = _10;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.106_11 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.106_11 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  pxList = pxUnblockedTCB->xStateListItem.pvContainer;
  # DEBUG BEGIN_STMT
  _12 = pxUnblockedTCB->xStateListItem.pxNext;
  _13 = pxUnblockedTCB->xStateListItem.pxPrevious;
  _12->pxPrevious = _13;
  # DEBUG BEGIN_STMT
  _14 = pxUnblockedTCB->xStateListItem.pxPrevious;
  _15 = pxUnblockedTCB->xStateListItem.pxNext;
  _14->pxNext = _15;
  # DEBUG BEGIN_STMT
  _16 = pxList->pxIndex;
  _17 = &pxUnblockedTCB->xStateListItem;
  if (_16 == _17)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  _18 = pxUnblockedTCB->xStateListItem.pxPrevious;
  pxList->pxIndex = _18;

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxUnblockedTCB->xStateListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _19 = pxList->uxNumberOfItems;
  _20 = _19 + 4294967295;
  pxList->uxNumberOfItems = _20;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _21 = pxUnblockedTCB->uxPriority;
  uxTopReadyPriority.107_22 = uxTopReadyPriority;
  if (_21 > uxTopReadyPriority.107_22)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  _23 = pxUnblockedTCB->uxPriority;
  uxTopReadyPriority = _23;

  <bb 12> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _24 = pxUnblockedTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_24].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxUnblockedTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _25 = pxIndex->pxPrevious;
  pxUnblockedTCB->xStateListItem.pxPrevious = _25;
  # DEBUG BEGIN_STMT
  _26 = pxIndex->pxPrevious;
  _27 = &pxUnblockedTCB->xStateListItem;
  _26->pxNext = _27;
  # DEBUG BEGIN_STMT
  _28 = &pxUnblockedTCB->xStateListItem;
  pxIndex->pxPrevious = _28;
  # DEBUG BEGIN_STMT
  _29 = pxUnblockedTCB->uxPriority;
  _30 = &pxReadyTasksLists[_29];
  pxUnblockedTCB->xStateListItem.pvContainer = _30;
  # DEBUG BEGIN_STMT
  _31 = pxUnblockedTCB->uxPriority;
  _32 = pxReadyTasksLists[_31].uxNumberOfItems;
  _33 = _32 + 1;
  pxReadyTasksLists[_31].uxNumberOfItems = _33;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 14>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  pxIndex = xPendingReadyList.pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxUnblockedTCB->xEventListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _34 = pxIndex->pxPrevious;
  pxUnblockedTCB->xEventListItem.pxPrevious = _34;
  # DEBUG BEGIN_STMT
  _35 = pxIndex->pxPrevious;
  _36 = &pxUnblockedTCB->xEventListItem;
  _35->pxNext = _36;
  # DEBUG BEGIN_STMT
  _37 = &pxUnblockedTCB->xEventListItem;
  pxIndex->pxPrevious = _37;
  # DEBUG BEGIN_STMT
  pxUnblockedTCB->xEventListItem.pvContainer = &xPendingReadyList;
  # DEBUG BEGIN_STMT
  _38 = xPendingReadyList.uxNumberOfItems;
  _39 = _38 + 1;
  xPendingReadyList.uxNumberOfItems = _39;

  <bb 14> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _40 = pxUnblockedTCB->uxPriority;
  pxCurrentTCB.108_41 = pxCurrentTCB;
  _42 = pxCurrentTCB.108_41->uxPriority;
  if (_40 > _42)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  xReturn = 1;
  # DEBUG BEGIN_STMT
  xYieldPending = 1;
  goto <bb 17>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  xReturn = 0;

  <bb 17> :
  # DEBUG BEGIN_STMT
  D.7952 = xReturn;
  return D.7952;

}


vTaskPlaceOnEventListRestricted (struct List_t * const pxEventList, TickType_t xTicksToWait, const BaseType_t xWaitIndefinitely)
{
  struct ListItem_t * const pxIndex;

  <bb 2> :
  # DEBUG BEGIN_STMT
  if (pxEventList == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxIndex = pxEventList->pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.101_1 = pxCurrentTCB;
  pxCurrentTCB.101_1->xEventListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.102_2 = pxCurrentTCB;
  _3 = pxIndex->pxPrevious;
  pxCurrentTCB.102_2->xEventListItem.pxPrevious = _3;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.103_4 = pxCurrentTCB;
  _5 = pxIndex->pxPrevious;
  _6 = &pxCurrentTCB.103_4->xEventListItem;
  _5->pxNext = _6;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.104_7 = pxCurrentTCB;
  _8 = &pxCurrentTCB.104_7->xEventListItem;
  pxIndex->pxPrevious = _8;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.105_9 = pxCurrentTCB;
  pxCurrentTCB.105_9->xEventListItem.pvContainer = pxEventList;
  # DEBUG BEGIN_STMT
  _10 = pxEventList->uxNumberOfItems;
  _11 = _10 + 1;
  pxEventList->uxNumberOfItems = _11;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xWaitIndefinitely != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  xTicksToWait = 4294967295;

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  prvAddCurrentTaskToDelayedList (xTicksToWait, xWaitIndefinitely);
  return;

}


vTaskPlaceOnUnorderedEventList (struct List_t * pxEventList, const TickType_t xItemValue, const TickType_t xTicksToWait)
{
  struct ListItem_t * const pxIndex;

  <bb 2> :
  # DEBUG BEGIN_STMT
  if (pxEventList == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.94_1 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.94_1 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 7>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.95_2 = pxCurrentTCB;
  _3 = xItemValue | 2147483648;
  pxCurrentTCB.95_2->xEventListItem.xItemValue = _3;
  # DEBUG BEGIN_STMT
  pxIndex = pxEventList->pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.96_4 = pxCurrentTCB;
  pxCurrentTCB.96_4->xEventListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.97_5 = pxCurrentTCB;
  _6 = pxIndex->pxPrevious;
  pxCurrentTCB.97_5->xEventListItem.pxPrevious = _6;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.98_7 = pxCurrentTCB;
  _8 = pxIndex->pxPrevious;
  _9 = &pxCurrentTCB.98_7->xEventListItem;
  _8->pxNext = _9;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.99_10 = pxCurrentTCB;
  _11 = &pxCurrentTCB.99_10->xEventListItem;
  pxIndex->pxPrevious = _11;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.100_12 = pxCurrentTCB;
  pxCurrentTCB.100_12->xEventListItem.pvContainer = pxEventList;
  # DEBUG BEGIN_STMT
  _13 = pxEventList->uxNumberOfItems;
  _14 = _13 + 1;
  pxEventList->uxNumberOfItems = _14;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  prvAddCurrentTaskToDelayedList (xTicksToWait, 1);
  return;

}


vTaskPlaceOnEventList (struct List_t * const pxEventList, const TickType_t xTicksToWait)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  if (pxEventList == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.93_1 = pxCurrentTCB;
  _2 = &pxCurrentTCB.93_1->xEventListItem;
  vListInsert (pxEventList, _2);
  # DEBUG BEGIN_STMT
  prvAddCurrentTaskToDelayedList (xTicksToWait, 1);
  return;

}


__attribute__((used))
vTaskSwitchContext ()
{
  struct List_t * const pxConstList;
  UBaseType_t uxTopPriority;

  <bb 2> :
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.92_1 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.92_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  xYieldPending = 1;
  goto <bb 13>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  xYieldPending = 0;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxTopPriority = uxTopReadyPriority;
  # DEBUG BEGIN_STMT
  goto <bb 9>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  if (uxTopPriority == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 7>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxTopPriority = uxTopPriority + 4294967295;

  <bb 9> :
  # DEBUG BEGIN_STMT
  _2 = pxReadyTasksLists[uxTopPriority].uxNumberOfItems;
  if (_2 == 0)
    goto <bb 5>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxConstList = &pxReadyTasksLists[uxTopPriority];
  # DEBUG BEGIN_STMT
  _3 = pxConstList->pxIndex;
  _4 = _3->pxNext;
  pxConstList->pxIndex = _4;
  # DEBUG BEGIN_STMT
  _5 = pxConstList->pxIndex;
  _6 = &pxConstList->xListEnd;
  if (_5 == _6)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  _7 = pxConstList->pxIndex;
  _8 = _7->pxNext;
  pxConstList->pxIndex = _8;

  <bb 12> :
  # DEBUG BEGIN_STMT
  _9 = pxConstList->pxIndex;
  _10 = _9->pvOwner;
  pxCurrentTCB = _10;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxTopReadyPriority = uxTopPriority;

  <bb 13> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  return;

}


xTaskIncrementTick ()
{
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  struct List_t * const pxList;
  struct List_t * pxTemp;
  const TickType_t xConstTickCount;
  BaseType_t xSwitchRequired;
  TickType_t xItemValue;
  struct TCB_t * pxTCB;
  BaseType_t D.7919;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xSwitchRequired = 0;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.79_1 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.79_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  xTickCount.80_2 = xTickCount;
  xConstTickCount = xTickCount.80_2 + 1;
  # DEBUG BEGIN_STMT
  xTickCount = xConstTickCount;
  # DEBUG BEGIN_STMT
  if (xConstTickCount == 0)
    goto <bb 4>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxDelayedTaskList.81_3 = pxDelayedTaskList;
  _4 = pxDelayedTaskList.81_3->uxNumberOfItems;
  if (_4 != 0)
    goto <bb 5>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 6>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTemp = pxDelayedTaskList;
  # DEBUG BEGIN_STMT
  pxOverflowDelayedTaskList.82_5 = pxOverflowDelayedTaskList;
  pxDelayedTaskList = pxOverflowDelayedTaskList.82_5;
  # DEBUG BEGIN_STMT
  pxOverflowDelayedTaskList = pxTemp;
  # DEBUG BEGIN_STMT
  xNumOfOverflows.83_6 = xNumOfOverflows;
  _7 = xNumOfOverflows.83_6 + 1;
  xNumOfOverflows = _7;
  # DEBUG BEGIN_STMT
  prvResetNextTaskUnblockTime ();
  # DEBUG BEGIN_STMT

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xNextTaskUnblockTime.84_8 = xNextTaskUnblockTime;
  if (xConstTickCount >= xNextTaskUnblockTime.84_8)
    goto <bb 9>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxDelayedTaskList.85_9 = pxDelayedTaskList;
  _10 = pxDelayedTaskList.85_9->uxNumberOfItems;
  if (_10 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  xNextTaskUnblockTime = 4294967295;
  # DEBUG BEGIN_STMT
  goto <bb 23>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxDelayedTaskList.86_11 = pxDelayedTaskList;
  _12 = pxDelayedTaskList.86_11->xListEnd.pxNext;
  pxTCB = _12->pvOwner;
  # DEBUG BEGIN_STMT
  xItemValue = pxTCB->xStateListItem.xItemValue;
  # DEBUG BEGIN_STMT
  if (xConstTickCount < xItemValue)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  xNextTaskUnblockTime = xItemValue;
  # DEBUG BEGIN_STMT
  goto <bb 23>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxList = pxTCB->xStateListItem.pvContainer;
  # DEBUG BEGIN_STMT
  _13 = pxTCB->xStateListItem.pxNext;
  _14 = pxTCB->xStateListItem.pxPrevious;
  _13->pxPrevious = _14;
  # DEBUG BEGIN_STMT
  _15 = pxTCB->xStateListItem.pxPrevious;
  _16 = pxTCB->xStateListItem.pxNext;
  _15->pxNext = _16;
  # DEBUG BEGIN_STMT
  _17 = pxList->pxIndex;
  _18 = &pxTCB->xStateListItem;
  if (_17 == _18)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  _19 = pxTCB->xStateListItem.pxPrevious;
  pxList->pxIndex = _19;

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _20 = pxList->uxNumberOfItems;
  _21 = _20 + 4294967295;
  pxList->uxNumberOfItems = _21;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _22 = pxTCB->xEventListItem.pvContainer;
  if (_22 != 0B)
    goto <bb 16>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  pxList = pxTCB->xEventListItem.pvContainer;
  # DEBUG BEGIN_STMT
  _23 = pxTCB->xEventListItem.pxNext;
  _24 = pxTCB->xEventListItem.pxPrevious;
  _23->pxPrevious = _24;
  # DEBUG BEGIN_STMT
  _25 = pxTCB->xEventListItem.pxPrevious;
  _26 = pxTCB->xEventListItem.pxNext;
  _25->pxNext = _26;
  # DEBUG BEGIN_STMT
  _27 = pxList->pxIndex;
  _28 = &pxTCB->xEventListItem;
  if (_27 == _28)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  _29 = pxTCB->xEventListItem.pxPrevious;
  pxList->pxIndex = _29;

  <bb 18> :
  # DEBUG BEGIN_STMT
  pxTCB->xEventListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _30 = pxList->uxNumberOfItems;
  _31 = _30 + 4294967295;
  pxList->uxNumberOfItems = _31;
  # DEBUG BEGIN_STMT

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _32 = pxTCB->uxPriority;
  uxTopReadyPriority.87_33 = uxTopReadyPriority;
  if (_32 > uxTopReadyPriority.87_33)
    goto <bb 20>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 20> :
  # DEBUG BEGIN_STMT
  _34 = pxTCB->uxPriority;
  uxTopReadyPriority = _34;

  <bb 21> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _35 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_35].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _36 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _36;
  # DEBUG BEGIN_STMT
  _37 = pxIndex->pxPrevious;
  _38 = &pxTCB->xStateListItem;
  _37->pxNext = _38;
  # DEBUG BEGIN_STMT
  _39 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _39;
  # DEBUG BEGIN_STMT
  _40 = pxTCB->uxPriority;
  _41 = &pxReadyTasksLists[_40];
  pxTCB->xStateListItem.pvContainer = _41;
  # DEBUG BEGIN_STMT
  _42 = pxTCB->uxPriority;
  _43 = pxReadyTasksLists[_42].uxNumberOfItems;
  _44 = _43 + 1;
  pxReadyTasksLists[_42].uxNumberOfItems = _44;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _45 = pxTCB->uxPriority;
  pxCurrentTCB.88_46 = pxCurrentTCB;
  _47 = pxCurrentTCB.88_46->uxPriority;
  if (_45 >= _47)
    goto <bb 22>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 22> :
  # DEBUG BEGIN_STMT
  xSwitchRequired = 1;
  goto <bb 9>; [INV]

  <bb 23> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.89_48 = pxCurrentTCB;
  _49 = pxCurrentTCB.89_48->uxPriority;
  _50 = pxReadyTasksLists[_49].uxNumberOfItems;
  if (_50 > 1)
    goto <bb 24>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 24> :
  # DEBUG BEGIN_STMT
  xSwitchRequired = 1;

  <bb 25> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xYieldPending.90_51 = xYieldPending;
  if (xYieldPending.90_51 != 0)
    goto <bb 26>; [INV]
  else
    goto <bb 28>; [INV]

  <bb 26> :
  # DEBUG BEGIN_STMT
  xSwitchRequired = 1;
  goto <bb 28>; [INV]

  <bb 27> :
  # DEBUG BEGIN_STMT
  xPendedTicks.91_52 = xPendedTicks;
  _53 = xPendedTicks.91_52 + 1;
  xPendedTicks = _53;

  <bb 28> :
  # DEBUG BEGIN_STMT
  D.7919 = xSwitchRequired;
  return D.7919;

}


xTaskAbortDelay (struct tskTaskControlBlock * xTask)
{
  struct ListItem_t * const pxIndex;
  BaseType_t xReturn;
  struct TCB_t * pxTCB;
  BaseType_t D.7885;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxTCB = xTask;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (pxTCB == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  _1 = eTaskGetState (xTask);
  if (_1 == 2)
    goto <bb 6>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  xReturn = 1;
  # DEBUG BEGIN_STMT
  _2 = &pxTCB->xStateListItem;
  uxListRemove (_2);
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _3 = pxTCB->xEventListItem.pvContainer;
  if (_3 != 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  _4 = &pxTCB->xEventListItem;
  uxListRemove (_4);
  # DEBUG BEGIN_STMT
  pxTCB->ucDelayAborted = 1;

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _5 = pxTCB->uxPriority;
  uxTopReadyPriority.77_6 = uxTopReadyPriority;
  if (_5 > uxTopReadyPriority.77_6)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  _7 = pxTCB->uxPriority;
  uxTopReadyPriority = _7;

  <bb 10> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _8 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_8].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _9 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _9;
  # DEBUG BEGIN_STMT
  _10 = pxIndex->pxPrevious;
  _11 = &pxTCB->xStateListItem;
  _10->pxNext = _11;
  # DEBUG BEGIN_STMT
  _12 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _12;
  # DEBUG BEGIN_STMT
  _13 = pxTCB->uxPriority;
  _14 = &pxReadyTasksLists[_13];
  pxTCB->xStateListItem.pvContainer = _14;
  # DEBUG BEGIN_STMT
  _15 = pxTCB->uxPriority;
  _16 = pxReadyTasksLists[_15].uxNumberOfItems;
  _17 = _16 + 1;
  pxReadyTasksLists[_15].uxNumberOfItems = _17;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _18 = pxTCB->uxPriority;
  pxCurrentTCB.78_19 = pxCurrentTCB;
  _20 = pxCurrentTCB.78_19->uxPriority;
  if (_18 > _20)
    goto <bb 11>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  xYieldPending = 1;
  goto <bb 13>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  xReturn = 0;

  <bb 13> :
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  D.7885 = xReturn;
  return D.7885;

}


xTaskCatchUpTicks (TickType_t xTicksToCatchUp)
{
  BaseType_t xYieldOccurred;
  BaseType_t D.7870;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.75_1 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.75_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  xPendedTicks.76_2 = xPendedTicks;
  _3 = xTicksToCatchUp + xPendedTicks.76_2;
  xPendedTicks = _3;
  # DEBUG BEGIN_STMT
  xYieldOccurred = xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  D.7870 = xYieldOccurred;
  return D.7870;

}


uxTaskGetSystemState (struct TaskStatus_t * const pxTaskStatusArray, const UBaseType_t uxArraySize, uint32_t * const pulTotalRunTime)
{
  UBaseType_t uxQueue;
  UBaseType_t uxTask;
  UBaseType_t D.7857;
  long unsigned int D.7853;
  long unsigned int D.7852;
  long unsigned int D.7851;
  long unsigned int D.7850;
  long unsigned int D.7849;

  <bb 2> :
  # DEBUG BEGIN_STMT
  uxTask = 0;
  uxQueue = 5;
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  uxCurrentNumberOfTasks.72_1 = uxCurrentNumberOfTasks;
  if (uxArraySize >= uxCurrentNumberOfTasks.72_1)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxQueue = uxQueue + 4294967295;
  # DEBUG BEGIN_STMT
  _2 = uxTask * 36;
  _3 = pxTaskStatusArray + _2;
  _4 = &pxReadyTasksLists[uxQueue];
  D.7849 = prvListTasksWithinSingleList (_3, _4, 1);
  uxTask = D.7849 + uxTask;
  # DEBUG BEGIN_STMT
  if (uxQueue != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  _5 = uxTask * 36;
  _6 = pxTaskStatusArray + _5;
  pxDelayedTaskList.73_7 = pxDelayedTaskList;
  D.7850 = prvListTasksWithinSingleList (_6, pxDelayedTaskList.73_7, 2);
  uxTask = D.7850 + uxTask;
  # DEBUG BEGIN_STMT
  _8 = uxTask * 36;
  _9 = pxTaskStatusArray + _8;
  pxOverflowDelayedTaskList.74_10 = pxOverflowDelayedTaskList;
  D.7851 = prvListTasksWithinSingleList (_9, pxOverflowDelayedTaskList.74_10, 2);
  uxTask = D.7851 + uxTask;
  # DEBUG BEGIN_STMT
  _11 = uxTask * 36;
  _12 = pxTaskStatusArray + _11;
  D.7852 = prvListTasksWithinSingleList (_12, &xTasksWaitingTermination, 4);
  uxTask = D.7852 + uxTask;
  # DEBUG BEGIN_STMT
  _13 = uxTask * 36;
  _14 = pxTaskStatusArray + _13;
  D.7853 = prvListTasksWithinSingleList (_14, &xSuspendedTaskList, 3);
  uxTask = D.7853 + uxTask;
  # DEBUG BEGIN_STMT
  if (pulTotalRunTime != 0B)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  *pulTotalRunTime = 0;

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  D.7857 = uxTask;
  return D.7857;

}


xTaskGetHandle (const char * pcNameToQuery)
{
  struct TCB_t * pxTCB;
  UBaseType_t uxQueue;
  struct tskTaskControlBlock * D.7828;

  <bb 2> :
  # DEBUG BEGIN_STMT
  uxQueue = 5;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 = strlen (pcNameToQuery);
  if (_1 > 9)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxQueue = uxQueue + 4294967295;
  # DEBUG BEGIN_STMT
  _2 = &pxReadyTasksLists[uxQueue];
  pxTCB = prvSearchForNameWithinSingleList (_2, pcNameToQuery);
  # DEBUG BEGIN_STMT
  if (pxTCB != 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  if (uxQueue != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  if (pxTCB == 0B)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxDelayedTaskList.70_3 = pxDelayedTaskList;
  pxTCB = prvSearchForNameWithinSingleList (pxDelayedTaskList.70_3, pcNameToQuery);

  <bb 10> :
  # DEBUG BEGIN_STMT
  if (pxTCB == 0B)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxOverflowDelayedTaskList.71_4 = pxOverflowDelayedTaskList;
  pxTCB = prvSearchForNameWithinSingleList (pxOverflowDelayedTaskList.71_4, pcNameToQuery);

  <bb 12> :
  # DEBUG BEGIN_STMT
  if (pxTCB == 0B)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  pxTCB = prvSearchForNameWithinSingleList (&xSuspendedTaskList, pcNameToQuery);

  <bb 14> :
  # DEBUG BEGIN_STMT
  if (pxTCB == 0B)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxTCB = prvSearchForNameWithinSingleList (&xTasksWaitingTermination, pcNameToQuery);

  <bb 16> :
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  D.7828 = pxTCB;
  return D.7828;

}


prvSearchForNameWithinSingleList (struct List_t * pxList, const char * pcNameToQuery)
{
  struct List_t * const pxConstList;
  struct List_t * const pxConstList;
  BaseType_t xBreakLoop;
  char cNextChar;
  UBaseType_t x;
  struct TCB_t * pxReturn;
  struct TCB_t * pxFirstTCB;
  struct TCB_t * pxNextTCB;
  struct TCB_t * D.7845;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxReturn = 0B;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 = pxList->uxNumberOfItems;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxConstList = pxList;
  # DEBUG BEGIN_STMT
  _2 = pxConstList->pxIndex;
  _3 = _2->pxNext;
  pxConstList->pxIndex = _3;
  # DEBUG BEGIN_STMT
  _4 = pxConstList->pxIndex;
  _5 = &pxConstList->xListEnd;
  if (_4 == _5)
    goto <bb 4>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  _6 = pxConstList->pxIndex;
  _7 = _6->pxNext;
  pxConstList->pxIndex = _7;

  <bb 5> :
  # DEBUG BEGIN_STMT
  _8 = pxConstList->pxIndex;
  pxFirstTCB = _8->pvOwner;

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxConstList = pxList;
  # DEBUG BEGIN_STMT
  _9 = pxConstList->pxIndex;
  _10 = _9->pxNext;
  pxConstList->pxIndex = _10;
  # DEBUG BEGIN_STMT
  _11 = pxConstList->pxIndex;
  _12 = &pxConstList->xListEnd;
  if (_11 == _12)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  _13 = pxConstList->pxIndex;
  _14 = _13->pxNext;
  pxConstList->pxIndex = _14;

  <bb 8> :
  # DEBUG BEGIN_STMT
  _15 = pxConstList->pxIndex;
  pxNextTCB = _15->pvOwner;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xBreakLoop = 0;
  # DEBUG BEGIN_STMT
  x = 0;
  goto <bb 15>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  cNextChar = pxNextTCB->pcTaskName[x];
  # DEBUG BEGIN_STMT
  _16 = pcNameToQuery + x;
  _17 = *_16;
  if (cNextChar != _17)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  xBreakLoop = 1;
  goto <bb 13>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  if (cNextChar == 0)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  pxReturn = pxNextTCB;
  # DEBUG BEGIN_STMT
  xBreakLoop = 1;

  <bb 13> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xBreakLoop != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  x = x + 1;

  <bb 15> :
  # DEBUG BEGIN_STMT
  if (x <= 9)
    goto <bb 9>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  if (pxReturn != 0B)
    goto <bb 18>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  if (pxNextTCB != pxFirstTCB)
    goto <bb 6>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  D.7845 = pxReturn;
  return D.7845;

}


pcTaskGetName (struct tskTaskControlBlock * xTaskToQuery)
{
  struct TCB_t * pxTCB;
  char * D.7815;
  struct TCB_t * iftmp.69;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTaskToQuery == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  iftmp.69 = pxCurrentTCB;
  goto <bb 5>; [INV]

  <bb 4> :
  iftmp.69 = xTaskToQuery;

  <bb 5> :
  pxTCB = iftmp.69;
  # DEBUG BEGIN_STMT
  if (pxTCB == 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 7>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  D.7815 = &pxTCB->pcTaskName[0];
  return D.7815;

}


uxTaskGetNumberOfTasks ()
{
  UBaseType_t D.7807;

  <bb 2> :
  # DEBUG BEGIN_STMT
  D.7807 = uxCurrentNumberOfTasks;
  return D.7807;

}


xTaskGetTickCountFromISR ()
{
  UBaseType_t uxSavedInterruptStatus;
  TickType_t xReturn;
  TickType_t D.7805;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus = 0;
  # DEBUG BEGIN_STMT
  xReturn = xTickCount;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  D.7805 = xReturn;
  return D.7805;

}


xTaskGetTickCount ()
{
  TickType_t xTicks;
  TickType_t D.7803;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xTicks = xTickCount;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  D.7803 = xTicks;
  return D.7803;

}


xTaskResumeAll ()
{
  TickType_t xPendedCounts;
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  struct List_t * const pxList;
  BaseType_t xAlreadyYielded;
  struct TCB_t * pxTCB;
  BaseType_t D.7801;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxTCB = 0B;
  # DEBUG BEGIN_STMT
  xAlreadyYielded = 0;
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.62_1 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.62_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.63_2 = uxSchedulerSuspended;
  _3 = uxSchedulerSuspended.63_2 + 4294967295;
  uxSchedulerSuspended = _3;
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.64_4 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.64_4 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  uxCurrentNumberOfTasks.65_5 = uxCurrentNumberOfTasks;
  if (uxCurrentNumberOfTasks.65_5 != 0)
    goto <bb 15>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  _6 = xPendingReadyList.xListEnd.pxNext;
  pxTCB = _6->pvOwner;
  # DEBUG BEGIN_STMT
  pxList = pxTCB->xEventListItem.pvContainer;
  # DEBUG BEGIN_STMT
  _7 = pxTCB->xEventListItem.pxNext;
  _8 = pxTCB->xEventListItem.pxPrevious;
  _7->pxPrevious = _8;
  # DEBUG BEGIN_STMT
  _9 = pxTCB->xEventListItem.pxPrevious;
  _10 = pxTCB->xEventListItem.pxNext;
  _9->pxNext = _10;
  # DEBUG BEGIN_STMT
  _11 = pxList->pxIndex;
  _12 = &pxTCB->xEventListItem;
  if (_11 == _12)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  _13 = pxTCB->xEventListItem.pxPrevious;
  pxList->pxIndex = _13;

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxTCB->xEventListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _14 = pxList->uxNumberOfItems;
  _15 = _14 + 4294967295;
  pxList->uxNumberOfItems = _15;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("" :  :  : "memory");
  # DEBUG BEGIN_STMT
  pxList = pxTCB->xStateListItem.pvContainer;
  # DEBUG BEGIN_STMT
  _16 = pxTCB->xStateListItem.pxNext;
  _17 = pxTCB->xStateListItem.pxPrevious;
  _16->pxPrevious = _17;
  # DEBUG BEGIN_STMT
  _18 = pxTCB->xStateListItem.pxPrevious;
  _19 = pxTCB->xStateListItem.pxNext;
  _18->pxNext = _19;
  # DEBUG BEGIN_STMT
  _20 = pxList->pxIndex;
  _21 = &pxTCB->xStateListItem;
  if (_20 == _21)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  _22 = pxTCB->xStateListItem.pxPrevious;
  pxList->pxIndex = _22;

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _23 = pxList->uxNumberOfItems;
  _24 = _23 + 4294967295;
  pxList->uxNumberOfItems = _24;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _25 = pxTCB->uxPriority;
  uxTopReadyPriority.66_26 = uxTopReadyPriority;
  if (_25 > uxTopReadyPriority.66_26)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  _27 = pxTCB->uxPriority;
  uxTopReadyPriority = _27;

  <bb 13> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _28 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_28].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _29 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _29;
  # DEBUG BEGIN_STMT
  _30 = pxIndex->pxPrevious;
  _31 = &pxTCB->xStateListItem;
  _30->pxNext = _31;
  # DEBUG BEGIN_STMT
  _32 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _32;
  # DEBUG BEGIN_STMT
  _33 = pxTCB->uxPriority;
  _34 = &pxReadyTasksLists[_33];
  pxTCB->xStateListItem.pvContainer = _34;
  # DEBUG BEGIN_STMT
  _35 = pxTCB->uxPriority;
  _36 = pxReadyTasksLists[_35].uxNumberOfItems;
  _37 = _36 + 1;
  pxReadyTasksLists[_35].uxNumberOfItems = _37;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _38 = pxTCB->uxPriority;
  pxCurrentTCB.67_39 = pxCurrentTCB;
  _40 = pxCurrentTCB.67_39->uxPriority;
  if (_38 >= _40)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  xYieldPending = 1;

  <bb 15> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _41 = xPendingReadyList.uxNumberOfItems;
  if (_41 != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  if (pxTCB != 0B)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  prvResetNextTaskUnblockTime ();

  <bb 18> :
  # DEBUG BEGIN_STMT
  xPendedCounts = xPendedTicks;
  # DEBUG BEGIN_STMT
  if (xPendedCounts != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _42 = xTaskIncrementTick ();
  if (_42 != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 20> :
  # DEBUG BEGIN_STMT
  xYieldPending = 1;

  <bb 21> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xPendedCounts = xPendedCounts + 4294967295;
  # DEBUG BEGIN_STMT
  if (xPendedCounts != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 22> :
  # DEBUG BEGIN_STMT
  xPendedTicks = 0;

  <bb 23> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xYieldPending.68_43 = xYieldPending;
  if (xYieldPending.68_43 != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 24> :
  # DEBUG BEGIN_STMT
  xAlreadyYielded = 1;
  # DEBUG BEGIN_STMT
  _44 = 3758157060B;
  *_44 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT

  <bb 25> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  D.7801 = xAlreadyYielded;
  return D.7801;

}


vTaskSuspendAll ()
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.61_1 = uxSchedulerSuspended;
  _2 = uxSchedulerSuspended.61_1 + 1;
  uxSchedulerSuspended = _2;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("" :  :  : "memory");
  return;

}


vTaskEndScheduler ()
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();
  # DEBUG BEGIN_STMT
  xSchedulerRunning = 0;
  # DEBUG BEGIN_STMT
  vPortEndScheduler ();
  return;

}


vTaskStartScheduler ()
{
  BaseType_t xReturn;
  long unsigned int vol.57;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xReturn = xTaskCreate (prvIdleTask, "IDLE", 90, 0B, 0, &xIdleTaskHandle);
  # DEBUG BEGIN_STMT
  if (xReturn == 1)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  xReturn = xTimerCreateTimerTask ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xReturn == 1)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();
  # DEBUG BEGIN_STMT
  xNextTaskUnblockTime = 4294967295;
  # DEBUG BEGIN_STMT
  xSchedulerRunning = 1;
  # DEBUG BEGIN_STMT
  xTickCount = 0;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 = xPortStartScheduler ();
  goto <bb 9>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  if (xReturn == -1)
    goto <bb 7>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 8>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vol.57 = uxTopUsedPriority;
  return;

}


xTaskResumeFromISR (struct tskTaskControlBlock * xTaskToResume)
{
  struct ListItem_t * const pxIndex;
  UBaseType_t uxSavedInterruptStatus;
  struct TCB_t * const pxTCB;
  BaseType_t xYieldRequired;
  BaseType_t D.7757;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xYieldRequired = 0;
  # DEBUG BEGIN_STMT
  pxTCB = xTaskToResume;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTaskToResume == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  # DEBUG BEGIN_STMT
  _1 = prvTaskIsTaskSuspended (pxTCB);
  if (_1 != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.54_2 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.54_2 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  _3 = pxTCB->uxPriority;
  pxCurrentTCB.55_4 = pxCurrentTCB;
  _5 = pxCurrentTCB.55_4->uxPriority;
  if (_3 >= _5)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  xYieldRequired = 1;
  # DEBUG BEGIN_STMT
  xYieldPending = 1;

  <bb 9> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _6 = &pxTCB->xStateListItem;
  uxListRemove (_6);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _7 = pxTCB->uxPriority;
  uxTopReadyPriority.56_8 = uxTopReadyPriority;
  if (_7 > uxTopReadyPriority.56_8)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  _9 = pxTCB->uxPriority;
  uxTopReadyPriority = _9;

  <bb 11> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _10 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_10].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _11 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _11;
  # DEBUG BEGIN_STMT
  _12 = pxIndex->pxPrevious;
  _13 = &pxTCB->xStateListItem;
  _12->pxNext = _13;
  # DEBUG BEGIN_STMT
  _14 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _14;
  # DEBUG BEGIN_STMT
  _15 = pxTCB->uxPriority;
  _16 = &pxReadyTasksLists[_15];
  pxTCB->xStateListItem.pvContainer = _16;
  # DEBUG BEGIN_STMT
  _17 = pxTCB->uxPriority;
  _18 = pxReadyTasksLists[_17].uxNumberOfItems;
  _19 = _18 + 1;
  pxReadyTasksLists[_17].uxNumberOfItems = _19;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 13>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  _20 = &pxTCB->xEventListItem;
  vListInsertEnd (&xPendingReadyList, _20);

  <bb 13> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptStatus);
  # DEBUG BEGIN_STMT
  D.7757 = xYieldRequired;
  return D.7757;

}


vTaskResume (struct tskTaskControlBlock * xTaskToResume)
{
  struct ListItem_t * const pxIndex;
  struct TCB_t * const pxTCB;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxTCB = xTaskToResume;
  # DEBUG BEGIN_STMT
  if (xTaskToResume == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.51_1 = pxCurrentTCB;
  if (pxTCB != pxCurrentTCB.51_1)
    goto <bb 6>; [INV]
  else
    goto <bb 13>; [INV]

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _2 = prvTaskIsTaskSuspended (pxTCB);
  if (_2 != 0)
    goto <bb 8>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _3 = &pxTCB->xStateListItem;
  uxListRemove (_3);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _4 = pxTCB->uxPriority;
  uxTopReadyPriority.52_5 = uxTopReadyPriority;
  if (_4 > uxTopReadyPriority.52_5)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  _6 = pxTCB->uxPriority;
  uxTopReadyPriority = _6;

  <bb 10> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _7 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_7].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _8 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _8;
  # DEBUG BEGIN_STMT
  _9 = pxIndex->pxPrevious;
  _10 = &pxTCB->xStateListItem;
  _9->pxNext = _10;
  # DEBUG BEGIN_STMT
  _11 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _11;
  # DEBUG BEGIN_STMT
  _12 = pxTCB->uxPriority;
  _13 = &pxReadyTasksLists[_12];
  pxTCB->xStateListItem.pvContainer = _13;
  # DEBUG BEGIN_STMT
  _14 = pxTCB->uxPriority;
  _15 = pxReadyTasksLists[_14].uxNumberOfItems;
  _16 = _15 + 1;
  pxReadyTasksLists[_14].uxNumberOfItems = _16;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _17 = pxTCB->uxPriority;
  pxCurrentTCB.53_18 = pxCurrentTCB;
  _19 = pxCurrentTCB.53_18->uxPriority;
  if (_17 >= _19)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  _20 = 3758157060B;
  *_20 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT

  <bb 12> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();

  <bb 13> :
  # DEBUG BEGIN_STMT
  return;

}


prvTaskIsTaskSuspended (struct tskTaskControlBlock * const xTask)
{
  const struct TCB_t * const pxTCB;
  BaseType_t xReturn;
  BaseType_t D.7742;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xReturn = 0;
  # DEBUG BEGIN_STMT
  pxTCB = xTask;
  # DEBUG BEGIN_STMT
  if (xTask == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 = pxTCB->xStateListItem.pvContainer;
  if (_1 == &xSuspendedTaskList)
    goto <bb 6>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  _2 = pxTCB->xEventListItem.pvContainer;
  if (_2 != &xPendingReadyList)
    goto <bb 7>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  _3 = pxTCB->xEventListItem.pvContainer;
  if (_3 == 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  xReturn = 1;

  <bb 9> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  D.7742 = xReturn;
  return D.7742;

}


vTaskSuspend (struct tskTaskControlBlock * xTaskToSuspend)
{
  BaseType_t x;
  struct TCB_t * pxTCB;
  struct TCB_t * iftmp.45;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  if (xTaskToSuspend == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  iftmp.45 = pxCurrentTCB;
  goto <bb 5>; [INV]

  <bb 4> :
  iftmp.45 = xTaskToSuspend;

  <bb 5> :
  pxTCB = iftmp.45;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 = &pxTCB->xStateListItem;
  _2 = uxListRemove (_1);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _3 = pxTCB->xEventListItem.pvContainer;
  if (_3 != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  _4 = &pxTCB->xEventListItem;
  uxListRemove (_4);

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _5 = &pxTCB->xStateListItem;
  vListInsertEnd (&xSuspendedTaskList, _5);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  x = 0;
  goto <bb 11>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  _6 = pxTCB->ucNotifyState[x];
  if (_6 == 1)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxTCB->ucNotifyState[x] = 0;

  <bb 10> :
  # DEBUG BEGIN_STMT
  x = x + 1;

  <bb 11> :
  # DEBUG BEGIN_STMT
  if (x <= 0)
    goto <bb 8>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  xSchedulerRunning.46_7 = xSchedulerRunning;
  if (xSchedulerRunning.46_7 != 0)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  prvResetNextTaskUnblockTime ();
  # DEBUG BEGIN_STMT
  vPortExitCritical ();

  <bb 14> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.47_8 = pxCurrentTCB;
  if (pxTCB == pxCurrentTCB.47_8)
    goto <bb 15>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  xSchedulerRunning.48_9 = xSchedulerRunning;
  if (xSchedulerRunning.48_9 != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.49_10 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.49_10 != 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 18> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 18>; [INV]

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _11 = 3758157060B;
  *_11 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT
  goto <bb 23>; [INV]

  <bb 20> :
  # DEBUG BEGIN_STMT
  _12 = xSuspendedTaskList.uxNumberOfItems;
  uxCurrentNumberOfTasks.50_13 = uxCurrentNumberOfTasks;
  if (_12 == uxCurrentNumberOfTasks.50_13)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB = 0B;
  goto <bb 23>; [INV]

  <bb 22> :
  # DEBUG BEGIN_STMT
  vTaskSwitchContext ();

  <bb 23> :
  # DEBUG BEGIN_STMT
  return;

}


vTaskPrioritySet (struct tskTaskControlBlock * xTask, UBaseType_t uxNewPriority)
{
  struct ListItem_t * const pxIndex;
  BaseType_t xYieldRequired;
  UBaseType_t uxPriorityUsedOnEntry;
  UBaseType_t uxCurrentBasePriority;
  struct TCB_t * pxTCB;
  struct TCB_t * iftmp.40;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xYieldRequired = 0;
  # DEBUG BEGIN_STMT
  if (uxNewPriority > 4)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (uxNewPriority > 4)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  uxNewPriority = 4;

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  if (xTask == 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  iftmp.40 = pxCurrentTCB;
  goto <bb 10>; [INV]

  <bb 9> :
  iftmp.40 = xTask;

  <bb 10> :
  pxTCB = iftmp.40;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxCurrentBasePriority = pxTCB->uxBasePriority;
  # DEBUG BEGIN_STMT
  if (uxCurrentBasePriority != uxNewPriority)
    goto <bb 11>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  if (uxNewPriority > uxCurrentBasePriority)
    goto <bb 12>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.41_1 = pxCurrentTCB;
  if (pxTCB != pxCurrentTCB.41_1)
    goto <bb 13>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.42_2 = pxCurrentTCB;
  _3 = pxCurrentTCB.42_2->uxPriority;
  if (uxNewPriority >= _3)
    goto <bb 14>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  xYieldRequired = 1;
  goto <bb 17>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.43_4 = pxCurrentTCB;
  if (pxTCB == pxCurrentTCB.43_4)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  xYieldRequired = 1;

  <bb 17> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxPriorityUsedOnEntry = pxTCB->uxPriority;
  # DEBUG BEGIN_STMT
  _5 = pxTCB->uxBasePriority;
  _6 = pxTCB->uxPriority;
  if (_5 == _6)
    goto <bb 18>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  pxTCB->uxPriority = uxNewPriority;

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->uxBasePriority = uxNewPriority;
  # DEBUG BEGIN_STMT
  _7 = pxTCB->xEventListItem.xItemValue;
  _8 = (signed int) _7;
  if (_8 >= 0)
    goto <bb 20>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 20> :
  # DEBUG BEGIN_STMT
  _9 = 5 - uxNewPriority;
  pxTCB->xEventListItem.xItemValue = _9;

  <bb 21> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _10 = pxTCB->xStateListItem.pvContainer;
  _11 = &pxReadyTasksLists[uxPriorityUsedOnEntry];
  if (_10 == _11)
    goto <bb 22>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 22> :
  # DEBUG BEGIN_STMT
  _12 = &pxTCB->xStateListItem;
  _13 = uxListRemove (_12);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _14 = pxTCB->uxPriority;
  uxTopReadyPriority.44_15 = uxTopReadyPriority;
  if (_14 > uxTopReadyPriority.44_15)
    goto <bb 23>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 23> :
  # DEBUG BEGIN_STMT
  _16 = pxTCB->uxPriority;
  uxTopReadyPriority = _16;

  <bb 24> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _17 = pxTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_17].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _18 = pxIndex->pxPrevious;
  pxTCB->xStateListItem.pxPrevious = _18;
  # DEBUG BEGIN_STMT
  _19 = pxIndex->pxPrevious;
  _20 = &pxTCB->xStateListItem;
  _19->pxNext = _20;
  # DEBUG BEGIN_STMT
  _21 = &pxTCB->xStateListItem;
  pxIndex->pxPrevious = _21;
  # DEBUG BEGIN_STMT
  _22 = pxTCB->uxPriority;
  _23 = &pxReadyTasksLists[_22];
  pxTCB->xStateListItem.pvContainer = _23;
  # DEBUG BEGIN_STMT
  _24 = pxTCB->uxPriority;
  _25 = pxReadyTasksLists[_24].uxNumberOfItems;
  _26 = _25 + 1;
  pxReadyTasksLists[_24].uxNumberOfItems = _26;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT

  <bb 25> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xYieldRequired != 0)
    goto <bb 26>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 26> :
  # DEBUG BEGIN_STMT
  _27 = 3758157060B;
  *_27 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT

  <bb 27> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  return;

}


uxTaskPriorityGetFromISR (struct tskTaskControlBlock * const xTask)
{
  UBaseType_t uxSavedInterruptState;
  UBaseType_t uxReturn;
  const struct TCB_t * pxTCB;
  UBaseType_t D.7646;
  const struct TCB_t * iftmp.39;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  uxSavedInterruptState = ulPortRaiseBASEPRI ();
  # DEBUG BEGIN_STMT
  if (xTask == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  iftmp.39 = pxCurrentTCB;
  goto <bb 5>; [INV]

  <bb 4> :
  iftmp.39 = xTask;

  <bb 5> :
  pxTCB = iftmp.39;
  # DEBUG BEGIN_STMT
  uxReturn = pxTCB->uxPriority;
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptState);
  # DEBUG BEGIN_STMT
  D.7646 = uxReturn;
  return D.7646;

}


uxTaskPriorityGet (struct tskTaskControlBlock * const xTask)
{
  UBaseType_t uxReturn;
  const struct TCB_t * pxTCB;
  UBaseType_t D.7640;
  const struct TCB_t * iftmp.38;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  if (xTask == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  iftmp.38 = pxCurrentTCB;
  goto <bb 5>; [INV]

  <bb 4> :
  iftmp.38 = xTask;

  <bb 5> :
  pxTCB = iftmp.38;
  # DEBUG BEGIN_STMT
  uxReturn = pxTCB->uxPriority;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  D.7640 = uxReturn;
  return D.7640;

}


eTaskGetState (struct tskTaskControlBlock * xTask)
{
  BaseType_t x;
  const struct TCB_t * const pxTCB;
  const struct List_t * pxOverflowedDelayedList;
  const struct List_t * pxDelayedList;
  const struct List_t * pxStateList;
  eTaskState eReturn;
  eTaskState D.7634;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxTCB = xTask;
  # DEBUG BEGIN_STMT
  if (pxTCB == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.37_1 = pxCurrentTCB;
  if (pxTCB == pxCurrentTCB.37_1)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  eReturn = 0;
  goto <bb 22>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  pxStateList = pxTCB->xStateListItem.pvContainer;
  # DEBUG BEGIN_STMT
  pxDelayedList = pxDelayedTaskList;
  # DEBUG BEGIN_STMT
  pxOverflowedDelayedList = pxOverflowDelayedTaskList;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  if (pxStateList == pxDelayedList)
    goto <bb 9>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 8> :
  if (pxStateList == pxOverflowedDelayedList)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  eReturn = 2;
  goto <bb 22>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  if (pxStateList == &xSuspendedTaskList)
    goto <bb 11>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  _2 = pxTCB->xEventListItem.pvContainer;
  if (_2 == 0B)
    goto <bb 12>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  eReturn = 3;
  # DEBUG BEGIN_STMT
  x = 0;
  goto <bb 16>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  _3 = pxTCB->ucNotifyState[x];
  if (_3 == 1)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  eReturn = 2;
  # DEBUG BEGIN_STMT
  goto <bb 22>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  x = x + 1;

  <bb 16> :
  # DEBUG BEGIN_STMT
  if (x <= 0)
    goto <bb 13>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  eReturn = 2;
  goto <bb 22>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  if (pxStateList == &xTasksWaitingTermination)
    goto <bb 20>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 19> :
  if (pxStateList == 0B)
    goto <bb 20>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 20> :
  # DEBUG BEGIN_STMT
  eReturn = 4;
  goto <bb 22>; [INV]

  <bb 21> :
  # DEBUG BEGIN_STMT
  eReturn = 1;

  <bb 22> :
  # DEBUG BEGIN_STMT
  D.7634 = eReturn;
  return D.7634;

}


vTaskDelay (const TickType_t xTicksToDelay)
{
  BaseType_t xAlreadyYielded;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xAlreadyYielded = 0;
  # DEBUG BEGIN_STMT
  if (xTicksToDelay != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.36_1 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.36_1 != 0)
    goto <bb 4>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 5>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  prvAddCurrentTaskToDelayedList (xTicksToDelay, 0);
  # DEBUG BEGIN_STMT
  xAlreadyYielded = xTaskResumeAll ();

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xAlreadyYielded == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  _2 = 3758157060B;
  *_2 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT

  <bb 9> :
  # DEBUG BEGIN_STMT
  return;

}


xTaskDelayUntil (TickType_t * const pxPreviousWakeTime, const TickType_t xTimeIncrement)
{
  const TickType_t xConstTickCount;
  BaseType_t xShouldDelay;
  BaseType_t xAlreadyYielded;
  TickType_t xTimeToWake;
  BaseType_t D.7590;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xShouldDelay = 0;
  # DEBUG BEGIN_STMT
  if (pxPreviousWakeTime == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xTimeIncrement == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 7>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.22_1 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.22_1 != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 10> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 10>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  xConstTickCount = xTickCount;
  # DEBUG BEGIN_STMT
  _2 = *pxPreviousWakeTime;
  xTimeToWake = xTimeIncrement + _2;
  # DEBUG BEGIN_STMT
  _3 = *pxPreviousWakeTime;
  if (xConstTickCount < _3)
    goto <bb 12>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  _4 = *pxPreviousWakeTime;
  if (xTimeToWake < _4)
    goto <bb 13>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 13> :
  if (xTimeToWake > xConstTickCount)
    goto <bb 14>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  xShouldDelay = 1;
  goto <bb 18>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  _5 = *pxPreviousWakeTime;
  if (xTimeToWake < _5)
    goto <bb 17>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 16> :
  if (xTimeToWake > xConstTickCount)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  xShouldDelay = 1;

  <bb 18> :
  # DEBUG BEGIN_STMT
  *pxPreviousWakeTime = xTimeToWake;
  # DEBUG BEGIN_STMT
  if (xShouldDelay != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _6 = xTimeToWake - xConstTickCount;
  prvAddCurrentTaskToDelayedList (_6, 0);

  <bb 20> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xAlreadyYielded = xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  if (xAlreadyYielded == 0)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  # DEBUG BEGIN_STMT
  _7 = 3758157060B;
  *_7 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT

  <bb 22> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  D.7590 = xShouldDelay;
  return D.7590;

}


vTaskDelete (struct tskTaskControlBlock * xTaskToDelete)
{
  struct TCB_t * pxTCB;
  struct TCB_t * iftmp.12;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  if (xTaskToDelete == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  iftmp.12 = pxCurrentTCB;
  goto <bb 5>; [INV]

  <bb 4> :
  iftmp.12 = xTaskToDelete;

  <bb 5> :
  pxTCB = iftmp.12;
  # DEBUG BEGIN_STMT
  _1 = &pxTCB->xStateListItem;
  _2 = uxListRemove (_1);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _3 = pxTCB->xEventListItem.pvContainer;
  if (_3 != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  _4 = &pxTCB->xEventListItem;
  uxListRemove (_4);

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxTaskNumber.13_5 = uxTaskNumber;
  _6 = uxTaskNumber.13_5 + 1;
  uxTaskNumber = _6;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.14_7 = pxCurrentTCB;
  if (pxTCB == pxCurrentTCB.14_7)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  _8 = &pxTCB->xStateListItem;
  vListInsertEnd (&xTasksWaitingTermination, _8);
  # DEBUG BEGIN_STMT
  uxDeletedTasksWaitingCleanUp.15_9 = uxDeletedTasksWaitingCleanUp;
  _10 = uxDeletedTasksWaitingCleanUp.15_9 + 1;
  uxDeletedTasksWaitingCleanUp = _10;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  uxCurrentNumberOfTasks.16_11 = uxCurrentNumberOfTasks;
  _12 = uxCurrentNumberOfTasks.16_11 + 4294967295;
  uxCurrentNumberOfTasks = _12;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  prvDeleteTCB (pxTCB);
  # DEBUG BEGIN_STMT
  prvResetNextTaskUnblockTime ();

  <bb 10> :
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  xSchedulerRunning.17_13 = xSchedulerRunning;
  if (xSchedulerRunning.17_13 != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.18_14 = pxCurrentTCB;
  if (pxTCB == pxCurrentTCB.18_14)
    goto <bb 12>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  uxSchedulerSuspended.19_15 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.19_15 != 0)
    goto <bb 13>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 14> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 14>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _16 = 3758157060B;
  *_16 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT

  <bb 16> :
  # DEBUG BEGIN_STMT
  return;

}


prvAddNewTaskToReadyList (struct TCB_t * pxNewTCB)
{
  struct ListItem_t * const pxIndex;

  <bb 2> :
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  uxCurrentNumberOfTasks.2_1 = uxCurrentNumberOfTasks;
  _2 = uxCurrentNumberOfTasks.2_1 + 1;
  uxCurrentNumberOfTasks = _2;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.3_3 = pxCurrentTCB;
  if (pxCurrentTCB.3_3 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB = pxNewTCB;
  # DEBUG BEGIN_STMT
  uxCurrentNumberOfTasks.4_4 = uxCurrentNumberOfTasks;
  if (uxCurrentNumberOfTasks.4_4 == 1)
    goto <bb 4>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  prvInitialiseTaskLists ();
  goto <bb 8>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  xSchedulerRunning.5_5 = xSchedulerRunning;
  if (xSchedulerRunning.5_5 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.6_6 = pxCurrentTCB;
  _7 = pxCurrentTCB.6_6->uxPriority;
  _8 = pxNewTCB->uxPriority;
  if (_7 <= _8)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB = pxNewTCB;

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxTaskNumber.7_9 = uxTaskNumber;
  _10 = uxTaskNumber.7_9 + 1;
  uxTaskNumber = _10;
  # DEBUG BEGIN_STMT
  uxTaskNumber.8_11 = uxTaskNumber;
  pxNewTCB->uxTCBNumber = uxTaskNumber.8_11;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _12 = pxNewTCB->uxPriority;
  uxTopReadyPriority.9_13 = uxTopReadyPriority;
  if (_12 > uxTopReadyPriority.9_13)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  _14 = pxNewTCB->uxPriority;
  uxTopReadyPriority = _14;

  <bb 10> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _15 = pxNewTCB->uxPriority;
  pxIndex = pxReadyTasksLists[_15].pxIndex;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxNewTCB->xStateListItem.pxNext = pxIndex;
  # DEBUG BEGIN_STMT
  _16 = pxIndex->pxPrevious;
  pxNewTCB->xStateListItem.pxPrevious = _16;
  # DEBUG BEGIN_STMT
  _17 = pxIndex->pxPrevious;
  _18 = &pxNewTCB->xStateListItem;
  _17->pxNext = _18;
  # DEBUG BEGIN_STMT
  _19 = &pxNewTCB->xStateListItem;
  pxIndex->pxPrevious = _19;
  # DEBUG BEGIN_STMT
  _20 = pxNewTCB->uxPriority;
  _21 = &pxReadyTasksLists[_20];
  pxNewTCB->xStateListItem.pvContainer = _21;
  # DEBUG BEGIN_STMT
  _22 = pxNewTCB->uxPriority;
  _23 = pxReadyTasksLists[_22].uxNumberOfItems;
  _24 = _23 + 1;
  pxReadyTasksLists[_22].uxNumberOfItems = _24;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  xSchedulerRunning.10_25 = xSchedulerRunning;
  if (xSchedulerRunning.10_25 != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.11_26 = pxCurrentTCB;
  _27 = pxCurrentTCB.11_26->uxPriority;
  _28 = pxNewTCB->uxPriority;
  if (_27 < _28)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  # DEBUG BEGIN_STMT
  _29 = 3758157060B;
  *_29 = 268435456;
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("dsb" :  :  : "memory");
  # DEBUG BEGIN_STMT
  __asm__ __volatile__("isb");
  # DEBUG BEGIN_STMT

  <bb 13> :
  # DEBUG BEGIN_STMT
  return;

}


prvInitialiseNewTask (void (*TaskFunction_t) (void *) pxTaskCode, const char * const pcName, const uint32_t ulStackDepth, void * const pvParameters, UBaseType_t uxPriority, struct tskTaskControlBlock * * const pxCreatedTask, struct TCB_t * pxNewTCB, const struct MemoryRegion_t * const xRegions)
{
  UBaseType_t x;
  StackType_t * pxTopOfStack;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 = pxNewTCB->pxStack;
  _2 = ulStackDepth * 4;
  memset (_1, 165, _2);
  # DEBUG BEGIN_STMT
  _3 = pxNewTCB->pxStack;
  _4 = ulStackDepth + 1073741823;
  _5 = _4 * 4;
  pxTopOfStack = _3 + _5;
  # DEBUG BEGIN_STMT
  pxTopOfStack.0_6 = (long unsigned int) pxTopOfStack;
  _7 = pxTopOfStack.0_6 & 4294967288;
  pxTopOfStack = (StackType_t *) _7;
  # DEBUG BEGIN_STMT
  pxTopOfStack.1_8 = (long unsigned int) pxTopOfStack;
  _9 = pxTopOfStack.1_8 & 7;
  if (_9 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 4>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (pcName != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  x = 0;
  goto <bb 9>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  _10 = pcName + x;
  _11 = *_10;
  pxNewTCB->pcTaskName[x] = _11;
  # DEBUG BEGIN_STMT
  _12 = pcName + x;
  _13 = *_12;
  if (_13 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  x = x + 1;

  <bb 9> :
  # DEBUG BEGIN_STMT
  if (x <= 9)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxNewTCB->pcTaskName[9] = 0;
  goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxNewTCB->pcTaskName[0] = 0;

  <bb 12> :
  # DEBUG BEGIN_STMT
  if (uxPriority > 4)
    goto <bb 13>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  vPortRaiseBASEPRI ();

  <bb 14> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  goto <bb 14>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (uxPriority > 4)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  uxPriority = 4;

  <bb 17> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxNewTCB->uxPriority = uxPriority;
  # DEBUG BEGIN_STMT
  pxNewTCB->uxBasePriority = uxPriority;
  # DEBUG BEGIN_STMT
  pxNewTCB->uxMutexesHeld = 0;
  # DEBUG BEGIN_STMT
  _14 = &pxNewTCB->xStateListItem;
  vListInitialiseItem (_14);
  # DEBUG BEGIN_STMT
  _15 = &pxNewTCB->xEventListItem;
  vListInitialiseItem (_15);
  # DEBUG BEGIN_STMT
  pxNewTCB->xStateListItem.pvOwner = pxNewTCB;
  # DEBUG BEGIN_STMT
  _16 = 5 - uxPriority;
  pxNewTCB->xEventListItem.xItemValue = _16;
  # DEBUG BEGIN_STMT
  pxNewTCB->xEventListItem.pvOwner = pxNewTCB;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _17 = &pxNewTCB->ulNotifiedValue[0];
  memset (_17, 0, 4);
  # DEBUG BEGIN_STMT
  _18 = &pxNewTCB->ucNotifyState[0];
  memset (_18, 0, 1);
  # DEBUG BEGIN_STMT
  pxNewTCB->ucDelayAborted = 0;
  # DEBUG BEGIN_STMT
  _19 = pxPortInitialiseStack (pxTopOfStack, pxTaskCode, pvParameters);
  pxNewTCB->pxTopOfStack = _19;
  # DEBUG BEGIN_STMT
  if (pxCreatedTask != 0B)
    goto <bb 18>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  *pxCreatedTask = pxNewTCB;

  <bb 19> :
  # DEBUG BEGIN_STMT
  return;

}


xTaskCreate (void (*TaskFunction_t) (void *) pxTaskCode, const char * const pcName, const uint16_t usStackDepth, void * const pvParameters, UBaseType_t uxPriority, struct tskTaskControlBlock * * const pxCreatedTask)
{
  StackType_t * pxStack;
  BaseType_t xReturn;
  struct TCB_t * pxNewTCB;
  BaseType_t D.7508;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 = (unsigned int) usStackDepth;
  _2 = _1 * 4;
  pxStack = pvPortMalloc (_2);
  # DEBUG BEGIN_STMT
  if (pxStack != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxNewTCB = pvPortMalloc (88);
  # DEBUG BEGIN_STMT
  if (pxNewTCB != 0B)
    goto <bb 4>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  pxNewTCB->pxStack = pxStack;
  goto <bb 7>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  vPortFree (pxStack);
  goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxNewTCB = 0B;

  <bb 7> :
  # DEBUG BEGIN_STMT
  if (pxNewTCB != 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  _3 = (long unsigned int) usStackDepth;
  prvInitialiseNewTask (pxTaskCode, pcName, _3, pvParameters, uxPriority, pxCreatedTask, pxNewTCB, 0B);
  # DEBUG BEGIN_STMT
  prvAddNewTaskToReadyList (pxNewTCB);
  # DEBUG BEGIN_STMT
  xReturn = 1;
  goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  xReturn = -1;

  <bb 10> :
  # DEBUG BEGIN_STMT
  D.7508 = xReturn;
  return D.7508;

}


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

}


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

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

}


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

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

}