prvAddCurrentTaskToDelayedList (TickType_t xTicksToWait, const BaseType_t xCanBlockIndefinitely)
{
  struct ListItem_t * const pxIndex;
  const TickType_t xConstTickCount;
  TickType_t xTimeToWake;

  <bb 2> :
  xConstTickCount = xTickCount;
  pxCurrentTCB.152_1 = pxCurrentTCB;
  pxCurrentTCB.152_1->ucDelayAborted = 0;
  pxCurrentTCB.153_2 = pxCurrentTCB;
  _3 = &pxCurrentTCB.153_2->xStateListItem;
  _4 = uxListRemove (_3);

  <bb 3> :
  if (xTicksToWait == 4294967295)
    goto <bb 4>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 5> :
  pxIndex = xSuspendedTaskList.pxIndex;
  pxCurrentTCB.154_5 = pxCurrentTCB;
  pxCurrentTCB.154_5->xStateListItem.pxNext = pxIndex;
  pxCurrentTCB.155_6 = pxCurrentTCB;
  _7 = pxIndex->pxPrevious;
  pxCurrentTCB.155_6->xStateListItem.pxPrevious = _7;
  pxCurrentTCB.156_8 = pxCurrentTCB;
  _9 = pxIndex->pxPrevious;
  _10 = &pxCurrentTCB.156_8->xStateListItem;
  _9->pxNext = _10;
  pxCurrentTCB.157_11 = pxCurrentTCB;
  _12 = &pxCurrentTCB.157_11->xStateListItem;
  pxIndex->pxPrevious = _12;
  pxCurrentTCB.158_13 = pxCurrentTCB;
  pxCurrentTCB.158_13->xStateListItem.pvContainer = &xSuspendedTaskList;
  _14 = xSuspendedTaskList.uxNumberOfItems;
  _15 = _14 + 1;
  xSuspendedTaskList.uxNumberOfItems = _15;
  goto <bb 10>; [INV]

  <bb 6> :
  xTimeToWake = xConstTickCount + xTicksToWait;
  pxCurrentTCB.159_16 = pxCurrentTCB;
  pxCurrentTCB.159_16->xStateListItem.xItemValue = xTimeToWake;
  if (xTimeToWake < xConstTickCount)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  pxOverflowDelayedTaskList.160_17 = pxOverflowDelayedTaskList;
  pxCurrentTCB.161_18 = pxCurrentTCB;
  _19 = &pxCurrentTCB.161_18->xStateListItem;
  vListInsert (pxOverflowDelayedTaskList.160_17, _19);
  goto <bb 10>; [INV]

  <bb 8> :
  pxDelayedTaskList.162_20 = pxDelayedTaskList;
  pxCurrentTCB.163_21 = pxCurrentTCB;
  _22 = &pxCurrentTCB.163_21->xStateListItem;
  vListInsert (pxDelayedTaskList.162_20, _22);
  xNextTaskUnblockTime.164_23 = xNextTaskUnblockTime;
  if (xTimeToWake < xNextTaskUnblockTime.164_23)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  xNextTaskUnblockTime = xTimeToWake;

  <bb 10> :
  return;

}


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

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

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

  <bb 4> :
  iftmp.151 = xTask;

  <bb 5> :
  pxTCB = iftmp.151;
  vPortEnterCritical ();
  ulReturn = pxTCB->ulNotifiedValue[uxIndexToClear];
  _1 = pxTCB->ulNotifiedValue[uxIndexToClear];
  _2 = ~ulBitsToClear;
  _3 = _1 & _2;
  pxTCB->ulNotifiedValue[uxIndexToClear] = _3;
  vPortExitCritical ();
  D.8224 = ulReturn;

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

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

  <bb 7> :
  iftmp.150 = xTask;

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

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

  <bb 10> :
  xReturn = 0;

  <bb 11> :
  vPortExitCritical ();
  D.8218 = xReturn;

  <bb 12> :
<L9>:
  return D.8218;

}


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> :
  if (xTaskToNotify == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

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

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

  <bb 10> :
  vPortRaiseBASEPRI ();

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

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

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

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

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

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

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

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

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

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

  <bb 21> :
  *pxHigherPriorityTaskWoken = 1;

  <bb 22> :
  xYieldPending = 1;

  <bb 23> :
  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.8187;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

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

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

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

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

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

  <bb 13> :
<L10>:
  pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue;
  goto <bb 23>; [INV]

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

  <bb 15> :
  pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue;
  goto <bb 17>; [INV]

  <bb 16> :
  xReturn = 0;

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

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

  <bb 19> :
<L16>:
  xTickCount.143_6 = xTickCount;
  if (xTickCount.143_6 != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 20> :
  vPortRaiseBASEPRI ();

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

  <bb 22> :

  <bb 23> :
  if (ucOriginalNotifyState == 1)
    goto <bb 24>; [INV]
  else
    goto <bb 38>; [INV]

  <bb 24> :
  _7 = pxTCB->xEventListItem.pvContainer;
  if (_7 != 0B)
    goto <bb 25>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 25> :
  vPortRaiseBASEPRI ();

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

  <bb 27> :
  uxSchedulerSuspended.144_8 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.144_8 == 0)
    goto <bb 28>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 28> :
  pxList = pxTCB->xStateListItem.pvContainer;
  _9 = pxTCB->xStateListItem.pxNext;
  _10 = pxTCB->xStateListItem.pxPrevious;
  _9->pxPrevious = _10;
  _11 = pxTCB->xStateListItem.pxPrevious;
  _12 = pxTCB->xStateListItem.pxNext;
  _11->pxNext = _12;
  _13 = pxList->pxIndex;
  _14 = &pxTCB->xStateListItem;
  if (_13 == _14)
    goto <bb 29>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 29> :
  _15 = pxTCB->xStateListItem.pxPrevious;
  pxList->pxIndex = _15;

  <bb 30> :
  pxTCB->xStateListItem.pvContainer = 0B;
  _16 = pxList->uxNumberOfItems;
  _17 = _16 + 4294967295;
  pxList->uxNumberOfItems = _17;
  _18 = pxTCB->uxPriority;
  uxTopReadyPriority.145_19 = uxTopReadyPriority;
  if (_18 > uxTopReadyPriority.145_19)
    goto <bb 31>; [INV]
  else
    goto <bb 32>; [INV]

  <bb 31> :
  _20 = pxTCB->uxPriority;
  uxTopReadyPriority = _20;

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

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

  <bb 34> :
  _37 = pxTCB->uxPriority;
  pxCurrentTCB.146_38 = pxCurrentTCB;
  _39 = pxCurrentTCB.146_38->uxPriority;
  if (_37 > _39)
    goto <bb 35>; [INV]
  else
    goto <bb 38>; [INV]

  <bb 35> :
  if (pxHigherPriorityTaskWoken != 0B)
    goto <bb 36>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 36> :
  *pxHigherPriorityTaskWoken = 1;

  <bb 37> :
  xYieldPending = 1;

  <bb 38> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.8187 = xReturn;

  <bb 39> :
<L38>:
  return D.8187;

}


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.8158;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

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

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

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

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

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

  <bb 13> :
<L10>:
  pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue;
  goto <bb 23>; [INV]

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

  <bb 15> :
  pxTCB->ulNotifiedValue[uxIndexToNotify] = ulValue;
  goto <bb 17>; [INV]

  <bb 16> :
  xReturn = 0;

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

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

  <bb 19> :
<L16>:
  xTickCount.140_6 = xTickCount;
  if (xTickCount.140_6 != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 20> :
  vPortRaiseBASEPRI ();

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

  <bb 22> :

  <bb 23> :
  if (ucOriginalNotifyState == 1)
    goto <bb 24>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 24> :
  pxList = pxTCB->xStateListItem.pvContainer;
  _7 = pxTCB->xStateListItem.pxNext;
  _8 = pxTCB->xStateListItem.pxPrevious;
  _7->pxPrevious = _8;
  _9 = pxTCB->xStateListItem.pxPrevious;
  _10 = pxTCB->xStateListItem.pxNext;
  _9->pxNext = _10;
  _11 = pxList->pxIndex;
  _12 = &pxTCB->xStateListItem;
  if (_11 == _12)
    goto <bb 25>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 25> :
  _13 = pxTCB->xStateListItem.pxPrevious;
  pxList->pxIndex = _13;

  <bb 26> :
  pxTCB->xStateListItem.pvContainer = 0B;
  _14 = pxList->uxNumberOfItems;
  _15 = _14 + 4294967295;
  pxList->uxNumberOfItems = _15;
  _16 = pxTCB->uxPriority;
  uxTopReadyPriority.141_17 = uxTopReadyPriority;
  if (_16 > uxTopReadyPriority.141_17)
    goto <bb 27>; [INV]
  else
    goto <bb 28>; [INV]

  <bb 27> :
  _18 = pxTCB->uxPriority;
  uxTopReadyPriority = _18;

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

  <bb 29> :
  vPortRaiseBASEPRI ();

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

  <bb 31> :
  _30 = pxTCB->uxPriority;
  pxCurrentTCB.142_31 = pxCurrentTCB;
  _32 = pxCurrentTCB.142_31->uxPriority;
  if (_30 > _32)
    goto <bb 32>; [INV]
  else
    goto <bb 33>; [INV]

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

  <bb 33> :
  vPortExitCritical ();
  D.8158 = xReturn;

  <bb 34> :
<L34>:
  return D.8158;

}


xTaskGenericNotifyWait (UBaseType_t uxIndexToWait, uint32_t ulBitsToClearOnEntry, uint32_t ulBitsToClearOnExit, uint32_t * pulNotificationValue, TickType_t xTicksToWait)
{
  BaseType_t xReturn;
  BaseType_t D.8133;
  struct TCB_t * pxCurrentTCB.138;
  struct TCB_t * pxCurrentTCB.134;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

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

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

  <bb 9> :
  pxCurrentTCB.136_8 = pxCurrentTCB;
  _9 = pxCurrentTCB.136_8->ulNotifiedValue[uxIndexToWait];
  *pulNotificationValue = _9;

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

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

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

  <bb 13> :
  pxCurrentTCB.139_15 = pxCurrentTCB;
  pxCurrentTCB.139_15->ucNotifyState[uxIndexToWait] = 0;
  vPortExitCritical ();
  D.8133 = xReturn;

  <bb 14> :
<L14>:
  return D.8133;

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

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

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

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

  <bb 10> :
  pxCurrentTCB.130_6 = pxCurrentTCB;
  pxCurrentTCB.130_6->ulNotifiedValue[uxIndexToWait] = 0;
  goto <bb 12>; [INV]

  <bb 11> :
  pxCurrentTCB.131_7 = pxCurrentTCB;
  _8 = ulReturn + 4294967295;
  pxCurrentTCB.131_7->ulNotifiedValue[uxIndexToWait] = _8;

  <bb 12> :
  pxCurrentTCB.132_9 = pxCurrentTCB;
  pxCurrentTCB.132_9->ucNotifyState[uxIndexToWait] = 0;
  vPortExitCritical ();
  D.8116 = ulReturn;

  <bb 13> :
<L15>:
  return D.8116;

}


pvTaskIncrementMutexHeldCount ()
{
  struct tskTaskControlBlock * D.8100;

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

  <bb 3> :
  pxCurrentTCB.126_2 = pxCurrentTCB;
  _3 = pxCurrentTCB.126_2->uxMutexesHeld;
  _4 = _3 + 1;
  pxCurrentTCB.126_2->uxMutexesHeld = _4;

  <bb 4> :
  D.8100 = pxCurrentTCB;

  <bb 5> :
<L2>:
  return D.8100;

}


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

  <bb 2> :
  pxCurrentTCB.122_1 = pxCurrentTCB;
  uxReturn = pxCurrentTCB.122_1->xEventListItem.xItemValue;
  pxCurrentTCB.123_2 = pxCurrentTCB;
  _3 = pxCurrentTCB.123_2->uxPriority;
  pxCurrentTCB.124_4 = pxCurrentTCB;
  _5 = 5 - _3;
  pxCurrentTCB.124_4->xEventListItem.xItemValue = _5;
  D.8096 = uxReturn;

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

}


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

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

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

  <bb 4> :
  _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>:
  cStatus = 88;
  goto <bb 11>; [INV]

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

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

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

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

  <bb 10> :
<L7>:
  cStatus = 0;

  <bb 11> :
  _6 = x * 36;
  _7 = pxTaskStatusArray + _6;
  _8 = _7->pcTaskName;
  pcWriteBuffer = prvWriteNameToBuffer (pcWriteBuffer, _8);
  _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);
  _20 = strlen (pcWriteBuffer);
  pcWriteBuffer = pcWriteBuffer + _20;
  x = x + 1;

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

  <bb 13> :
  vPortFree (pxTaskStatusArray);

  <bb 14> :
  return;

}


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

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

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

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

  <bb 5> :
  _2 = pcBuffer + x;
  *_2 = 0;
  D.8091 = pcBuffer + x;

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

}


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> :
  pxTCB = pxMutexHolder;
  uxOnlyOneMutexHeld = 1;
  if (pxMutexHolder != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 21>; [INV]

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

  <bb 4> :
  vPortRaiseBASEPRI ();

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

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

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

  <bb 8> :
  uxPriorityToUse = pxTCB->uxBasePriority;

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

  <bb 10> :
  _4 = pxTCB->uxMutexesHeld;
  if (uxOnlyOneMutexHeld == _4)
    goto <bb 11>; [INV]
  else
    goto <bb 21>; [INV]

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

  <bb 12> :
  vPortRaiseBASEPRI ();

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

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

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

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

  <bb 17> :
  _11 = &pxTCB->xStateListItem;
  _12 = uxListRemove (_11);

  <bb 18> :
  _13 = pxTCB->uxPriority;
  uxTopReadyPriority.120_14 = uxTopReadyPriority;
  if (_13 > uxTopReadyPriority.120_14)
    goto <bb 19>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 19> :
  _15 = pxTCB->uxPriority;
  uxTopReadyPriority = _15;

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

  <bb 21> :
  return;

}


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

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

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

  <bb 4> :
  vPortRaiseBASEPRI ();

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

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

  <bb 7> :
  vPortRaiseBASEPRI ();

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

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

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

  <bb 11> :
  _8 = &pxTCB->xStateListItem;
  _9 = uxListRemove (_8);

  <bb 12> :
  _10 = pxTCB->uxBasePriority;
  pxTCB->uxPriority = _10;
  _11 = pxTCB->uxPriority;
  _12 = 5 - _11;
  pxTCB->xEventListItem.xItemValue = _12;
  _13 = pxTCB->uxPriority;
  uxTopReadyPriority.118_14 = uxTopReadyPriority;
  if (_13 > uxTopReadyPriority.118_14)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  _15 = pxTCB->uxPriority;
  uxTopReadyPriority = _15;

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

  <bb 15> :
  D.8062 = xReturn;

  <bb 16> :
<L20>:
  return D.8062;

}


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

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

  <bb 3> :
  _1 = pxMutexHolderTCB->uxPriority;
  pxCurrentTCB.111_2 = pxCurrentTCB;
  _3 = pxCurrentTCB.111_2->uxPriority;
  if (_1 < _3)
    goto <bb 4>; [INV]
  else
    goto <bb 13>; [INV]

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

  <bb 5> :
  pxCurrentTCB.112_6 = pxCurrentTCB;
  _7 = pxCurrentTCB.112_6->uxPriority;
  _8 = 5 - _7;
  pxMutexHolderTCB->xEventListItem.xItemValue = _8;

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

  <bb 7> :
  _12 = &pxMutexHolderTCB->xStateListItem;
  _13 = uxListRemove (_12);

  <bb 8> :
  pxCurrentTCB.113_14 = pxCurrentTCB;
  _15 = pxCurrentTCB.113_14->uxPriority;
  pxMutexHolderTCB->uxPriority = _15;
  _16 = pxMutexHolderTCB->uxPriority;
  uxTopReadyPriority.114_17 = uxTopReadyPriority;
  if (_16 > uxTopReadyPriority.114_17)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  _18 = pxMutexHolderTCB->uxPriority;
  uxTopReadyPriority = _18;

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

  <bb 11> :
  pxCurrentTCB.115_29 = pxCurrentTCB;
  _30 = pxCurrentTCB.115_29->uxPriority;
  pxMutexHolderTCB->uxPriority = _30;

  <bb 12> :
  xReturn = 1;
  goto <bb 15>; [INV]

  <bb 13> :
  _31 = pxMutexHolderTCB->uxBasePriority;
  pxCurrentTCB.116_32 = pxCurrentTCB;
  _33 = pxCurrentTCB.116_32->uxPriority;
  if (_31 < _33)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  xReturn = 1;

  <bb 15> :
  D.8042 = xReturn;

  <bb 16> :
<L20>:
  return D.8042;

}


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

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

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

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

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

  <bb 6> :
  xReturn = 0;

  <bb 7> :
  D.8020 = xReturn;

  <bb 8> :
<L6>:
  return D.8020;

}


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

  <bb 2> :
  xReturn = pxCurrentTCB;
  D.8012 = xReturn;

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

}


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

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

  <bb 4> :
  pxDelayedTaskList.108_3 = pxDelayedTaskList;
  _4 = pxDelayedTaskList.108_3->xListEnd.pxNext;
  _5 = _4->xItemValue;
  xNextTaskUnblockTime = _5;

  <bb 5> :
  return;

}


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

}


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

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

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

  <bb 4> :
  iftmp.106 = xTask;

  <bb 5> :
  pxTCB = iftmp.106;
  pucEndOfStack = pxTCB->pxStack;
  _1 = prvTaskCheckFreeStackSpace (pucEndOfStack);
  uxReturn = (UBaseType_t) _1;
  D.8007 = uxReturn;

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

}


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

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

  <bb 3> :
  pucStackByte = pucStackByte + 1;
  ulCount = ulCount + 1;

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

  <bb 5> :
  ulCount = ulCount / 4;
  D.8001 = (uint16_t) ulCount;

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

}


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.7999;

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

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

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

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

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

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

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

  <bb 9> :
  D.7999 = uxTask;

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

}


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

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

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

  <bb 4> :
  iftmp.104 = xTask;

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

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

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

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

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

  <bb 10> :
  pxTaskStatus->eCurrentState = 2;

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

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

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

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

  <bb 15> :
  pxTaskStatus->usStackHighWaterMark = 0;

  <bb 16> :
  return;

}


prvCheckTasksWaitingTermination ()
{
  struct TCB_t * pxTCB;

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

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

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

  <bb 5> :
  return;

}


prvInitialiseTaskLists ()
{
  UBaseType_t uxPriority;

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

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

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

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

}


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

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

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

}


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

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

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

  <bb 4> :
  return;

}


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

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

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

  <bb 4> :
  uxReturn = 0;

  <bb 5> :
  D.7968 = uxReturn;

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

}


vTaskMissedYield ()
{
  <bb 2> :
  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.7963;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

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

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

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

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

  <bb 12> :
  _6 = pxTimeOut->xOverflowCount;
  xNumOfOverflows.100_7 = xNumOfOverflows;
  if (_6 != xNumOfOverflows.100_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> :
  xReturn = 1;
  *pxTicksToWait = 0;
  goto <bb 18>; [INV]

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

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

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

  <bb 18> :
  vPortExitCritical ();
  D.7963 = xReturn;

  <bb 19> :
<L19>:
  return D.7963;

}


vTaskInternalSetTimeOutState (struct TimeOut_t * const pxTimeOut)
{
  <bb 2> :
  xNumOfOverflows.96_1 = xNumOfOverflows;
  pxTimeOut->xOverflowCount = xNumOfOverflows.96_1;
  xTickCount.97_2 = xTickCount;
  pxTimeOut->xTimeOnEntering = xTickCount.97_2;
  return;

}


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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  vPortEnterCritical ();
  xNumOfOverflows.94_1 = xNumOfOverflows;
  pxTimeOut->xOverflowCount = xNumOfOverflows.94_1;
  xTickCount.95_2 = xTickCount;
  pxTimeOut->xTimeOnEntering = xTickCount.95_2;
  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> :
  uxSchedulerSuspended.91_1 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.91_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

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

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

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

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

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

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

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

  <bb 15> :
  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.7930;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

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

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

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

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

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

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

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

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

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

  <bb 16> :
  xReturn = 0;

  <bb 17> :
  D.7930 = xReturn;

  <bb 18> :
<L15>:
  return D.7930;

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  pxIndex = pxEventList->pxIndex;
  pxCurrentTCB.83_1 = pxCurrentTCB;
  pxCurrentTCB.83_1->xEventListItem.pxNext = pxIndex;
  pxCurrentTCB.84_2 = pxCurrentTCB;
  _3 = pxIndex->pxPrevious;
  pxCurrentTCB.84_2->xEventListItem.pxPrevious = _3;
  pxCurrentTCB.85_4 = pxCurrentTCB;
  _5 = pxIndex->pxPrevious;
  _6 = &pxCurrentTCB.85_4->xEventListItem;
  _5->pxNext = _6;
  pxCurrentTCB.86_7 = pxCurrentTCB;
  _8 = &pxCurrentTCB.86_7->xEventListItem;
  pxIndex->pxPrevious = _8;
  pxCurrentTCB.87_9 = pxCurrentTCB;
  pxCurrentTCB.87_9->xEventListItem.pvContainer = pxEventList;
  _10 = pxEventList->uxNumberOfItems;
  _11 = _10 + 1;
  pxEventList->uxNumberOfItems = _11;
  if (xWaitIndefinitely != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  xTicksToWait = 4294967295;

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

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

  <bb 8> :
  pxCurrentTCB.77_2 = pxCurrentTCB;
  _3 = xItemValue | 2147483648;
  pxCurrentTCB.77_2->xEventListItem.xItemValue = _3;
  pxIndex = pxEventList->pxIndex;
  pxCurrentTCB.78_4 = pxCurrentTCB;
  pxCurrentTCB.78_4->xEventListItem.pxNext = pxIndex;
  pxCurrentTCB.79_5 = pxCurrentTCB;
  _6 = pxIndex->pxPrevious;
  pxCurrentTCB.79_5->xEventListItem.pxPrevious = _6;
  pxCurrentTCB.80_7 = pxCurrentTCB;
  _8 = pxIndex->pxPrevious;
  _9 = &pxCurrentTCB.80_7->xEventListItem;
  _8->pxNext = _9;
  pxCurrentTCB.81_10 = pxCurrentTCB;
  _11 = &pxCurrentTCB.81_10->xEventListItem;
  pxIndex->pxPrevious = _11;
  pxCurrentTCB.82_12 = pxCurrentTCB;
  pxCurrentTCB.82_12->xEventListItem.pvContainer = pxEventList;
  _13 = pxEventList->uxNumberOfItems;
  _14 = _13 + 1;
  pxEventList->uxNumberOfItems = _14;
  prvAddCurrentTaskToDelayedList (xTicksToWait, 1);
  return;

}


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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

}


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

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

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

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

  <bb 8> :
  uxTopPriority = uxTopPriority + 4294967295;

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

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

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

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

  <bb 13> :
  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.7897;

  <bb 2> :
  xSwitchRequired = 0;
  uxSchedulerSuspended.61_1 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.61_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 28>; [INV]

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

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

  <bb 5> :
  vPortRaiseBASEPRI ();

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

  <bb 7> :
  pxTemp = pxDelayedTaskList;
  pxOverflowDelayedTaskList.64_5 = pxOverflowDelayedTaskList;
  pxDelayedTaskList = pxOverflowDelayedTaskList.64_5;
  pxOverflowDelayedTaskList = pxTemp;
  xNumOfOverflows.65_6 = xNumOfOverflows;
  _7 = xNumOfOverflows.65_6 + 1;
  xNumOfOverflows = _7;
  prvResetNextTaskUnblockTime ();

  <bb 8> :
  xNextTaskUnblockTime.66_8 = xNextTaskUnblockTime;
  if (xConstTickCount >= xNextTaskUnblockTime.66_8)
    goto <bb 9>; [INV]
  else
    goto <bb 24>; [INV]

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

  <bb 10> :
  xNextTaskUnblockTime = 4294967295;
  goto <bb 24>; [INV]

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

  <bb 12> :
  xNextTaskUnblockTime = xItemValue;
  goto <bb 24>; [INV]

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

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

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

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

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

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

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

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

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

  <bb 22> :
  xSwitchRequired = 1;

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

  <bb 24> :
  pxCurrentTCB.71_48 = pxCurrentTCB;
  _49 = pxCurrentTCB.71_48->uxPriority;
  _50 = pxReadyTasksLists[_49].uxNumberOfItems;
  if (_50 > 1)
    goto <bb 25>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 25> :
  xSwitchRequired = 1;

  <bb 26> :
  xYieldPending.72_51 = xYieldPending;
  if (xYieldPending.72_51 != 0)
    goto <bb 27>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 27> :
  xSwitchRequired = 1;
  goto <bb 29>; [INV]

  <bb 28> :
  xPendedTicks.73_52 = xPendedTicks;
  _53 = xPendedTicks.73_52 + 1;
  xPendedTicks = _53;

  <bb 29> :
  D.7897 = xSwitchRequired;

  <bb 30> :
<L35>:
  return D.7897;

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

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

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

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

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

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

  <bb 12> :
  xReturn = 0;

  <bb 13> :
  xTaskResumeAll ();
  D.7863 = xReturn;

  <bb 14> :
<L14>:
  return D.7863;

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  vTaskSuspendAll ();
  xPendedTicks.58_2 = xPendedTicks;
  _3 = xTicksToCatchUp + xPendedTicks.58_2;
  xPendedTicks = _3;
  xYieldOccurred = xTaskResumeAll ();
  D.7848 = xYieldOccurred;

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

}


uxTaskGetSystemState (struct TaskStatus_t * const pxTaskStatusArray, const UBaseType_t uxArraySize, uint32_t * const pulTotalRunTime)
{
  UBaseType_t uxQueue;
  UBaseType_t uxTask;
  UBaseType_t D.7844;
  long unsigned int D.7840;
  long unsigned int D.7839;
  long unsigned int D.7838;
  long unsigned int D.7837;
  long unsigned int D.7836;

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

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

  <bb 4> :
  _5 = uxTask * 36;
  _6 = pxTaskStatusArray + _5;
  pxDelayedTaskList.55_7 = pxDelayedTaskList;
  D.7837 = prvListTasksWithinSingleList (_6, pxDelayedTaskList.55_7, 2);
  uxTask = D.7837 + uxTask;
  _8 = uxTask * 36;
  _9 = pxTaskStatusArray + _8;
  pxOverflowDelayedTaskList.56_10 = pxOverflowDelayedTaskList;
  D.7838 = prvListTasksWithinSingleList (_9, pxOverflowDelayedTaskList.56_10, 2);
  uxTask = D.7838 + uxTask;
  _11 = uxTask * 36;
  _12 = pxTaskStatusArray + _11;
  D.7839 = prvListTasksWithinSingleList (_12, &xTasksWaitingTermination, 4);
  uxTask = D.7839 + uxTask;
  _13 = uxTask * 36;
  _14 = pxTaskStatusArray + _13;
  D.7840 = prvListTasksWithinSingleList (_14, &xSuspendedTaskList, 3);
  uxTask = D.7840 + uxTask;
  if (pulTotalRunTime != 0B)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  *pulTotalRunTime = 0;

  <bb 6> :
  xTaskResumeAll ();
  D.7844 = uxTask;

  <bb 7> :
<L7>:
  return D.7844;

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  vTaskSuspendAll ();

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

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

  <bb 8> :
  if (uxQueue != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 9>; [INV]

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

  <bb 10> :
  pxDelayedTaskList.52_3 = pxDelayedTaskList;
  pxTCB = prvSearchForNameWithinSingleList (pxDelayedTaskList.52_3, pcNameToQuery);

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

  <bb 12> :
  pxOverflowDelayedTaskList.53_4 = pxOverflowDelayedTaskList;
  pxTCB = prvSearchForNameWithinSingleList (pxOverflowDelayedTaskList.53_4, pcNameToQuery);

  <bb 13> :
  if (pxTCB == 0B)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  pxTCB = prvSearchForNameWithinSingleList (&xSuspendedTaskList, pcNameToQuery);

  <bb 15> :
  if (pxTCB == 0B)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  pxTCB = prvSearchForNameWithinSingleList (&xTasksWaitingTermination, pcNameToQuery);

  <bb 17> :
  xTaskResumeAll ();
  D.7832 = pxTCB;

  <bb 18> :
<L15>:
  return D.7832;

}


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.7818;

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

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

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

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

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

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

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

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

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

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

  <bb 12> :
  pxReturn = pxNextTCB;
  xBreakLoop = 1;

  <bb 13> :
  if (xBreakLoop != 0)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

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

  <bb 15> :
  x = x + 1;

  <bb 16> :
  if (x <= 9)
    goto <bb 9>; [INV]
  else
    goto <bb 17>; [INV]

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

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

  <bb 19> :
  if (pxNextTCB != pxFirstTCB)
    goto <bb 6>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 20> :

  <bb 21> :
  D.7818 = pxReturn;

  <bb 22> :
<L22>:
  return D.7818;

}


pcTaskGetName (struct tskTaskControlBlock * xTaskToQuery)
{
  struct TCB_t * pxTCB;
  char * D.7799;
  struct TCB_t * iftmp.51;

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

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

  <bb 4> :
  iftmp.51 = xTaskToQuery;

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

  <bb 8> :
  D.7799 = &pxTCB->pcTaskName[0];

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

}


uxTaskGetNumberOfTasks ()
{
  UBaseType_t D.7791;

  <bb 2> :
  D.7791 = uxCurrentNumberOfTasks;

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

}


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

  <bb 2> :
  vPortValidateInterruptPriority ();
  uxSavedInterruptStatus = 0;
  xReturn = xTickCount;
  D.7789 = xReturn;

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

}


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

  <bb 2> :
  xTicks = xTickCount;
  D.7787 = xTicks;

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

}


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.7785;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  vPortEnterCritical ();
  uxSchedulerSuspended.45_2 = uxSchedulerSuspended;
  _3 = uxSchedulerSuspended.45_2 + 4294967295;
  uxSchedulerSuspended = _3;
  uxSchedulerSuspended.46_4 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.46_4 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 6> :
  uxCurrentNumberOfTasks.47_5 = uxCurrentNumberOfTasks;
  if (uxCurrentNumberOfTasks.47_5 != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 26>; [INV]

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

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

  <bb 9> :
  _13 = pxTCB->xEventListItem.pxPrevious;
  pxList->pxIndex = _13;

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

  <bb 11> :
  _22 = pxTCB->xStateListItem.pxPrevious;
  pxList->pxIndex = _22;

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

  <bb 13> :
  _27 = pxTCB->uxPriority;
  uxTopReadyPriority = _27;

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

  <bb 15> :
  xYieldPending = 1;

  <bb 16> :
  _41 = xPendingReadyList.uxNumberOfItems;
  if (_41 != 0)
    goto <bb 8>; [INV]
  else
    goto <bb 17>; [INV]

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

  <bb 18> :
  prvResetNextTaskUnblockTime ();

  <bb 19> :
  xPendedCounts = xPendedTicks;
  if (xPendedCounts != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 24>; [INV]

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

  <bb 21> :
  xYieldPending = 1;

  <bb 22> :
  xPendedCounts = xPendedCounts + 4294967295;
  if (xPendedCounts != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 23> :
  xPendedTicks = 0;

  <bb 24> :
  xYieldPending.50_43 = xYieldPending;
  if (xYieldPending.50_43 != 0)
    goto <bb 25>; [INV]
  else
    goto <bb 26>; [INV]

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

  <bb 26> :
  vPortExitCritical ();
  D.7785 = xAlreadyYielded;

  <bb 27> :
<L33>:
  return D.7785;

}


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

}


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

}


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

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

  <bb 3> :
  xReturn = xTimerCreateTimerTask ();

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

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

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

  <bb 7> :
  vPortRaiseBASEPRI ();

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

  <bb 9> :
  vol.42 = 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.7744;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

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

  <bb 8> :
  xYieldRequired = 1;
  xYieldPending = 1;

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

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

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

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

  <bb 13> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.7744 = xYieldRequired;

  <bb 14> :
<L14>:
  return D.7744;

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  pxCurrentTCB.36_1 = pxCurrentTCB;
  if (pxTCB != pxCurrentTCB.36_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> :
  vPortEnterCritical ();
  _2 = prvTaskIsTaskSuspended (pxTCB);
  if (_2 != 0)
    goto <bb 8>; [INV]
  else
    goto <bb 12>; [INV]

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

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

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

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

  <bb 12> :
  vPortExitCritical ();

  <bb 13> :
  return;

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

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

  <bb 8> :
  xReturn = 1;

  <bb 9> :
  D.7714 = xReturn;

  <bb 10> :
<L12>:
  return D.7714;

}


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

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

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

  <bb 4> :
  iftmp.30 = xTaskToSuspend;

  <bb 5> :
  pxTCB = iftmp.30;
  _1 = &pxTCB->xStateListItem;
  _2 = uxListRemove (_1);

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

  <bb 7> :
  _4 = &pxTCB->xEventListItem;
  uxListRemove (_4);

  <bb 8> :
  _5 = &pxTCB->xStateListItem;
  vListInsertEnd (&xSuspendedTaskList, _5);
  x = 0;
  goto <bb 12>; [INV]

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

  <bb 10> :
  pxTCB->ucNotifyState[x] = 0;

  <bb 11> :
  x = x + 1;

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

  <bb 13> :
  vPortExitCritical ();
  xSchedulerRunning.31_7 = xSchedulerRunning;
  if (xSchedulerRunning.31_7 != 0)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  vPortEnterCritical ();
  prvResetNextTaskUnblockTime ();
  vPortExitCritical ();

  <bb 15> :
  pxCurrentTCB.32_8 = pxCurrentTCB;
  if (pxTCB == pxCurrentTCB.32_8)
    goto <bb 16>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 16> :
  xSchedulerRunning.33_9 = xSchedulerRunning;
  if (xSchedulerRunning.33_9 != 0)
    goto <bb 17>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 17> :
  uxSchedulerSuspended.34_10 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.34_10 != 0)
    goto <bb 18>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 18> :
  vPortRaiseBASEPRI ();

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

  <bb 20> :
  _11 = 3758157060B;
  *_11 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 24>; [INV]

  <bb 21> :
  _12 = xSuspendedTaskList.uxNumberOfItems;
  uxCurrentNumberOfTasks.35_13 = uxCurrentNumberOfTasks;
  if (_12 == uxCurrentNumberOfTasks.35_13)
    goto <bb 22>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 22> :
  pxCurrentTCB = 0B;
  goto <bb 24>; [INV]

  <bb 23> :
  vTaskSwitchContext ();

  <bb 24> :
  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.25;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  uxNewPriority = 4;

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

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

  <bb 9> :
  iftmp.25 = xTask;

  <bb 10> :
  pxTCB = iftmp.25;
  uxCurrentBasePriority = pxTCB->uxBasePriority;
  if (uxCurrentBasePriority != uxNewPriority)
    goto <bb 11>; [INV]
  else
    goto <bb 28>; [INV]

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

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

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

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

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

  <bb 16> :
  xYieldRequired = 1;

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

  <bb 18> :
  pxTCB->uxPriority = uxNewPriority;

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

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

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

  <bb 22> :
  _12 = &pxTCB->xStateListItem;
  _13 = uxListRemove (_12);

  <bb 23> :
  _14 = pxTCB->uxPriority;
  uxTopReadyPriority.29_15 = uxTopReadyPriority;
  if (_14 > uxTopReadyPriority.29_15)
    goto <bb 24>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 24> :
  _16 = pxTCB->uxPriority;
  uxTopReadyPriority = _16;

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

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

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

  <bb 28> :
  vPortExitCritical ();
  return;

}


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

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

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

  <bb 4> :
  iftmp.24 = xTask;

  <bb 5> :
  pxTCB = iftmp.24;
  uxReturn = pxTCB->uxPriority;
  vPortSetBASEPRI (uxSavedInterruptState);
  D.7633 = uxReturn;

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

}


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

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

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

  <bb 4> :
  iftmp.23 = xTask;

  <bb 5> :
  pxTCB = iftmp.23;
  uxReturn = pxTCB->uxPriority;
  vPortExitCritical ();
  D.7627 = uxReturn;

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

}


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.7621;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  eReturn = 0;
  goto <bb 23>; [INV]

  <bb 7> :
  vPortEnterCritical ();
  pxStateList = pxTCB->xStateListItem.pvContainer;
  pxDelayedList = pxDelayedTaskList;
  pxOverflowedDelayedList = pxOverflowDelayedTaskList;
  vPortExitCritical ();
  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> :
  eReturn = 2;
  goto <bb 23>; [INV]

  <bb 10> :
  if (pxStateList == &xSuspendedTaskList)
    goto <bb 11>; [INV]
  else
    goto <bb 19>; [INV]

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

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

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

  <bb 14> :
  eReturn = 2;
  goto <bb 17>; [INV]

  <bb 15> :
  x = x + 1;

  <bb 16> :
  if (x <= 0)
    goto <bb 13>; [INV]
  else
    goto <bb 17>; [INV]

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

  <bb 18> :
  eReturn = 2;
  goto <bb 23>; [INV]

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

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

  <bb 21> :
  eReturn = 4;
  goto <bb 23>; [INV]

  <bb 22> :
  eReturn = 1;

  <bb 23> :
  D.7621 = eReturn;

  <bb 24> :
<L25>:
  return D.7621;

}


vTaskDelay (const TickType_t xTicksToDelay)
{
  BaseType_t xAlreadyYielded;

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

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

  <bb 4> :
  vPortRaiseBASEPRI ();

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

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

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

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

  <bb 9> :
  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> :
  xShouldDelay = 0;
  if (pxPreviousWakeTime == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

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

  <bb 9> :
  vPortRaiseBASEPRI ();

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

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

  <bb 12> :
  _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> :
  xShouldDelay = 1;
  goto <bb 18>; [INV]

  <bb 15> :
  _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> :
  xShouldDelay = 1;

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

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

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

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

  <bb 22> :
  D.7590 = xShouldDelay;

  <bb 23> :
<L26>:
  return D.7590;

}


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

  <bb 2> :
  vPortEnterCritical ();
  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;
  _1 = &pxTCB->xStateListItem;
  _2 = uxListRemove (_1);

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

  <bb 7> :
  _4 = &pxTCB->xEventListItem;
  uxListRemove (_4);

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

  <bb 9> :
  _8 = &pxTCB->xStateListItem;
  vListInsertEnd (&xTasksWaitingTermination, _8);
  uxDeletedTasksWaitingCleanUp.15_9 = uxDeletedTasksWaitingCleanUp;
  _10 = uxDeletedTasksWaitingCleanUp.15_9 + 1;
  uxDeletedTasksWaitingCleanUp = _10;
  goto <bb 11>; [INV]

  <bb 10> :
  uxCurrentNumberOfTasks.16_11 = uxCurrentNumberOfTasks;
  _12 = uxCurrentNumberOfTasks.16_11 + 4294967295;
  uxCurrentNumberOfTasks = _12;
  prvDeleteTCB (pxTCB);
  prvResetNextTaskUnblockTime ();

  <bb 11> :
  vPortExitCritical ();
  xSchedulerRunning.17_13 = xSchedulerRunning;
  if (xSchedulerRunning.17_13 != 0)
    goto <bb 12>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 12> :
  pxCurrentTCB.18_14 = pxCurrentTCB;
  if (pxTCB == pxCurrentTCB.18_14)
    goto <bb 13>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 13> :
  uxSchedulerSuspended.19_15 = uxSchedulerSuspended;
  if (uxSchedulerSuspended.19_15 != 0)
    goto <bb 14>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 14> :
  vPortRaiseBASEPRI ();

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

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

  <bb 17> :
  return;

}


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

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

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

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

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

  <bb 6> :
  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> :
  pxCurrentTCB = pxNewTCB;

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

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

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

  <bb 11> :
  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> :
  _29 = 3758157060B;
  *_29 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");

  <bb 13> :
  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> :
  _1 = pxNewTCB->pxStack;
  _2 = ulStackDepth * 4;
  memset (_1, 165, _2);
  _3 = pxNewTCB->pxStack;
  _4 = ulStackDepth + 1073741823;
  _5 = _4 * 4;
  pxTopOfStack = _3 + _5;
  pxTopOfStack.0_6 = (long unsigned int) pxTopOfStack;
  _7 = pxTopOfStack.0_6 & 4294967288;
  pxTopOfStack = (StackType_t *) _7;
  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> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  pxNewTCB->pxEndOfStack = pxTopOfStack;
  if (pcName != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 6> :
  x = 0;
  goto <bb 10>; [INV]

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

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

  <bb 9> :
  x = x + 1;

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

  <bb 11> :
  pxNewTCB->pcTaskName[9] = 0;
  goto <bb 13>; [INV]

  <bb 12> :
  pxNewTCB->pcTaskName[0] = 0;

  <bb 13> :
  if (uxPriority > 4)
    goto <bb 14>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 14> :
  vPortRaiseBASEPRI ();

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

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

  <bb 17> :
  uxPriority = 4;

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

  <bb 19> :
  *pxCreatedTask = pxNewTCB;

  <bb 20> :
  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.7510;

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

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

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

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

  <bb 6> :
  pxNewTCB = 0B;

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

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

  <bb 9> :
  xReturn = -1;

  <bb 10> :
  D.7510 = xReturn;

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

}


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

}


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

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

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

}


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

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

}