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) @06161000
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: prvWriteNameToBuffer/83 
  Calls: 
sprintf/111 (sprintf) @06141ee0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskList/84 
  Calls: 
strlen/110 (strlen) @060d49a0
  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) @060d4000
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskEndScheduler/44 
  Calls: 
xPortStartScheduler/108 (xPortStartScheduler) @05a9ac40
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskStartScheduler/43 
  Calls: 
xTimerCreateTimerTask/107 (xTimerCreateTimerTask) @05a9ab60
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: vTaskStartScheduler/43 
  Calls: 
vPortValidateInterruptPriority/106 (vPortValidateInterruptPriority) @05a83e00
  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) @05a837e0
  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) @05a830e0
  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) @05a83000
  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) @060b4ee0
  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) @060b4d20
  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) @060b4b60
  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) @060b48c0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: prvInitialiseNewTask/30 
  Calls: 
vListInitialiseItem/98 (vListInitialiseItem) @060b47e0
  Type: function
  Visibility: external public
  References: 
  Referring: 
  Availability: not_available
  Function flags: optimize_size
  Called by: prvInitialiseNewTask/30 prvInitialiseNewTask/30 
  Calls: 
memset/97 (memset) @060b4700
  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) @060b4540
  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) @060b4460
  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) @060b4000
  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) @0607a540
  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) @0607ad20
  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) @0607a8c0
  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) @0607a460
  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) @0606ce00
  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) @0606cd20
  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) @0606c8c0
  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) @0606c460
  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) @0606c1c0
  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) @0604fc40
  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) @0604f540
  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) @0604f000
  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) @0604fb60
  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) @0604f700
  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) @0604f460
  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) @0604f1c0
  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) @06043c40
  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) @06043380
  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) @06043ee0
  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) @06043b60
  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) @060438c0
  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) @06043620
  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) @060432a0
  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) @0603fee0
  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) @0603f9a0
  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) @0603fe00
  Type: function definition analyzed
  Visibility: externally_visible public
  References: 
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
uxTaskGetTaskNumber/67 (uxTaskGetTaskNumber) @0603fb60
  Type: function definition analyzed
  Visibility: externally_visible public
  References: 
  Referring: 
  Availability: available
  Function flags: body optimize_size
  Called by: 
  Calls: 
vTaskMissedYield/66 (vTaskMissedYield) @0603f8c0
  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) @0603f620
  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) @0603f1c0
  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) @05f9ab60
  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) @05f9aee0
  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) @05f9aa80
  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) @05f9a620
  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) @05f9a2a0
  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) @05f8aa80
  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) @05f8ae00
  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) @05f8a9a0
  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) @05f8a380
  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) @05f8a000
  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) @05f7f7e0
  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) @05f7f2a0
  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) @05f7fe00
  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) @05f7fb60
  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) @05f7f700
  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) @05f7f460
  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) @05f7f1c0
  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) @05f6ce00
  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) @05f6cd20
  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) @05f6ca80
  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) @05f6c7e0
  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) @05f6c540
  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) @05f6c1c0
  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) @05f5d9a0
  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) @05f5de00
  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) @05f5d8c0
  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) @05f5d380
  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) @05f5d000
  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) @05f482a0
  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) @05f48c40
  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) @05f487e0
  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) @05f481c0
  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) @05f36540
  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) @05f36c40
  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) @05f36700
  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) @05f305a0
  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) @05f30510
  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) @05f30480
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: vTaskStartScheduler/43 (addr)
  Availability: available
  Varpool flags: initialized
xNextTaskUnblockTime/25 (xNextTaskUnblockTime) @05f303f0
  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) @05f30360
  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) @05f30318
  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) @05f302d0
  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) @05f30240
  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) @05f301b0
  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) @05f30120
  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) @05f300d8
  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) @05f30090
  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) @05f2cf78
  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) @05f2cee8
  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) @05f2ce58
  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) @05f2cdc8
  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) @05f2cd38
  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) @05f2ccf0
  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) @05f2cca8
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: prvInitialiseTaskLists/70 (addr)prvInitialiseTaskLists/70 (addr)
  Availability: available
  Varpool flags:
xDelayedTaskList1/9 (xDelayedTaskList1) @05f2cc18
  Type: variable definition analyzed
  Visibility: prevailing_def_ironly
  References: 
  Referring: prvInitialiseTaskLists/70 (addr)prvInitialiseTaskLists/70 (addr)
  Availability: available
  Varpool flags:
pxReadyTasksLists/8 (pxReadyTasksLists) @05f2cb88
  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) @05f2cb40
  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) @05e54b60
  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) @05e548c0
  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) @05e54540
  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;

}