BLE/Debug_FLASH/FreeRTOS/Source/tasks.c.017i.build_ssa_passes

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;

}