prvAddCurrentTaskToDelayedList (TickType_t xTicksToWait, const BaseType_t xCanBlockIndefinitely)
{
  struct ListItem_t * const pxIndex;
  const TickType_t xConstTickCount;
  TickType_t xTimeToWake;
  struct TCB_t * pxCurrentTCB.23_1;
  struct TCB_t * pxCurrentTCB.24_2;
  struct ListItem_t * _3;
  long unsigned int _4;
  struct TCB_t * pxCurrentTCB.25_5;
  struct TCB_t * pxCurrentTCB.26_6;
  struct xLIST_ITEM * _7;
  struct TCB_t * pxCurrentTCB.27_8;
  struct xLIST_ITEM * _9;
  struct ListItem_t * _10;
  struct TCB_t * pxCurrentTCB.28_11;
  struct ListItem_t * _12;
  struct TCB_t * pxCurrentTCB.29_13;
  long unsigned int _14;
  long unsigned int _15;
  struct TCB_t * pxCurrentTCB.30_16;
  struct List_t * pxOverflowDelayedTaskList.31_17;
  struct TCB_t * pxCurrentTCB.32_18;
  struct ListItem_t * _19;
  struct List_t * pxDelayedTaskList.33_20;
  struct TCB_t * pxCurrentTCB.34_21;
  struct ListItem_t * _22;
  long unsigned int xNextTaskUnblockTime.35_23;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  xTimeToWake_38 = xConstTickCount_26 + xTicksToWait_29(D);
  # DEBUG xTimeToWake => xTimeToWake_38
  # DEBUG BEGIN_STMT
  pxCurrentTCB.30_16 ={v} pxCurrentTCB;
  pxCurrentTCB.30_16->xStateListItem.xItemValue = xTimeToWake_38;
  # DEBUG BEGIN_STMT
  if (xTimeToWake_38 < xConstTickCount_26)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

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

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  xNextTaskUnblockTime ={v} xTimeToWake_38;

  <bb 9> :
  # DEBUG BEGIN_STMT
  return;

}


ulTaskGenericNotifyValueClear (struct tskTaskControlBlock * xTask, UBaseType_t uxIndexToClear, uint32_t ulBitsToClear)
{
  uint32_t ulReturn;
  struct TCB_t * pxTCB;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  struct TCB_t * iftmp.164_4;
  struct TCB_t * iftmp.164_6;
  struct TCB_t * iftmp.164_8;
  uint32_t _16;

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

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

  <bb 4> :
  iftmp.164_6 = xTask_5(D);

  <bb 5> :
  # iftmp.164_4 = PHI <iftmp.164_8(3), iftmp.164_6(4)>
  pxTCB_9 = iftmp.164_4;
  # DEBUG pxTCB => pxTCB_9
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  ulReturn_12 ={v} pxTCB_9->ulNotifiedValue[uxIndexToClear_11(D)];
  # DEBUG ulReturn => ulReturn_12
  # DEBUG BEGIN_STMT
  _1 ={v} pxTCB_9->ulNotifiedValue[uxIndexToClear_11(D)];
  _2 = ~ulBitsToClear_13(D);
  _3 = _1 & _2;
  pxTCB_9->ulNotifiedValue[uxIndexToClear_11(D)] ={v} _3;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _16 = ulReturn_12;
  return _16;

}


xTaskGenericNotifyStateClear (struct tskTaskControlBlock * xTask, UBaseType_t uxIndexToClear)
{
  BaseType_t xReturn;
  struct TCB_t * pxTCB;
  unsigned char _1;
  struct TCB_t * iftmp.163_3;
  struct TCB_t * iftmp.163_7;
  struct TCB_t * iftmp.163_9;
  BaseType_t _16;

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

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

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

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

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

  <bb 7> :
  iftmp.163_7 = xTask_6(D);

  <bb 8> :
  # iftmp.163_3 = PHI <iftmp.163_9(6), iftmp.163_7(7)>
  pxTCB_10 = iftmp.163_3;
  # DEBUG pxTCB => pxTCB_10
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _1 ={v} pxTCB_10->ucNotifyState[uxIndexToClear_5(D)];
  if (_1 == 2)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxTCB_10->ucNotifyState[uxIndexToClear_5(D)] ={v} 0;
  # DEBUG BEGIN_STMT
  xReturn_14 = 1;
  # DEBUG xReturn => xReturn_14
  goto <bb 11>; [INV]

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

  <bb 11> :
  # xReturn_2 = PHI <xReturn_14(9), xReturn_12(10)>
  # DEBUG xReturn => xReturn_2
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _16 = xReturn_2;
  return _16;

}


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;
  long unsigned int _1;
  long unsigned int _2;
  struct xLIST * _3;
  long unsigned int uxSchedulerSuspended.160_4;
  struct xLIST_ITEM * _5;
  struct xLIST_ITEM * _6;
  struct xLIST_ITEM * _7;
  struct xLIST_ITEM * _8;
  struct ListItem_t * _9;
  struct ListItem_t * _10;
  struct xLIST_ITEM * _11;
  long unsigned int _12;
  long unsigned int _13;
  long unsigned int _14;
  long unsigned int uxTopReadyPriority.161_15;
  long unsigned int _16;
  long unsigned int _17;
  struct xLIST_ITEM * _18;
  struct xLIST_ITEM * _19;
  struct ListItem_t * _20;
  struct ListItem_t * _21;
  long unsigned int _22;
  struct List_t * _23;
  long unsigned int _24;
  long unsigned int _25;
  long unsigned int _26;
  struct xLIST_ITEM * _27;
  struct xLIST_ITEM * _28;
  struct ListItem_t * _29;
  struct ListItem_t * _30;
  long unsigned int _31;
  long unsigned int _32;
  long unsigned int _33;
  struct TCB_t * pxCurrentTCB.162_34;
  long unsigned int _35;

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

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

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

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

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

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  pxTCB_45 = xTaskToNotify_41(D);
  # DEBUG pxTCB => pxTCB_45
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus_47 = ulPortRaiseBASEPRI ();
  # DEBUG uxSavedInterruptStatus => uxSavedInterruptStatus_47
  # DEBUG BEGIN_STMT
  ucOriginalNotifyState_48 ={v} pxTCB_45->ucNotifyState[uxIndexToNotify_42(D)];
  # DEBUG ucOriginalNotifyState => ucOriginalNotifyState_48
  # DEBUG BEGIN_STMT
  pxTCB_45->ucNotifyState[uxIndexToNotify_42(D)] ={v} 2;
  # DEBUG BEGIN_STMT
  _1 ={v} pxTCB_45->ulNotifiedValue[uxIndexToNotify_42(D)];
  _2 = _1 + 1;
  pxTCB_45->ulNotifiedValue[uxIndexToNotify_42(D)] ={v} _2;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (ucOriginalNotifyState_48 == 1)
    goto <bb 9>; [INV]
  else
    goto <bb 23>; [INV]

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

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

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

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

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

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

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

  <bb 16> :
  # DEBUG BEGIN_STMT
  _16 = pxTCB_45->uxPriority;
  uxTopReadyPriority ={v} _16;

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

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

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

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

  <bb 21> :
  # DEBUG BEGIN_STMT
  *pxHigherPriorityTaskWoken_72(D) = 1;

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

  <bb 23> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptStatus_47);
  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;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  long unsigned int xTickCount.156_6;
  struct xLIST * _7;
  long unsigned int uxSchedulerSuspended.157_8;
  struct xLIST_ITEM * _9;
  struct xLIST_ITEM * _10;
  struct xLIST_ITEM * _11;
  struct xLIST_ITEM * _12;
  struct ListItem_t * _13;
  struct ListItem_t * _14;
  struct xLIST_ITEM * _15;
  long unsigned int _16;
  long unsigned int _17;
  long unsigned int _18;
  long unsigned int uxTopReadyPriority.158_19;
  long unsigned int _20;
  long unsigned int _21;
  struct xLIST_ITEM * _22;
  struct xLIST_ITEM * _23;
  struct ListItem_t * _24;
  struct ListItem_t * _25;
  long unsigned int _26;
  struct List_t * _27;
  long unsigned int _28;
  long unsigned int _29;
  long unsigned int _30;
  struct xLIST_ITEM * _31;
  struct xLIST_ITEM * _32;
  struct ListItem_t * _33;
  struct ListItem_t * _34;
  long unsigned int _35;
  long unsigned int _36;
  long unsigned int _37;
  struct TCB_t * pxCurrentTCB.159_38;
  long unsigned int _39;
  BaseType_t _94;

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

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

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

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

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

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  pxTCB_53 = xTaskToNotify_49(D);
  # DEBUG pxTCB => pxTCB_53
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus_55 = ulPortRaiseBASEPRI ();
  # DEBUG uxSavedInterruptStatus => uxSavedInterruptStatus_55
  # DEBUG BEGIN_STMT
  if (pulPreviousNotificationValue_56(D) != 0B)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  _1 ={v} pxTCB_53->ulNotifiedValue[uxIndexToNotify_50(D)];
  *pulPreviousNotificationValue_56(D) = _1;

  <bb 10> :
  # DEBUG BEGIN_STMT
  ucOriginalNotifyState_58 ={v} pxTCB_53->ucNotifyState[uxIndexToNotify_50(D)];
  # DEBUG ucOriginalNotifyState => ucOriginalNotifyState_58
  # DEBUG BEGIN_STMT
  pxTCB_53->ucNotifyState[uxIndexToNotify_50(D)] ={v} 2;
  # DEBUG BEGIN_STMT
  switch (eAction_60(D)) <default: <L16> [INV], case 0: <L39> [INV], case 1: <L8> [INV], case 2: <L9> [INV], case 3: <L10> [INV], case 4: <L11> [INV]>

  <bb 11> :
<L8>:
  # DEBUG BEGIN_STMT
  _2 ={v} pxTCB_53->ulNotifiedValue[uxIndexToNotify_50(D)];
  _3 = ulValue_62(D) | _2;
  pxTCB_53->ulNotifiedValue[uxIndexToNotify_50(D)] ={v} _3;
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

  <bb 12> :
<L9>:
  # DEBUG BEGIN_STMT
  _4 ={v} pxTCB_53->ulNotifiedValue[uxIndexToNotify_50(D)];
  _5 = _4 + 1;
  pxTCB_53->ulNotifiedValue[uxIndexToNotify_50(D)] ={v} _5;
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

  <bb 13> :
<L10>:
  # DEBUG BEGIN_STMT
  pxTCB_53->ulNotifiedValue[uxIndexToNotify_50(D)] ={v} ulValue_62(D);
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

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

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxTCB_53->ulNotifiedValue[uxIndexToNotify_50(D)] ={v} ulValue_62(D);
  goto <bb 20>; [INV]

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

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

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

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

  <bb 20> :
  # xReturn_40 = PHI <xReturn_48(11), xReturn_48(12), xReturn_48(13), xReturn_61(16), xReturn_48(10), xReturn_48(17), xReturn_48(15)>
<L39>:
  # DEBUG xReturn => xReturn_40
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (ucOriginalNotifyState_58 == 1)
    goto <bb 21>; [INV]
  else
    goto <bb 35>; [INV]

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

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

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

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

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

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

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

  <bb 28> :
  # DEBUG BEGIN_STMT
  _20 = pxTCB_53->uxPriority;
  uxTopReadyPriority ={v} _20;

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

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

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

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

  <bb 33> :
  # DEBUG BEGIN_STMT
  *pxHigherPriorityTaskWoken_89(D) = 1;

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

  <bb 35> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptStatus_55);
  # DEBUG BEGIN_STMT
  _94 = xReturn_40;
  return _94;

}


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;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  long unsigned int xTickCount.153_6;
  struct xLIST_ITEM * _7;
  struct xLIST_ITEM * _8;
  struct xLIST_ITEM * _9;
  struct xLIST_ITEM * _10;
  struct ListItem_t * _11;
  struct ListItem_t * _12;
  struct xLIST_ITEM * _13;
  long unsigned int _14;
  long unsigned int _15;
  long unsigned int _16;
  long unsigned int uxTopReadyPriority.154_17;
  long unsigned int _18;
  long unsigned int _19;
  struct xLIST_ITEM * _20;
  struct xLIST_ITEM * _21;
  struct ListItem_t * _22;
  struct ListItem_t * _23;
  long unsigned int _24;
  struct List_t * _25;
  long unsigned int _26;
  long unsigned int _27;
  long unsigned int _28;
  struct xLIST * _29;
  long unsigned int _30;
  struct TCB_t * pxCurrentTCB.155_31;
  long unsigned int _32;
  volatile uint32_t * _33;
  BaseType_t _77;

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

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

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

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

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

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

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  _1 ={v} pxTCB_43->ulNotifiedValue[uxIndexToNotify_41(D)];
  *pulPreviousNotificationValue_46(D) = _1;

  <bb 10> :
  # DEBUG BEGIN_STMT
  ucOriginalNotifyState_48 ={v} pxTCB_43->ucNotifyState[uxIndexToNotify_41(D)];
  # DEBUG ucOriginalNotifyState => ucOriginalNotifyState_48
  # DEBUG BEGIN_STMT
  pxTCB_43->ucNotifyState[uxIndexToNotify_41(D)] ={v} 2;
  # DEBUG BEGIN_STMT
  switch (eAction_50(D)) <default: <L16> [INV], case 0: <L35> [INV], case 1: <L8> [INV], case 2: <L9> [INV], case 3: <L10> [INV], case 4: <L11> [INV]>

  <bb 11> :
<L8>:
  # DEBUG BEGIN_STMT
  _2 ={v} pxTCB_43->ulNotifiedValue[uxIndexToNotify_41(D)];
  _3 = ulValue_52(D) | _2;
  pxTCB_43->ulNotifiedValue[uxIndexToNotify_41(D)] ={v} _3;
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

  <bb 12> :
<L9>:
  # DEBUG BEGIN_STMT
  _4 ={v} pxTCB_43->ulNotifiedValue[uxIndexToNotify_41(D)];
  _5 = _4 + 1;
  pxTCB_43->ulNotifiedValue[uxIndexToNotify_41(D)] ={v} _5;
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

  <bb 13> :
<L10>:
  # DEBUG BEGIN_STMT
  pxTCB_43->ulNotifiedValue[uxIndexToNotify_41(D)] ={v} ulValue_52(D);
  # DEBUG BEGIN_STMT
  goto <bb 20>; [INV]

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

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxTCB_43->ulNotifiedValue[uxIndexToNotify_41(D)] ={v} ulValue_52(D);
  goto <bb 20>; [INV]

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

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

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

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

  <bb 20> :
  # xReturn_34 = PHI <xReturn_40(11), xReturn_40(12), xReturn_40(13), xReturn_51(16), xReturn_40(10), xReturn_40(17), xReturn_40(15)>
<L35>:
  # DEBUG xReturn => xReturn_34
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (ucOriginalNotifyState_48 == 1)
    goto <bb 21>; [INV]
  else
    goto <bb 30>; [INV]

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

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

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

  <bb 24> :
  # DEBUG BEGIN_STMT
  _18 = pxTCB_43->uxPriority;
  uxTopReadyPriority ={v} _18;

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

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

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

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

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

  <bb 30> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _77 = xReturn_34;
  return _77;

}


xTaskGenericNotifyWait (UBaseType_t uxIndexToWait, uint32_t ulBitsToClearOnEntry, uint32_t ulBitsToClearOnExit, uint32_t * pulNotificationValue, TickType_t xTicksToWait)
{
  BaseType_t xReturn;
  struct TCB_t * pxCurrentTCB.146_1;
  unsigned char _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  struct TCB_t * pxCurrentTCB.148_6;
  volatile uint32_t * _7;
  struct TCB_t * pxCurrentTCB.149_8;
  long unsigned int _9;
  struct TCB_t * pxCurrentTCB.150_10;
  unsigned char _11;
  long unsigned int _12;
  long unsigned int _13;
  long unsigned int _14;
  struct TCB_t * pxCurrentTCB.152_15;
  struct TCB_t * pxCurrentTCB.147_23;
  struct TCB_t * pxCurrentTCB.151_36;
  BaseType_t _43;

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

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

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

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

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.147_23 ={v} pxCurrentTCB;
  _3 ={v} pxCurrentTCB.147_23->ulNotifiedValue[uxIndexToWait_20(D)];
  _4 = ~ulBitsToClearOnEntry_24(D);
  _5 = _3 & _4;
  pxCurrentTCB.147_23->ulNotifiedValue[uxIndexToWait_20(D)] ={v} _5;
  # DEBUG BEGIN_STMT
  pxCurrentTCB.148_6 ={v} pxCurrentTCB;
  pxCurrentTCB.148_6->ucNotifyState[uxIndexToWait_20(D)] ={v} 1;
  # DEBUG BEGIN_STMT
  if (xTicksToWait_27(D) != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

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

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.149_8 ={v} pxCurrentTCB;
  _9 ={v} pxCurrentTCB.149_8->ulNotifiedValue[uxIndexToWait_20(D)];
  *pulNotificationValue_34(D) = _9;

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

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.151_36 ={v} pxCurrentTCB;
  _12 ={v} pxCurrentTCB.151_36->ulNotifiedValue[uxIndexToWait_20(D)];
  _13 = ~ulBitsToClearOnExit_37(D);
  _14 = _12 & _13;
  pxCurrentTCB.151_36->ulNotifiedValue[uxIndexToWait_20(D)] ={v} _14;
  # DEBUG BEGIN_STMT
  xReturn_39 = 1;
  # DEBUG xReturn => xReturn_39

  <bb 13> :
  # xReturn_16 = PHI <xReturn_40(11), xReturn_39(12)>
  # DEBUG xReturn => xReturn_16
  # DEBUG BEGIN_STMT
  pxCurrentTCB.152_15 ={v} pxCurrentTCB;
  pxCurrentTCB.152_15->ucNotifyState[uxIndexToWait_20(D)] ={v} 0;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _43 = xReturn_16;
  return _43;

}


ulTaskGenericNotifyTake (UBaseType_t uxIndexToWait, BaseType_t xClearCountOnExit, TickType_t xTicksToWait)
{
  uint32_t ulReturn;
  struct TCB_t * pxCurrentTCB.140_1;
  long unsigned int _2;
  struct TCB_t * pxCurrentTCB.141_3;
  volatile uint32_t * _4;
  struct TCB_t * pxCurrentTCB.142_5;
  struct TCB_t * pxCurrentTCB.143_6;
  struct TCB_t * pxCurrentTCB.144_7;
  long unsigned int _8;
  struct TCB_t * pxCurrentTCB.145_9;
  uint32_t _29;

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

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

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

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

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.141_3 ={v} pxCurrentTCB;
  pxCurrentTCB.141_3->ucNotifyState[uxIndexToWait_12(D)] ={v} 1;
  # DEBUG BEGIN_STMT
  if (xTicksToWait_16(D) != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

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

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

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

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.143_6 ={v} pxCurrentTCB;
  pxCurrentTCB.143_6->ulNotifiedValue[uxIndexToWait_12(D)] ={v} 0;
  goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.144_7 ={v} pxCurrentTCB;
  _8 = ulReturn_23 + 4294967295;
  pxCurrentTCB.144_7->ulNotifiedValue[uxIndexToWait_12(D)] ={v} _8;

  <bb 12> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.145_9 ={v} pxCurrentTCB;
  pxCurrentTCB.145_9->ucNotifyState[uxIndexToWait_12(D)] ={v} 0;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _29 = ulReturn_23;
  return _29;

}


pvTaskIncrementMutexHeldCount ()
{
  struct TCB_t * pxCurrentTCB.138_1;
  struct TCB_t * pxCurrentTCB.139_2;
  long unsigned int _3;
  long unsigned int _4;
  struct tskTaskControlBlock * _8;

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

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

  <bb 4> :
  # DEBUG BEGIN_STMT
  _8 ={v} pxCurrentTCB;
  return _8;

}


uxTaskResetEventItemValue ()
{
  TickType_t uxReturn;
  struct TCB_t * pxCurrentTCB.135_1;
  struct TCB_t * pxCurrentTCB.136_2;
  long unsigned int _3;
  struct TCB_t * pxCurrentTCB.137_4;
  long unsigned int _5;
  TickType_t _9;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.135_1 ={v} pxCurrentTCB;
  uxReturn_7 = pxCurrentTCB.135_1->xEventListItem.xItemValue;
  # DEBUG uxReturn => uxReturn_7
  # DEBUG BEGIN_STMT
  pxCurrentTCB.136_2 ={v} pxCurrentTCB;
  _3 = pxCurrentTCB.136_2->uxPriority;
  pxCurrentTCB.137_4 ={v} pxCurrentTCB;
  _5 = 5 - _3;
  pxCurrentTCB.137_4->xEventListItem.xItemValue = _5;
  # DEBUG BEGIN_STMT
  _9 = uxReturn_7;
  return _9;

}


vTaskList (char * pcWriteBuffer)
{
  char cStatus;
  UBaseType_t x;
  UBaseType_t uxArraySize;
  struct TaskStatus_t * pxTaskStatusArray;
  long unsigned int uxCurrentNumberOfTasks.134_1;
  long unsigned int _2;
  long unsigned int _3;
  struct TaskStatus_t * _4;
  <unnamed type> _5;
  long unsigned int _6;
  struct TaskStatus_t * _7;
  const char * _8;
  int _9;
  long unsigned int _10;
  struct TaskStatus_t * _11;
  long unsigned int _12;
  long unsigned int _13;
  struct TaskStatus_t * _14;
  short unsigned int _15;
  unsigned int _16;
  long unsigned int _17;
  struct TaskStatus_t * _18;
  long unsigned int _19;
  unsigned int _20;

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

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

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

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

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

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

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

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

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

  <bb 11> :
  # cStatus_23 = PHI <cStatus_40(5), cStatus_39(6), cStatus_38(7), cStatus_37(8), cStatus_36(9), cStatus_41(10)>
  # DEBUG cStatus => cStatus_23
  # DEBUG BEGIN_STMT
  _6 = x_22 * 36;
  _7 = pxTaskStatusArray_31 + _6;
  _8 = _7->pcTaskName;
  pcWriteBuffer_43 = prvWriteNameToBuffer (pcWriteBuffer_21, _8);
  # DEBUG pcWriteBuffer => pcWriteBuffer_43
  # DEBUG BEGIN_STMT
  _9 = (int) cStatus_23;
  _10 = x_22 * 36;
  _11 = pxTaskStatusArray_31 + _10;
  _12 = _11->uxCurrentPriority;
  _13 = x_22 * 36;
  _14 = pxTaskStatusArray_31 + _13;
  _15 = _14->usStackHighWaterMark;
  _16 = (unsigned int) _15;
  _17 = x_22 * 36;
  _18 = pxTaskStatusArray_31 + _17;
  _19 = _18->xTaskNumber;
  sprintf (pcWriteBuffer_43, "\t%c\t%u\t%u\t%u\r\n", _9, _12, _16, _19);
  # DEBUG BEGIN_STMT
  _20 = strlen (pcWriteBuffer_43);
  pcWriteBuffer_45 = pcWriteBuffer_43 + _20;
  # DEBUG pcWriteBuffer => pcWriteBuffer_45
  # DEBUG BEGIN_STMT
  x_46 = x_22 + 1;
  # DEBUG x => x_46

  <bb 12> :
  # pcWriteBuffer_21 = PHI <pcWriteBuffer_27(D)(3), pcWriteBuffer_45(11)>
  # x_22 = PHI <x_34(3), x_46(11)>
  # DEBUG x => x_22
  # DEBUG pcWriteBuffer => pcWriteBuffer_21
  # DEBUG BEGIN_STMT
  if (x_22 < uxArraySize_33)
    goto <bb 4>; [INV]
  else
    goto <bb 13>; [INV]

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

  <bb 14> :
  # DEBUG BEGIN_STMT
  return;

}


prvWriteNameToBuffer (char * pcBuffer, const char * pcTaskName)
{
  size_t x;
  char * _1;
  char * _2;
  char * _11;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  strcpy (pcBuffer_6(D), pcTaskName_7(D));
  # DEBUG BEGIN_STMT
  x_9 = strlen (pcBuffer_6(D));
  # DEBUG x => x_9
  goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  _1 = pcBuffer_6(D) + x_3;
  *_1 = 32;
  # DEBUG BEGIN_STMT
  x_13 = x_3 + 1;
  # DEBUG x => x_13

  <bb 4> :
  # x_3 = PHI <x_9(2), x_13(3)>
  # DEBUG x => x_3
  # DEBUG BEGIN_STMT
  if (x_3 <= 8)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  _2 = pcBuffer_6(D) + x_3;
  *_2 = 0;
  # DEBUG BEGIN_STMT
  _11 = pcBuffer_6(D) + x_3;
  return _11;

}


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;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  long unsigned int _4;
  struct TCB_t * pxCurrentTCB.132_5;
  long unsigned int _6;
  signed int _7;
  long unsigned int _8;
  struct xLIST * _9;
  struct List_t * _10;
  struct ListItem_t * _11;
  long unsigned int _12;
  long unsigned int _13;
  long unsigned int uxTopReadyPriority.133_14;
  long unsigned int _15;
  long unsigned int _16;
  struct xLIST_ITEM * _17;
  struct xLIST_ITEM * _18;
  struct ListItem_t * _19;
  struct ListItem_t * _20;
  long unsigned int _21;
  struct List_t * _22;
  long unsigned int _23;
  long unsigned int _24;
  long unsigned int _25;

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

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

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

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

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  uxPriorityToUse_36 = uxHighestPriorityWaitingTask_34(D);
  # DEBUG uxPriorityToUse => uxPriorityToUse_36
  goto <bb 9>; [INV]

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

  <bb 9> :
  # uxPriorityToUse_26 = PHI <uxPriorityToUse_36(7), uxPriorityToUse_35(8)>
  # DEBUG uxPriorityToUse => uxPriorityToUse_26
  # DEBUG BEGIN_STMT
  _3 = pxTCB_31->uxPriority;
  if (uxPriorityToUse_26 != _3)
    goto <bb 10>; [INV]
  else
    goto <bb 20>; [INV]

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

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

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

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

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

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

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

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

  <bb 18> :
  # DEBUG BEGIN_STMT
  _15 = pxTCB_31->uxPriority;
  uxTopReadyPriority ={v} _15;

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

  <bb 20> :
  # DEBUG BEGIN_STMT
  return;

}


xTaskPriorityDisinherit (struct tskTaskControlBlock * const pxMutexHolder)
{
  struct ListItem_t * const pxIndex;
  BaseType_t xReturn;
  struct TCB_t * const pxTCB;
  struct TCB_t * pxCurrentTCB.130_1;
  long unsigned int _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  long unsigned int _6;
  long unsigned int _7;
  struct ListItem_t * _8;
  long unsigned int _9;
  long unsigned int _10;
  long unsigned int _11;
  long unsigned int _12;
  long unsigned int _13;
  long unsigned int uxTopReadyPriority.131_14;
  long unsigned int _15;
  long unsigned int _16;
  struct xLIST_ITEM * _17;
  struct xLIST_ITEM * _18;
  struct ListItem_t * _19;
  struct ListItem_t * _20;
  long unsigned int _21;
  struct List_t * _22;
  long unsigned int _23;
  long unsigned int _24;
  long unsigned int _25;
  BaseType_t _48;

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

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

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

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

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

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

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

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

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

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  _15 = pxTCB_30->uxPriority;
  uxTopReadyPriority ={v} _15;

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

  <bb 14> :
  # xReturn_26 = PHI <xReturn_31(2), xReturn_45(13), xReturn_31(9), xReturn_31(10)>
  # DEBUG xReturn => xReturn_26
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _48 = xReturn_26;
  return _48;

}


xTaskPriorityInherit (struct tskTaskControlBlock * const pxMutexHolder)
{
  struct ListItem_t * const pxIndex;
  BaseType_t xReturn;
  struct TCB_t * const pxMutexHolderTCB;
  long unsigned int _1;
  struct TCB_t * pxCurrentTCB.124_2;
  long unsigned int _3;
  long unsigned int _4;
  signed int _5;
  struct TCB_t * pxCurrentTCB.125_6;
  long unsigned int _7;
  long unsigned int _8;
  struct xLIST * _9;
  long unsigned int _10;
  struct List_t * _11;
  struct ListItem_t * _12;
  long unsigned int _13;
  struct TCB_t * pxCurrentTCB.126_14;
  long unsigned int _15;
  long unsigned int _16;
  long unsigned int uxTopReadyPriority.127_17;
  long unsigned int _18;
  long unsigned int _19;
  struct xLIST_ITEM * _20;
  struct xLIST_ITEM * _21;
  struct ListItem_t * _22;
  struct ListItem_t * _23;
  long unsigned int _24;
  struct List_t * _25;
  long unsigned int _26;
  long unsigned int _27;
  long unsigned int _28;
  struct TCB_t * pxCurrentTCB.128_29;
  long unsigned int _30;
  long unsigned int _31;
  struct TCB_t * pxCurrentTCB.129_32;
  long unsigned int _33;
  BaseType_t _57;

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

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

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

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

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

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  _18 = pxMutexHolderTCB_40->uxPriority;
  uxTopReadyPriority ={v} _18;

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

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB.128_29 ={v} pxCurrentTCB;
  _30 = pxCurrentTCB.128_29->uxPriority;
  pxMutexHolderTCB_40->uxPriority = _30;

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

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

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

  <bb 14> :
  # xReturn_34 = PHI <xReturn_41(2), xReturn_41(12), xReturn_56(11), xReturn_43(13)>
  # DEBUG xReturn => xReturn_34
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _57 = xReturn_34;
  return _57;

}


xTaskGetSchedulerState ()
{
  BaseType_t xReturn;
  long int xSchedulerRunning.122_1;
  long unsigned int uxSchedulerSuspended.123_2;
  BaseType_t _8;

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

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

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

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

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

  <bb 7> :
  # xReturn_3 = PHI <xReturn_7(3), xReturn_6(5), xReturn_5(6)>
  # DEBUG xReturn => xReturn_3
  # DEBUG BEGIN_STMT
  _8 = xReturn_3;
  return _8;

}


xTaskGetCurrentTaskHandle ()
{
  struct tskTaskControlBlock * xReturn;
  struct tskTaskControlBlock * _3;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xReturn_2 ={v} pxCurrentTCB;
  # DEBUG xReturn => xReturn_2
  # DEBUG BEGIN_STMT
  _3 = xReturn_2;
  return _3;

}


prvResetNextTaskUnblockTime ()
{
  struct List_t * pxDelayedTaskList.20_1;
  long unsigned int _2;
  struct List_t * pxDelayedTaskList.21_3;
  struct xLIST_ITEM * _4;
  long unsigned int _5;

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

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

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

  <bb 5> :
  return;

}


prvDeleteTCB (struct TCB_t * pxTCB)
{
  StackType_t * _1;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 = pxTCB_3(D)->pxStack;
  vPortFree (_1);
  # DEBUG BEGIN_STMT
  vPortFree (pxTCB_3(D));
  return;

}


uxTaskGetStackHighWaterMark (struct tskTaskControlBlock * xTask)
{
  UBaseType_t uxReturn;
  uint8_t * pucEndOfStack;
  struct TCB_t * pxTCB;
  short unsigned int _1;
  struct TCB_t * iftmp.121_2;
  struct TCB_t * iftmp.121_4;
  struct TCB_t * iftmp.121_6;
  UBaseType_t _11;

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

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

  <bb 4> :
  iftmp.121_4 = xTask_3(D);

  <bb 5> :
  # iftmp.121_2 = PHI <iftmp.121_6(3), iftmp.121_4(4)>
  pxTCB_7 = iftmp.121_2;
  # DEBUG pxTCB => pxTCB_7
  # DEBUG BEGIN_STMT
  pucEndOfStack_8 = pxTCB_7->pxStack;
  # DEBUG pucEndOfStack => pucEndOfStack_8
  # DEBUG BEGIN_STMT
  _1 = prvTaskCheckFreeStackSpace (pucEndOfStack_8);
  uxReturn_10 = (UBaseType_t) _1;
  # DEBUG uxReturn => uxReturn_10
  # DEBUG BEGIN_STMT
  _11 = uxReturn_10;
  return _11;

}


prvTaskCheckFreeStackSpace (const uint8_t * pucStackByte)
{
  uint32_t ulCount;
  unsigned char _1;
  uint16_t _8;

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

  <bb 3> :
  # DEBUG BEGIN_STMT
  pucStackByte_9 = pucStackByte_2 + 1;
  # DEBUG pucStackByte => pucStackByte_9
  # DEBUG BEGIN_STMT
  ulCount_10 = ulCount_3 + 1;
  # DEBUG ulCount => ulCount_10

  <bb 4> :
  # pucStackByte_2 = PHI <pucStackByte_5(D)(2), pucStackByte_9(3)>
  # ulCount_3 = PHI <ulCount_4(2), ulCount_10(3)>
  # DEBUG ulCount => ulCount_3
  # DEBUG pucStackByte => pucStackByte_2
  # DEBUG BEGIN_STMT
  _1 = *pucStackByte_2;
  if (_1 == 165)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  ulCount_7 = ulCount_3 / 4;
  # DEBUG ulCount => ulCount_7
  # DEBUG BEGIN_STMT
  _8 = (uint16_t) ulCount_7;
  return _8;

}


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;
  long unsigned int _1;
  struct ListItem_t * _2;
  struct xLIST_ITEM * _3;
  struct ListItem_t * _4;
  struct MiniListItem_t * _5;
  struct ListItem_t * _6;
  struct xLIST_ITEM * _7;
  struct ListItem_t * _8;
  struct ListItem_t * _9;
  struct xLIST_ITEM * _10;
  struct ListItem_t * _11;
  struct MiniListItem_t * _12;
  struct ListItem_t * _13;
  struct xLIST_ITEM * _14;
  struct ListItem_t * _15;
  long unsigned int _16;
  struct TaskStatus_t * _17;
  UBaseType_t _39;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxTask_24 = 0;
  # DEBUG uxTask => uxTask_24
  # DEBUG BEGIN_STMT
  _1 ={v} pxList_26(D)->uxNumberOfItems;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 9>; [INV]

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

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

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

  <bb 6> :
  # uxTask_18 = PHI <uxTask_24(5), uxTask_38(8)>
  # DEBUG uxTask => uxTask_18
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxConstList_31 = pxList_26(D);
  # DEBUG pxConstList => pxConstList_31
  # DEBUG BEGIN_STMT
  _9 = pxConstList_31->pxIndex;
  _10 = _9->pxNext;
  pxConstList_31->pxIndex = _10;
  # DEBUG BEGIN_STMT
  _11 = pxConstList_31->pxIndex;
  _12 = &pxConstList_31->xListEnd;
  if (_11 == _12)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  _15 = pxConstList_31->pxIndex;
  pxNextTCB_34 = _15->pvOwner;
  # DEBUG pxNextTCB => pxNextTCB_34
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _16 = uxTask_18 * 36;
  _17 = pxTaskStatusArray_35(D) + _16;
  vTaskGetInfo (pxNextTCB_34, _17, 1, eState_36(D));
  # DEBUG BEGIN_STMT
  uxTask_38 = uxTask_18 + 1;
  # DEBUG uxTask => uxTask_38
  # DEBUG BEGIN_STMT
  if (pxNextTCB_34 != pxFirstTCB_30)
    goto <bb 6>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 9> :
  # uxTask_19 = PHI <uxTask_24(2), uxTask_38(8)>
  # DEBUG uxTask => uxTask_19
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _39 = uxTask_19;
  return _39;

}


vTaskGetInfo (struct tskTaskControlBlock * xTask, struct TaskStatus_t * pxTaskStatus, BaseType_t xGetFreeStackSpace, eTaskState eState)
{
  struct TCB_t * pxTCB;
  char * _1;
  long unsigned int _2;
  StackType_t * _3;
  long unsigned int _4;
  long unsigned int _5;
  struct TCB_t * pxCurrentTCB.120_6;
  struct xLIST * _7;
  <unnamed type> _8;
  StackType_t * _9;
  short unsigned int _10;
  struct TCB_t * iftmp.119_11;
  struct TCB_t * iftmp.119_16;
  struct TCB_t * iftmp.119_18;

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

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

  <bb 4> :
  iftmp.119_16 = xTask_15(D);

  <bb 5> :
  # iftmp.119_11 = PHI <iftmp.119_18(3), iftmp.119_16(4)>
  pxTCB_19 = iftmp.119_11;
  # DEBUG pxTCB => pxTCB_19
  # DEBUG BEGIN_STMT
  pxTaskStatus_20(D)->xHandle = pxTCB_19;
  # DEBUG BEGIN_STMT
  _1 = &pxTCB_19->pcTaskName[0];
  pxTaskStatus_20(D)->pcTaskName = _1;
  # DEBUG BEGIN_STMT
  _2 = pxTCB_19->uxPriority;
  pxTaskStatus_20(D)->uxCurrentPriority = _2;
  # DEBUG BEGIN_STMT
  _3 = pxTCB_19->pxStack;
  pxTaskStatus_20(D)->pxStackBase = _3;
  # DEBUG BEGIN_STMT
  _4 = pxTCB_19->uxTCBNumber;
  pxTaskStatus_20(D)->xTaskNumber = _4;
  # DEBUG BEGIN_STMT
  _5 = pxTCB_19->uxBasePriority;
  pxTaskStatus_20(D)->uxBasePriority = _5;
  # DEBUG BEGIN_STMT
  pxTaskStatus_20(D)->ulRunTimeCounter = 0;
  # DEBUG BEGIN_STMT
  if (eState_28(D) != 5)
    goto <bb 6>; [INV]
  else
    goto <bb 12>; [INV]

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  pxTaskStatus_20(D)->eCurrentState = 0;
  goto <bb 13>; [INV]

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

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

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxTaskStatus_20(D)->eCurrentState = 2;

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  _8 = eTaskGetState (pxTCB_19);
  pxTaskStatus_20(D)->eCurrentState = _8;

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

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

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxTaskStatus_20(D)->usStackHighWaterMark = 0;

  <bb 16> :
  return;

}


prvCheckTasksWaitingTermination ()
{
  struct TCB_t * pxTCB;
  struct xLIST_ITEM * _1;
  struct ListItem_t * _2;
  long unsigned int uxCurrentNumberOfTasks.58_3;
  long unsigned int _4;
  long unsigned int uxDeletedTasksWaitingCleanUp.59_5;
  long unsigned int _6;
  long unsigned int uxDeletedTasksWaitingCleanUp.60_7;

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

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

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

  <bb 5> :
  return;

}


prvInitialiseTaskLists ()
{
  UBaseType_t uxPriority;
  struct List_t * _1;

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

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

  <bb 4> :
  # uxPriority_2 = PHI <uxPriority_4(2), uxPriority_14(3)>
  # DEBUG uxPriority => uxPriority_2
  # DEBUG BEGIN_STMT
  if (uxPriority_2 <= 4)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

}


prvIdleTask (void * pvParameters)
{
  long unsigned int _1;
  volatile uint32_t * _2;

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

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

}


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

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

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxTCB_4 = xTask_2(D);
  # DEBUG pxTCB => pxTCB_4
  # DEBUG BEGIN_STMT
  pxTCB_4->uxTaskNumber = uxHandle_5(D);

  <bb 4> :
  return;

}


uxTaskGetTaskNumber (struct tskTaskControlBlock * xTask)
{
  const struct TCB_t * pxTCB;
  UBaseType_t uxReturn;
  UBaseType_t _7;

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

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxTCB_4 = xTask_2(D);
  # DEBUG pxTCB => pxTCB_4
  # DEBUG BEGIN_STMT
  uxReturn_6 = pxTCB_4->uxTaskNumber;
  # DEBUG uxReturn => uxReturn_6
  goto <bb 5>; [INV]

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

  <bb 5> :
  # uxReturn_1 = PHI <uxReturn_6(3), uxReturn_3(4)>
  # DEBUG uxReturn => uxReturn_1
  # DEBUG BEGIN_STMT
  _7 = uxReturn_1;
  return _7;

}


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

}


xTaskCheckForTimeOut (struct TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait)
{
  const TickType_t xElapsedTime;
  const TickType_t xConstTickCount;
  BaseType_t xReturn;
  long unsigned int _1;
  struct TCB_t * pxCurrentTCB.116_2;
  unsigned char _3;
  struct TCB_t * pxCurrentTCB.117_4;
  long unsigned int _5;
  long int _6;
  long int xNumOfOverflows.118_7;
  long unsigned int _8;
  long unsigned int _9;
  long unsigned int _10;
  long unsigned int _11;
  BaseType_t _31;

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

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

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

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

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

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

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

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

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

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

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

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

  <bb 14> :
  # DEBUG BEGIN_STMT
  xReturn_20 = 1;
  # DEBUG xReturn => xReturn_20
  # DEBUG BEGIN_STMT
  *pxTicksToWait_15(D) = 0;
  goto <bb 18>; [INV]

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

  <bb 16> :
  # DEBUG BEGIN_STMT
  _10 = *pxTicksToWait_15(D);
  _11 = _10 - xElapsedTime_19;
  *pxTicksToWait_15(D) = _11;
  # DEBUG BEGIN_STMT
  vTaskInternalSetTimeOutState (pxTimeOut_14(D));
  # DEBUG BEGIN_STMT
  xReturn_26 = 0;
  # DEBUG xReturn => xReturn_26
  goto <bb 18>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  *pxTicksToWait_15(D) = 0;
  # DEBUG BEGIN_STMT
  xReturn_23 = 1;
  # DEBUG xReturn => xReturn_23

  <bb 18> :
  # xReturn_12 = PHI <xReturn_29(9), xReturn_27(11), xReturn_20(14), xReturn_26(16), xReturn_23(17)>
  # DEBUG xReturn => xReturn_12
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _31 = xReturn_12;
  return _31;

}


vTaskInternalSetTimeOutState (struct TimeOut_t * const pxTimeOut)
{
  long int xNumOfOverflows.114_1;
  long unsigned int xTickCount.115_2;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xNumOfOverflows.114_1 ={v} xNumOfOverflows;
  pxTimeOut_4(D)->xOverflowCount = xNumOfOverflows.114_1;
  # DEBUG BEGIN_STMT
  xTickCount.115_2 ={v} xTickCount;
  pxTimeOut_4(D)->xTimeOnEntering = xTickCount.115_2;
  return;

}


vTaskSetTimeOutState (struct TimeOut_t * const pxTimeOut)
{
  long int xNumOfOverflows.112_1;
  long unsigned int xTickCount.113_2;

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

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

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

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

}


vTaskRemoveFromUnorderedEventList (struct ListItem_t * pxEventListItem, const TickType_t xItemValue)
{
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  struct List_t * const pxList;
  struct TCB_t * pxUnblockedTCB;
  long unsigned int uxSchedulerSuspended.109_1;
  long unsigned int _2;
  struct xLIST_ITEM * _3;
  struct xLIST_ITEM * _4;
  struct xLIST_ITEM * _5;
  struct xLIST_ITEM * _6;
  struct ListItem_t * _7;
  struct xLIST_ITEM * _8;
  long unsigned int _9;
  long unsigned int _10;
  struct xLIST_ITEM * _11;
  struct xLIST_ITEM * _12;
  struct xLIST_ITEM * _13;
  struct xLIST_ITEM * _14;
  struct ListItem_t * _15;
  struct ListItem_t * _16;
  struct xLIST_ITEM * _17;
  long unsigned int _18;
  long unsigned int _19;
  long unsigned int _20;
  long unsigned int uxTopReadyPriority.110_21;
  long unsigned int _22;
  long unsigned int _23;
  struct xLIST_ITEM * _24;
  struct xLIST_ITEM * _25;
  struct ListItem_t * _26;
  struct ListItem_t * _27;
  long unsigned int _28;
  struct List_t * _29;
  long unsigned int _30;
  long unsigned int _31;
  long unsigned int _32;
  long unsigned int _33;
  struct TCB_t * pxCurrentTCB.111_34;
  long unsigned int _35;

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

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

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

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

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

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

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  _8 = pxEventListItem_42(D)->pxPrevious;
  pxList_45->pxIndex = _8;

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

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

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

  <bb 13> :
  # DEBUG BEGIN_STMT
  _22 = pxUnblockedTCB_44->uxPriority;
  uxTopReadyPriority ={v} _22;

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

  <bb 15> :
  # DEBUG BEGIN_STMT
  xYieldPending ={v} 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;
  struct xLIST_ITEM * _1;
  struct xLIST_ITEM * _2;
  struct xLIST_ITEM * _3;
  struct xLIST_ITEM * _4;
  struct xLIST_ITEM * _5;
  struct ListItem_t * _6;
  struct ListItem_t * _7;
  struct xLIST_ITEM * _8;
  long unsigned int _9;
  long unsigned int _10;
  long unsigned int uxSchedulerSuspended.106_11;
  struct xLIST_ITEM * _12;
  struct xLIST_ITEM * _13;
  struct xLIST_ITEM * _14;
  struct xLIST_ITEM * _15;
  struct ListItem_t * _16;
  struct ListItem_t * _17;
  struct xLIST_ITEM * _18;
  long unsigned int _19;
  long unsigned int _20;
  long unsigned int _21;
  long unsigned int uxTopReadyPriority.107_22;
  long unsigned int _23;
  long unsigned int _24;
  struct xLIST_ITEM * _25;
  struct xLIST_ITEM * _26;
  struct ListItem_t * _27;
  struct ListItem_t * _28;
  long unsigned int _29;
  struct List_t * _30;
  long unsigned int _31;
  long unsigned int _32;
  long unsigned int _33;
  struct xLIST_ITEM * _34;
  struct xLIST_ITEM * _35;
  struct ListItem_t * _36;
  struct ListItem_t * _37;
  long unsigned int _38;
  long unsigned int _39;
  long unsigned int _40;
  struct TCB_t * pxCurrentTCB.108_41;
  long unsigned int _42;
  BaseType_t _82;

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

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

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

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

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

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

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

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

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

  <bb 11> :
  # DEBUG BEGIN_STMT
  _23 = pxUnblockedTCB_51->uxPriority;
  uxTopReadyPriority ={v} _23;

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

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

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

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

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

  <bb 17> :
  # xReturn_43 = PHI <xReturn_80(15), xReturn_79(16)>
  # DEBUG xReturn => xReturn_43
  # DEBUG BEGIN_STMT
  _82 = xReturn_43;
  return _82;

}


vTaskPlaceOnEventListRestricted (struct List_t * const pxEventList, TickType_t xTicksToWait, const BaseType_t xWaitIndefinitely)
{
  struct ListItem_t * const pxIndex;
  struct TCB_t * pxCurrentTCB.101_1;
  struct TCB_t * pxCurrentTCB.102_2;
  struct xLIST_ITEM * _3;
  struct TCB_t * pxCurrentTCB.103_4;
  struct xLIST_ITEM * _5;
  struct ListItem_t * _6;
  struct TCB_t * pxCurrentTCB.104_7;
  struct ListItem_t * _8;
  struct TCB_t * pxCurrentTCB.105_9;
  long unsigned int _10;
  long unsigned int _11;

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

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

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

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

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

  <bb 7> :
  # xTicksToWait_12 = PHI <xTicksToWait_23(D)(5), xTicksToWait_24(6)>
  # DEBUG xTicksToWait => xTicksToWait_12
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  prvAddCurrentTaskToDelayedList (xTicksToWait_12, xWaitIndefinitely_22(D));
  return;

}


vTaskPlaceOnUnorderedEventList (struct List_t * pxEventList, const TickType_t xItemValue, const TickType_t xTicksToWait)
{
  struct ListItem_t * const pxIndex;
  long unsigned int uxSchedulerSuspended.94_1;
  struct TCB_t * pxCurrentTCB.95_2;
  long unsigned int _3;
  struct TCB_t * pxCurrentTCB.96_4;
  struct TCB_t * pxCurrentTCB.97_5;
  struct xLIST_ITEM * _6;
  struct TCB_t * pxCurrentTCB.98_7;
  struct xLIST_ITEM * _8;
  struct ListItem_t * _9;
  struct TCB_t * pxCurrentTCB.99_10;
  struct ListItem_t * _11;
  struct TCB_t * pxCurrentTCB.100_12;
  long unsigned int _13;
  long unsigned int _14;

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

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

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

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

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

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

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

}


vTaskPlaceOnEventList (struct List_t * const pxEventList, const TickType_t xTicksToWait)
{
  struct TCB_t * pxCurrentTCB.93_1;
  struct ListItem_t * _2;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxCurrentTCB.93_1 ={v} pxCurrentTCB;
  _2 = &pxCurrentTCB.93_1->xEventListItem;
  vListInsert (pxEventList_3(D), _2);
  # DEBUG BEGIN_STMT
  prvAddCurrentTaskToDelayedList (xTicksToWait_6(D), 1);
  return;

}


__attribute__((used))
vTaskSwitchContext ()
{
  struct List_t * const pxConstList;
  UBaseType_t uxTopPriority;
  long unsigned int uxSchedulerSuspended.92_1;
  long unsigned int _2;
  struct ListItem_t * _3;
  struct xLIST_ITEM * _4;
  struct ListItem_t * _5;
  struct MiniListItem_t * _6;
  struct ListItem_t * _7;
  struct xLIST_ITEM * _8;
  struct ListItem_t * _9;
  void * _10;

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

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

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

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

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

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

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

  <bb 9> :
  # uxTopPriority_11 = PHI <uxTopPriority_16(4), uxTopPriority_22(8)>
  # DEBUG uxTopPriority => uxTopPriority_11
  # DEBUG BEGIN_STMT
  _2 ={v} pxReadyTasksLists[uxTopPriority_11].uxNumberOfItems;
  if (_2 == 0)
    goto <bb 5>; [INV]
  else
    goto <bb 10>; [INV]

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

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  _9 = pxConstList_17->pxIndex;
  _10 = _9->pvOwner;
  pxCurrentTCB ={v} _10;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxTopReadyPriority ={v} uxTopPriority_11;

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

}


xTaskIncrementTick ()
{
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  struct List_t * const pxList;
  struct List_t * pxTemp;
  const TickType_t xConstTickCount;
  BaseType_t xSwitchRequired;
  TickType_t xItemValue;
  struct TCB_t * pxTCB;
  long unsigned int uxSchedulerSuspended.79_1;
  long unsigned int xTickCount.80_2;
  struct List_t * pxDelayedTaskList.81_3;
  long unsigned int _4;
  struct List_t * pxOverflowDelayedTaskList.82_5;
  long int xNumOfOverflows.83_6;
  long int _7;
  long unsigned int xNextTaskUnblockTime.84_8;
  struct List_t * pxDelayedTaskList.85_9;
  long unsigned int _10;
  struct List_t * pxDelayedTaskList.86_11;
  struct xLIST_ITEM * _12;
  struct xLIST_ITEM * _13;
  struct xLIST_ITEM * _14;
  struct xLIST_ITEM * _15;
  struct xLIST_ITEM * _16;
  struct ListItem_t * _17;
  struct ListItem_t * _18;
  struct xLIST_ITEM * _19;
  long unsigned int _20;
  long unsigned int _21;
  struct xLIST * _22;
  struct xLIST_ITEM * _23;
  struct xLIST_ITEM * _24;
  struct xLIST_ITEM * _25;
  struct xLIST_ITEM * _26;
  struct ListItem_t * _27;
  struct ListItem_t * _28;
  struct xLIST_ITEM * _29;
  long unsigned int _30;
  long unsigned int _31;
  long unsigned int _32;
  long unsigned int uxTopReadyPriority.87_33;
  long unsigned int _34;
  long unsigned int _35;
  struct xLIST_ITEM * _36;
  struct xLIST_ITEM * _37;
  struct ListItem_t * _38;
  struct ListItem_t * _39;
  long unsigned int _40;
  struct List_t * _41;
  long unsigned int _42;
  long unsigned int _43;
  long unsigned int _44;
  long unsigned int _45;
  struct TCB_t * pxCurrentTCB.88_46;
  long unsigned int _47;
  struct TCB_t * pxCurrentTCB.89_48;
  long unsigned int _49;
  long unsigned int _50;
  long int xYieldPending.90_51;
  long unsigned int xPendedTicks.91_52;
  long unsigned int _53;
  BaseType_t _104;

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

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

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

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

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

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

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

  <bb 9> :
  # xSwitchRequired_54 = PHI <xSwitchRequired_66(8), xSwitchRequired_99(22), xSwitchRequired_54(21)>
  # DEBUG xSwitchRequired => xSwitchRequired_54
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxDelayedTaskList.85_9 ={v} pxDelayedTaskList;
  _10 ={v} pxDelayedTaskList.85_9->uxNumberOfItems;
  if (_10 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

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

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  xNextTaskUnblockTime ={v} xItemValue_78;
  # DEBUG BEGIN_STMT
  goto <bb 23>; [INV]

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

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

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

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

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

  <bb 18> :
  # DEBUG BEGIN_STMT
  pxTCB_77->xEventListItem.pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _30 ={v} pxList_85->uxNumberOfItems;
  _31 = _30 + 4294967295;
  pxList_85->uxNumberOfItems ={v} _31;
  # DEBUG BEGIN_STMT

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

  <bb 20> :
  # DEBUG BEGIN_STMT
  _34 = pxTCB_77->uxPriority;
  uxTopReadyPriority ={v} _34;

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

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

  <bb 23> :
  # xSwitchRequired_55 = PHI <xSwitchRequired_66(8), xSwitchRequired_54(10), xSwitchRequired_54(12)>
  # DEBUG xSwitchRequired => xSwitchRequired_55
  # DEBUG BEGIN_STMT
  pxCurrentTCB.89_48 ={v} pxCurrentTCB;
  _49 = pxCurrentTCB.89_48->uxPriority;
  _50 ={v} pxReadyTasksLists[_49].uxNumberOfItems;
  if (_50 > 1)
    goto <bb 24>; [INV]
  else
    goto <bb 25>; [INV]

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

  <bb 25> :
  # xSwitchRequired_56 = PHI <xSwitchRequired_55(23), xSwitchRequired_102(24)>
  # DEBUG xSwitchRequired => xSwitchRequired_56
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xYieldPending.90_51 ={v} xYieldPending;
  if (xYieldPending.90_51 != 0)
    goto <bb 26>; [INV]
  else
    goto <bb 28>; [INV]

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

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

  <bb 28> :
  # xSwitchRequired_57 = PHI <xSwitchRequired_103(26), xSwitchRequired_66(27), xSwitchRequired_56(25)>
  # DEBUG xSwitchRequired => xSwitchRequired_57
  # DEBUG BEGIN_STMT
  _104 = xSwitchRequired_57;
  return _104;

}


xTaskAbortDelay (struct tskTaskControlBlock * xTask)
{
  struct ListItem_t * const pxIndex;
  BaseType_t xReturn;
  struct TCB_t * pxTCB;
  <unnamed type> _1;
  struct ListItem_t * _2;
  struct xLIST * _3;
  struct ListItem_t * _4;
  long unsigned int _5;
  long unsigned int uxTopReadyPriority.77_6;
  long unsigned int _7;
  long unsigned int _8;
  struct xLIST_ITEM * _9;
  struct xLIST_ITEM * _10;
  struct ListItem_t * _11;
  struct ListItem_t * _12;
  long unsigned int _13;
  struct List_t * _14;
  long unsigned int _15;
  long unsigned int _16;
  long unsigned int _17;
  long unsigned int _18;
  struct TCB_t * pxCurrentTCB.78_19;
  long unsigned int _20;
  BaseType_t _47;

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

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

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

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

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

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

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  _7 = pxTCB_26->uxPriority;
  uxTopReadyPriority ={v} _7;

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

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

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

  <bb 13> :
  # xReturn_21 = PHI <xReturn_31(11), xReturn_30(12), xReturn_31(10)>
  # DEBUG xReturn => xReturn_21
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  _47 = xReturn_21;
  return _47;

}


xTaskCatchUpTicks (TickType_t xTicksToCatchUp)
{
  BaseType_t xYieldOccurred;
  long unsigned int uxSchedulerSuspended.75_1;
  long unsigned int xPendedTicks.76_2;
  long unsigned int _3;
  BaseType_t _10;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  xPendedTicks.76_2 ={v} xPendedTicks;
  _3 = xTicksToCatchUp_6(D) + xPendedTicks.76_2;
  xPendedTicks ={v} _3;
  # DEBUG BEGIN_STMT
  xYieldOccurred_9 = xTaskResumeAll ();
  # DEBUG xYieldOccurred => xYieldOccurred_9
  # DEBUG BEGIN_STMT
  _10 = xYieldOccurred_9;
  return _10;

}


uxTaskGetSystemState (struct TaskStatus_t * const pxTaskStatusArray, const UBaseType_t uxArraySize, uint32_t * const pulTotalRunTime)
{
  UBaseType_t uxQueue;
  UBaseType_t uxTask;
  long unsigned int uxCurrentNumberOfTasks.72_1;
  long unsigned int _2;
  struct TaskStatus_t * _3;
  struct List_t * _4;
  long unsigned int _5;
  struct TaskStatus_t * _6;
  struct List_t * pxDelayedTaskList.73_7;
  long unsigned int _8;
  struct TaskStatus_t * _9;
  struct List_t * pxOverflowDelayedTaskList.74_10;
  long unsigned int _11;
  struct TaskStatus_t * _12;
  long unsigned int _13;
  struct TaskStatus_t * _14;
  long unsigned int _28;
  long unsigned int _31;
  long unsigned int _34;
  long unsigned int _37;
  long unsigned int _40;
  UBaseType_t _45;

  <bb 2> :
  # DEBUG BEGIN_STMT
  uxTask_20 = 0;
  # DEBUG uxTask => uxTask_20
  uxQueue_21 = 5;
  # DEBUG uxQueue => uxQueue_21
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  uxCurrentNumberOfTasks.72_1 ={v} uxCurrentNumberOfTasks;
  if (uxArraySize_24(D) >= uxCurrentNumberOfTasks.72_1)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 3> :
  # uxTask_15 = PHI <uxTask_20(2), uxTask_29(3)>
  # uxQueue_17 = PHI <uxQueue_21(2), uxQueue_25(3)>
  # DEBUG uxQueue => uxQueue_17
  # DEBUG uxTask => uxTask_15
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxQueue_25 = uxQueue_17 + 4294967295;
  # DEBUG uxQueue => uxQueue_25
  # DEBUG BEGIN_STMT
  _2 = uxTask_15 * 36;
  _3 = pxTaskStatusArray_26(D) + _2;
  _4 = &pxReadyTasksLists[uxQueue_25];
  _28 = prvListTasksWithinSingleList (_3, _4, 1);
  uxTask_29 = _28 + uxTask_15;
  # DEBUG uxTask => uxTask_29
  # DEBUG BEGIN_STMT
  if (uxQueue_25 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  _5 = uxTask_29 * 36;
  _6 = pxTaskStatusArray_26(D) + _5;
  pxDelayedTaskList.73_7 ={v} pxDelayedTaskList;
  _31 = prvListTasksWithinSingleList (_6, pxDelayedTaskList.73_7, 2);
  uxTask_32 = _31 + uxTask_29;
  # DEBUG uxTask => uxTask_32
  # DEBUG BEGIN_STMT
  _8 = uxTask_32 * 36;
  _9 = pxTaskStatusArray_26(D) + _8;
  pxOverflowDelayedTaskList.74_10 ={v} pxOverflowDelayedTaskList;
  _34 = prvListTasksWithinSingleList (_9, pxOverflowDelayedTaskList.74_10, 2);
  uxTask_35 = _34 + uxTask_32;
  # DEBUG uxTask => uxTask_35
  # DEBUG BEGIN_STMT
  _11 = uxTask_35 * 36;
  _12 = pxTaskStatusArray_26(D) + _11;
  _37 = prvListTasksWithinSingleList (_12, &xTasksWaitingTermination, 4);
  uxTask_38 = _37 + uxTask_35;
  # DEBUG uxTask => uxTask_38
  # DEBUG BEGIN_STMT
  _13 = uxTask_38 * 36;
  _14 = pxTaskStatusArray_26(D) + _13;
  _40 = prvListTasksWithinSingleList (_14, &xSuspendedTaskList, 3);
  uxTask_41 = _40 + uxTask_38;
  # DEBUG uxTask => uxTask_41
  # DEBUG BEGIN_STMT
  if (pulTotalRunTime_42(D) != 0B)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  *pulTotalRunTime_42(D) = 0;

  <bb 6> :
  # uxTask_16 = PHI <uxTask_20(2), uxTask_41(5), uxTask_41(4)>
  # DEBUG uxTask => uxTask_16
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  _45 = uxTask_16;
  return _45;

}


xTaskGetHandle (const char * pcNameToQuery)
{
  struct TCB_t * pxTCB;
  UBaseType_t uxQueue;
  unsigned int _1;
  struct List_t * _2;
  struct List_t * pxDelayedTaskList.70_3;
  struct List_t * pxOverflowDelayedTaskList.71_4;
  struct tskTaskControlBlock * _31;

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

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

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

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

  <bb 6> :
  # uxQueue_5 = PHI <uxQueue_15(5), uxQueue_19(7)>
  # DEBUG uxQueue => uxQueue_5
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxQueue_19 = uxQueue_5 + 4294967295;
  # DEBUG uxQueue => uxQueue_19
  # DEBUG BEGIN_STMT
  _2 = &pxReadyTasksLists[uxQueue_19];
  pxTCB_21 = prvSearchForNameWithinSingleList (_2, pcNameToQuery_17(D));
  # DEBUG pxTCB => pxTCB_21
  # DEBUG BEGIN_STMT
  if (pxTCB_21 != 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 7>; [INV]

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

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxDelayedTaskList.70_3 ={v} pxDelayedTaskList;
  pxTCB_23 = prvSearchForNameWithinSingleList (pxDelayedTaskList.70_3, pcNameToQuery_17(D));
  # DEBUG pxTCB => pxTCB_23

  <bb 10> :
  # pxTCB_6 = PHI <pxTCB_21(8), pxTCB_23(9)>
  # DEBUG pxTCB => pxTCB_6
  # DEBUG BEGIN_STMT
  if (pxTCB_6 == 0B)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxOverflowDelayedTaskList.71_4 ={v} pxOverflowDelayedTaskList;
  pxTCB_25 = prvSearchForNameWithinSingleList (pxOverflowDelayedTaskList.71_4, pcNameToQuery_17(D));
  # DEBUG pxTCB => pxTCB_25

  <bb 12> :
  # pxTCB_7 = PHI <pxTCB_6(10), pxTCB_25(11)>
  # DEBUG pxTCB => pxTCB_7
  # DEBUG BEGIN_STMT
  if (pxTCB_7 == 0B)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 14> :
  # pxTCB_8 = PHI <pxTCB_7(12), pxTCB_27(13)>
  # DEBUG pxTCB => pxTCB_8
  # DEBUG BEGIN_STMT
  if (pxTCB_8 == 0B)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

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

  <bb 16> :
  # pxTCB_9 = PHI <pxTCB_8(14), pxTCB_29(15)>
  # DEBUG pxTCB => pxTCB_9
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  _31 = pxTCB_9;
  return _31;

}


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;
  long unsigned int _1;
  struct ListItem_t * _2;
  struct xLIST_ITEM * _3;
  struct ListItem_t * _4;
  struct MiniListItem_t * _5;
  struct ListItem_t * _6;
  struct xLIST_ITEM * _7;
  struct ListItem_t * _8;
  struct ListItem_t * _9;
  struct xLIST_ITEM * _10;
  struct ListItem_t * _11;
  struct MiniListItem_t * _12;
  struct ListItem_t * _13;
  struct xLIST_ITEM * _14;
  struct ListItem_t * _15;
  const char * _16;
  char _17;
  struct TCB_t * _49;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxReturn_30 = 0B;
  # DEBUG pxReturn => pxReturn_30
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 ={v} pxList_32(D)->uxNumberOfItems;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 18>; [INV]

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

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

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

  <bb 6> :
  # pxReturn_18 = PHI <pxReturn_30(5), pxReturn_21(17)>
  # DEBUG pxReturn => pxReturn_18
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxConstList_37 = pxList_32(D);
  # DEBUG pxConstList => pxConstList_37
  # DEBUG BEGIN_STMT
  _9 = pxConstList_37->pxIndex;
  _10 = _9->pxNext;
  pxConstList_37->pxIndex = _10;
  # DEBUG BEGIN_STMT
  _11 = pxConstList_37->pxIndex;
  _12 = &pxConstList_37->xListEnd;
  if (_11 == _12)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

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

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  cNextChar_43 = pxNextTCB_40->pcTaskName[x_23];
  # DEBUG cNextChar => cNextChar_43
  # DEBUG BEGIN_STMT
  _16 = pcNameToQuery_44(D) + x_23;
  _17 = *_16;
  if (cNextChar_43 != _17)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

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

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  pxReturn_45 = pxNextTCB_40;
  # DEBUG pxReturn => pxReturn_45
  # DEBUG BEGIN_STMT
  xBreakLoop_46 = 1;
  # DEBUG xBreakLoop => xBreakLoop_46

  <bb 13> :
  # pxReturn_19 = PHI <pxReturn_20(10), pxReturn_20(11), pxReturn_45(12)>
  # xBreakLoop_24 = PHI <xBreakLoop_47(10), xBreakLoop_25(11), xBreakLoop_46(12)>
  # DEBUG xBreakLoop => xBreakLoop_24
  # DEBUG pxReturn => pxReturn_19
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xBreakLoop_24 != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 15> :
  # pxReturn_20 = PHI <pxReturn_18(8), pxReturn_19(14)>
  # x_23 = PHI <x_42(8), x_48(14)>
  # xBreakLoop_25 = PHI <xBreakLoop_41(8), xBreakLoop_24(14)>
  # DEBUG xBreakLoop => xBreakLoop_25
  # DEBUG x => x_23
  # DEBUG pxReturn => pxReturn_20
  # DEBUG BEGIN_STMT
  if (x_23 <= 9)
    goto <bb 9>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 16> :
  # pxReturn_21 = PHI <pxReturn_19(13), pxReturn_20(15)>
  # DEBUG pxReturn => pxReturn_21
  # DEBUG BEGIN_STMT
  if (pxReturn_21 != 0B)
    goto <bb 18>; [INV]
  else
    goto <bb 17>; [INV]

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

  <bb 18> :
  # pxReturn_22 = PHI <pxReturn_30(2), pxReturn_21(17), pxReturn_21(16)>
  # DEBUG pxReturn => pxReturn_22
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _49 = pxReturn_22;
  return _49;

}


pcTaskGetName (struct tskTaskControlBlock * xTaskToQuery)
{
  struct TCB_t * pxTCB;
  struct TCB_t * iftmp.69_1;
  struct TCB_t * iftmp.69_3;
  struct TCB_t * iftmp.69_5;
  char * _7;

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

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

  <bb 4> :
  iftmp.69_3 = xTaskToQuery_2(D);

  <bb 5> :
  # iftmp.69_1 = PHI <iftmp.69_5(3), iftmp.69_3(4)>
  pxTCB_6 = iftmp.69_1;
  # DEBUG pxTCB => pxTCB_6
  # DEBUG BEGIN_STMT
  if (pxTCB_6 == 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

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

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _7 = &pxTCB_6->pcTaskName[0];
  return _7;

}


uxTaskGetNumberOfTasks ()
{
  UBaseType_t _2;

  <bb 2> :
  # DEBUG BEGIN_STMT
  _2 ={v} uxCurrentNumberOfTasks;
  return _2;

}


xTaskGetTickCountFromISR ()
{
  UBaseType_t uxSavedInterruptStatus;
  TickType_t xReturn;
  TickType_t _5;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus_3 = 0;
  # DEBUG uxSavedInterruptStatus => uxSavedInterruptStatus_3
  # DEBUG BEGIN_STMT
  xReturn_4 ={v} xTickCount;
  # DEBUG xReturn => xReturn_4
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _5 = xReturn_4;
  return _5;

}


xTaskGetTickCount ()
{
  TickType_t xTicks;
  TickType_t _3;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xTicks_2 ={v} xTickCount;
  # DEBUG xTicks => xTicks_2
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _3 = xTicks_2;
  return _3;

}


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;
  long unsigned int uxSchedulerSuspended.62_1;
  long unsigned int uxSchedulerSuspended.63_2;
  long unsigned int _3;
  long unsigned int uxSchedulerSuspended.64_4;
  long unsigned int uxCurrentNumberOfTasks.65_5;
  struct xLIST_ITEM * _6;
  struct xLIST_ITEM * _7;
  struct xLIST_ITEM * _8;
  struct xLIST_ITEM * _9;
  struct xLIST_ITEM * _10;
  struct ListItem_t * _11;
  struct ListItem_t * _12;
  struct xLIST_ITEM * _13;
  long unsigned int _14;
  long unsigned int _15;
  struct xLIST_ITEM * _16;
  struct xLIST_ITEM * _17;
  struct xLIST_ITEM * _18;
  struct xLIST_ITEM * _19;
  struct ListItem_t * _20;
  struct ListItem_t * _21;
  struct xLIST_ITEM * _22;
  long unsigned int _23;
  long unsigned int _24;
  long unsigned int _25;
  long unsigned int uxTopReadyPriority.66_26;
  long unsigned int _27;
  long unsigned int _28;
  struct xLIST_ITEM * _29;
  struct xLIST_ITEM * _30;
  struct ListItem_t * _31;
  struct ListItem_t * _32;
  long unsigned int _33;
  struct List_t * _34;
  long unsigned int _35;
  long unsigned int _36;
  long unsigned int _37;
  long unsigned int _38;
  struct TCB_t * pxCurrentTCB.67_39;
  long unsigned int _40;
  long unsigned int _41;
  long int _42;
  long int xYieldPending.68_43;
  volatile uint32_t * _44;
  BaseType_t _96;

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

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

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

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

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

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

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

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

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

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  _27 = pxTCB_72->uxPriority;
  uxTopReadyPriority ={v} _27;

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

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

  <bb 15> :
  # pxTCB_45 = PHI <pxTCB_57(6), pxTCB_72(13), pxTCB_72(14)>
  # DEBUG pxTCB => pxTCB_45
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _41 ={v} xPendingReadyList.uxNumberOfItems;
  if (_41 != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 16>; [INV]

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

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

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

  <bb 19> :
  # xPendedCounts_47 = PHI <xPendedCounts_63(18), xPendedCounts_66(21)>
  # DEBUG xPendedCounts => xPendedCounts_47
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _42 = xTaskIncrementTick ();
  if (_42 != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 21>; [INV]

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

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

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

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

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

  <bb 25> :
  # xAlreadyYielded_46 = PHI <xAlreadyYielded_58(5), xAlreadyYielded_58(23), xAlreadyYielded_58(6), xAlreadyYielded_68(24)>
  # DEBUG xAlreadyYielded => xAlreadyYielded_46
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _96 = xAlreadyYielded_46;
  return _96;

}


vTaskSuspendAll ()
{
  long unsigned int uxSchedulerSuspended.61_1;
  long unsigned int _2;

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

}


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

}


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

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

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

  <bb 4> :
  # xReturn_2 = PHI <xReturn_7(2), xReturn_9(3)>
  # DEBUG xReturn => xReturn_2
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xReturn_2 == 1)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

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

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

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

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vol.57_16 ={v} uxTopUsedPriority;
  return;

}


xTaskResumeFromISR (struct tskTaskControlBlock * xTaskToResume)
{
  struct ListItem_t * const pxIndex;
  UBaseType_t uxSavedInterruptStatus;
  struct TCB_t * const pxTCB;
  BaseType_t xYieldRequired;
  long int _1;
  long unsigned int uxSchedulerSuspended.54_2;
  long unsigned int _3;
  struct TCB_t * pxCurrentTCB.55_4;
  long unsigned int _5;
  struct ListItem_t * _6;
  long unsigned int _7;
  long unsigned int uxTopReadyPriority.56_8;
  long unsigned int _9;
  long unsigned int _10;
  struct xLIST_ITEM * _11;
  struct xLIST_ITEM * _12;
  struct ListItem_t * _13;
  struct ListItem_t * _14;
  long unsigned int _15;
  struct List_t * _16;
  long unsigned int _17;
  long unsigned int _18;
  long unsigned int _19;
  struct ListItem_t * _20;
  BaseType_t _47;

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

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

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

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

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

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  xYieldRequired_35 = 1;
  # DEBUG xYieldRequired => xYieldRequired_35
  # DEBUG BEGIN_STMT
  xYieldPending ={v} 1;

  <bb 9> :
  # xYieldRequired_21 = PHI <xYieldRequired_26(7), xYieldRequired_35(8)>
  # DEBUG xYieldRequired => xYieldRequired_21
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _6 = &pxTCB_28->xStateListItem;
  uxListRemove (_6);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _7 = pxTCB_28->uxPriority;
  uxTopReadyPriority.56_8 ={v} uxTopReadyPriority;
  if (_7 > uxTopReadyPriority.56_8)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  _9 = pxTCB_28->uxPriority;
  uxTopReadyPriority ={v} _9;

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

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

  <bb 13> :
  # xYieldRequired_22 = PHI <xYieldRequired_26(5), xYieldRequired_26(12), xYieldRequired_21(11)>
  # DEBUG xYieldRequired => xYieldRequired_22
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptStatus_32);
  # DEBUG BEGIN_STMT
  _47 = xYieldRequired_22;
  return _47;

}


vTaskResume (struct tskTaskControlBlock * xTaskToResume)
{
  struct ListItem_t * const pxIndex;
  struct TCB_t * const pxTCB;
  struct TCB_t * pxCurrentTCB.51_1;
  long int _2;
  struct ListItem_t * _3;
  long unsigned int _4;
  long unsigned int uxTopReadyPriority.52_5;
  long unsigned int _6;
  long unsigned int _7;
  struct xLIST_ITEM * _8;
  struct xLIST_ITEM * _9;
  struct ListItem_t * _10;
  struct ListItem_t * _11;
  long unsigned int _12;
  struct List_t * _13;
  long unsigned int _14;
  long unsigned int _15;
  long unsigned int _16;
  long unsigned int _17;
  struct TCB_t * pxCurrentTCB.53_18;
  long unsigned int _19;
  volatile uint32_t * _20;

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

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

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

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

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

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

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  _6 = pxTCB_25->uxPriority;
  uxTopReadyPriority ={v} _6;

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

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

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

  <bb 13> :
  # DEBUG BEGIN_STMT
  return;

}


prvTaskIsTaskSuspended (struct tskTaskControlBlock * const xTask)
{
  const struct TCB_t * const pxTCB;
  BaseType_t xReturn;
  struct xLIST * _1;
  struct xLIST * _2;
  struct xLIST * _3;
  BaseType_t _10;

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

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

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

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

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

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

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

  <bb 9> :
  # xReturn_4 = PHI <xReturn_5(5), xReturn_9(8), xReturn_5(6), xReturn_5(7)>
  # DEBUG xReturn => xReturn_4
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _10 = xReturn_4;
  return _10;

}


vTaskSuspend (struct tskTaskControlBlock * xTaskToSuspend)
{
  BaseType_t x;
  struct TCB_t * pxTCB;
  struct ListItem_t * _1;
  long unsigned int _2;
  struct xLIST * _3;
  struct ListItem_t * _4;
  struct ListItem_t * _5;
  unsigned char _6;
  long int xSchedulerRunning.46_7;
  struct TCB_t * pxCurrentTCB.47_8;
  long int xSchedulerRunning.48_9;
  long unsigned int uxSchedulerSuspended.49_10;
  volatile uint32_t * _11;
  long unsigned int _12;
  long unsigned int uxCurrentNumberOfTasks.50_13;
  struct TCB_t * iftmp.45_15;
  struct TCB_t * iftmp.45_24;
  struct TCB_t * iftmp.45_25;

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

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

  <bb 4> :
  iftmp.45_24 = xTaskToSuspend_23(D);

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

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

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  _6 ={v} pxTCB_26->ucNotifyState[x_14];
  if (_6 == 1)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxTCB_26->ucNotifyState[x_14] ={v} 0;

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

  <bb 11> :
  # x_14 = PHI <x_30(7), x_42(10)>
  # DEBUG x => x_14
  # DEBUG BEGIN_STMT
  if (x_14 <= 0)
    goto <bb 8>; [INV]
  else
    goto <bb 12>; [INV]

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

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

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

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

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

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

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

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

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

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

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

  <bb 23> :
  # DEBUG BEGIN_STMT
  return;

}


vTaskPrioritySet (struct tskTaskControlBlock * xTask, UBaseType_t uxNewPriority)
{
  struct ListItem_t * const pxIndex;
  BaseType_t xYieldRequired;
  UBaseType_t uxPriorityUsedOnEntry;
  UBaseType_t uxCurrentBasePriority;
  struct TCB_t * pxTCB;
  struct TCB_t * pxCurrentTCB.41_1;
  struct TCB_t * pxCurrentTCB.42_2;
  long unsigned int _3;
  struct TCB_t * pxCurrentTCB.43_4;
  long unsigned int _5;
  long unsigned int _6;
  long unsigned int _7;
  signed int _8;
  long unsigned int _9;
  struct xLIST * _10;
  struct List_t * _11;
  struct ListItem_t * _12;
  long unsigned int _13;
  long unsigned int _14;
  long unsigned int uxTopReadyPriority.44_15;
  long unsigned int _16;
  long unsigned int _17;
  struct xLIST_ITEM * _18;
  struct xLIST_ITEM * _19;
  struct ListItem_t * _20;
  struct ListItem_t * _21;
  long unsigned int _22;
  struct List_t * _23;
  long unsigned int _24;
  long unsigned int _25;
  long unsigned int _26;
  volatile uint32_t * _27;
  struct TCB_t * iftmp.40_30;
  struct TCB_t * iftmp.40_42;
  struct TCB_t * iftmp.40_43;

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

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

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

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

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

  <bb 7> :
  # uxNewPriority_28 = PHI <uxNewPriority_37(D)(5), uxNewPriority_38(6)>
  # DEBUG uxNewPriority => uxNewPriority_28
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  if (xTask_41(D) == 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

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

  <bb 9> :
  iftmp.40_42 = xTask_41(D);

  <bb 10> :
  # iftmp.40_30 = PHI <iftmp.40_43(8), iftmp.40_42(9)>
  pxTCB_44 = iftmp.40_30;
  # DEBUG pxTCB => pxTCB_44
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxCurrentBasePriority_45 = pxTCB_44->uxBasePriority;
  # DEBUG uxCurrentBasePriority => uxCurrentBasePriority_45
  # DEBUG BEGIN_STMT
  if (uxCurrentBasePriority_45 != uxNewPriority_28)
    goto <bb 11>; [INV]
  else
    goto <bb 27>; [INV]

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

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

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

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

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

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

  <bb 17> :
  # xYieldRequired_29 = PHI <xYieldRequired_47(14), xYieldRequired_36(15), xYieldRequired_46(16), xYieldRequired_36(12), xYieldRequired_36(13)>
  # DEBUG xYieldRequired => xYieldRequired_29
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxPriorityUsedOnEntry_48 = pxTCB_44->uxPriority;
  # DEBUG uxPriorityUsedOnEntry => uxPriorityUsedOnEntry_48
  # DEBUG BEGIN_STMT
  _5 = pxTCB_44->uxBasePriority;
  _6 = pxTCB_44->uxPriority;
  if (_5 == _6)
    goto <bb 18>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  pxTCB_44->uxPriority = uxNewPriority_28;

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

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

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

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

  <bb 23> :
  # DEBUG BEGIN_STMT
  _16 = pxTCB_44->uxPriority;
  uxTopReadyPriority ={v} _16;

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

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

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

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

}


uxTaskPriorityGetFromISR (struct tskTaskControlBlock * const xTask)
{
  UBaseType_t uxSavedInterruptState;
  UBaseType_t uxReturn;
  const struct TCB_t * pxTCB;
  const struct TCB_t * iftmp.39_1;
  const struct TCB_t * iftmp.39_7;
  const struct TCB_t * iftmp.39_8;
  UBaseType_t _12;

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

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

  <bb 4> :
  iftmp.39_7 = xTask_6(D);

  <bb 5> :
  # iftmp.39_1 = PHI <iftmp.39_8(3), iftmp.39_7(4)>
  pxTCB_9 = iftmp.39_1;
  # DEBUG pxTCB => pxTCB_9
  # DEBUG BEGIN_STMT
  uxReturn_10 = pxTCB_9->uxPriority;
  # DEBUG uxReturn => uxReturn_10
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptState_5);
  # DEBUG BEGIN_STMT
  _12 = uxReturn_10;
  return _12;

}


uxTaskPriorityGet (struct tskTaskControlBlock * const xTask)
{
  UBaseType_t uxReturn;
  const struct TCB_t * pxTCB;
  const struct TCB_t * iftmp.38_1;
  const struct TCB_t * iftmp.38_5;
  const struct TCB_t * iftmp.38_6;
  UBaseType_t _10;

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

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

  <bb 4> :
  iftmp.38_5 = xTask_4(D);

  <bb 5> :
  # iftmp.38_1 = PHI <iftmp.38_6(3), iftmp.38_5(4)>
  pxTCB_7 = iftmp.38_1;
  # DEBUG pxTCB => pxTCB_7
  # DEBUG BEGIN_STMT
  uxReturn_8 = pxTCB_7->uxPriority;
  # DEBUG uxReturn => uxReturn_8
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _10 = uxReturn_8;
  return _10;

}


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;
  struct TCB_t * pxCurrentTCB.37_1;
  struct xLIST * _2;
  unsigned char _3;
  eTaskState _24;

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

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

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

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

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  pxStateList_11 = pxTCB_8->xStateListItem.pvContainer;
  # DEBUG pxStateList => pxStateList_11
  # DEBUG BEGIN_STMT
  pxDelayedList_12 ={v} pxDelayedTaskList;
  # DEBUG pxDelayedList => pxDelayedList_12
  # DEBUG BEGIN_STMT
  pxOverflowedDelayedList_13 ={v} pxOverflowDelayedTaskList;
  # DEBUG pxOverflowedDelayedList => pxOverflowedDelayedList_13
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  if (pxStateList_11 == pxDelayedList_12)
    goto <bb 9>; [INV]
  else
    goto <bb 8>; [INV]

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

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

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

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

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

  <bb 13> :
  # DEBUG BEGIN_STMT
  _3 ={v} pxTCB_8->ucNotifyState[x_5];
  if (_3 == 1)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

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

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

  <bb 16> :
  # x_5 = PHI <x_19(12), x_20(15)>
  # DEBUG x => x_5
  # DEBUG BEGIN_STMT
  if (x_5 <= 0)
    goto <bb 13>; [INV]
  else
    goto <bb 22>; [INV]

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

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

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

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

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

  <bb 22> :
  # eReturn_4 = PHI <eReturn_23(6), eReturn_22(9), eReturn_17(17), eReturn_16(20), eReturn_15(21), eReturn_18(16), eReturn_21(14)>
  # DEBUG eReturn => eReturn_4
  # DEBUG BEGIN_STMT
  _24 = eReturn_4;
  return _24;

}


vTaskDelay (const TickType_t xTicksToDelay)
{
  BaseType_t xAlreadyYielded;
  long unsigned int uxSchedulerSuspended.36_1;
  volatile uint32_t * _2;

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

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

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

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

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

  <bb 7> :
  # xAlreadyYielded_3 = PHI <xAlreadyYielded_6(2), xAlreadyYielded_12(6)>
  # DEBUG xAlreadyYielded => xAlreadyYielded_3
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xAlreadyYielded_3 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  return;

}


xTaskDelayUntil (TickType_t * const pxPreviousWakeTime, const TickType_t xTimeIncrement)
{
  const TickType_t xConstTickCount;
  BaseType_t xShouldDelay;
  BaseType_t xAlreadyYielded;
  TickType_t xTimeToWake;
  long unsigned int uxSchedulerSuspended.22_1;
  long unsigned int _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  long unsigned int _6;
  volatile uint32_t * _7;
  BaseType_t _27;

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

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

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

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

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

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

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

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

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

  <bb 11> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  xConstTickCount_16 ={v} xTickCount;
  # DEBUG xConstTickCount => xConstTickCount_16
  # DEBUG BEGIN_STMT
  _2 = *pxPreviousWakeTime_12(D);
  xTimeToWake_17 = xTimeIncrement_13(D) + _2;
  # DEBUG xTimeToWake => xTimeToWake_17
  # DEBUG BEGIN_STMT
  _3 = *pxPreviousWakeTime_12(D);
  if (xConstTickCount_16 < _3)
    goto <bb 12>; [INV]
  else
    goto <bb 15>; [INV]

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

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

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

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

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

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

  <bb 18> :
  # xShouldDelay_8 = PHI <xShouldDelay_11(13), xShouldDelay_11(16), xShouldDelay_18(17), xShouldDelay_11(12), xShouldDelay_19(14)>
  # DEBUG xShouldDelay => xShouldDelay_8
  # DEBUG BEGIN_STMT
  *pxPreviousWakeTime_12(D) = xTimeToWake_17;
  # DEBUG BEGIN_STMT
  if (xShouldDelay_8 != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 20>; [INV]

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

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

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

  <bb 22> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _27 = xShouldDelay_8;
  return _27;

}


vTaskDelete (struct tskTaskControlBlock * xTaskToDelete)
{
  struct TCB_t * pxTCB;
  struct ListItem_t * _1;
  long unsigned int _2;
  struct xLIST * _3;
  struct ListItem_t * _4;
  long unsigned int uxTaskNumber.13_5;
  long unsigned int _6;
  struct TCB_t * pxCurrentTCB.14_7;
  struct ListItem_t * _8;
  long unsigned int uxDeletedTasksWaitingCleanUp.15_9;
  long unsigned int _10;
  long unsigned int uxCurrentNumberOfTasks.16_11;
  long unsigned int _12;
  long int xSchedulerRunning.17_13;
  struct TCB_t * pxCurrentTCB.18_14;
  long unsigned int uxSchedulerSuspended.19_15;
  volatile uint32_t * _16;
  struct TCB_t * iftmp.12_17;
  struct TCB_t * iftmp.12_24;
  struct TCB_t * iftmp.12_25;

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

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

  <bb 4> :
  iftmp.12_24 = xTaskToDelete_23(D);

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

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

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

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

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

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

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

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

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

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

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

  <bb 16> :
  # DEBUG BEGIN_STMT
  return;

}


prvAddNewTaskToReadyList (struct TCB_t * pxNewTCB)
{
  struct ListItem_t * const pxIndex;
  long unsigned int uxCurrentNumberOfTasks.2_1;
  long unsigned int _2;
  struct TCB_t * pxCurrentTCB.3_3;
  long unsigned int uxCurrentNumberOfTasks.4_4;
  long int xSchedulerRunning.5_5;
  struct TCB_t * pxCurrentTCB.6_6;
  long unsigned int _7;
  long unsigned int _8;
  long unsigned int uxTaskNumber.7_9;
  long unsigned int _10;
  long unsigned int uxTaskNumber.8_11;
  long unsigned int _12;
  long unsigned int uxTopReadyPriority.9_13;
  long unsigned int _14;
  long unsigned int _15;
  struct xLIST_ITEM * _16;
  struct xLIST_ITEM * _17;
  struct ListItem_t * _18;
  struct ListItem_t * _19;
  long unsigned int _20;
  struct List_t * _21;
  long unsigned int _22;
  long unsigned int _23;
  long unsigned int _24;
  long int xSchedulerRunning.10_25;
  struct TCB_t * pxCurrentTCB.11_26;
  long unsigned int _27;
  long unsigned int _28;
  volatile uint32_t * _29;

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

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

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

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

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  pxCurrentTCB ={v} pxNewTCB_36(D);

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  _14 = pxNewTCB_36(D)->uxPriority;
  uxTopReadyPriority ={v} _14;

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

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

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

  <bb 13> :
  # DEBUG BEGIN_STMT
  return;

}


prvInitialiseNewTask (void (*TaskFunction_t) (void *) pxTaskCode, const char * const pcName, const uint32_t ulStackDepth, void * const pvParameters, UBaseType_t uxPriority, struct tskTaskControlBlock * * const pxCreatedTask, struct TCB_t * pxNewTCB, const struct MemoryRegion_t * const xRegions)
{
  UBaseType_t x;
  StackType_t * pxTopOfStack;
  StackType_t * _1;
  unsigned int _2;
  StackType_t * _3;
  sizetype _4;
  sizetype _5;
  long unsigned int pxTopOfStack.0_6;
  long unsigned int _7;
  long unsigned int pxTopOfStack.1_8;
  long unsigned int _9;
  const char * _10;
  char _11;
  const char * _12;
  char _13;
  struct ListItem_t * _14;
  struct ListItem_t * _15;
  long unsigned int _16;
  volatile uint32_t * _17;
  volatile uint8_t * _18;
  StackType_t * _19;

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

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

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

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

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

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

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

  <bb 9> :
  # x_21 = PHI <x_34(6), x_36(8)>
  # DEBUG x => x_21
  # DEBUG BEGIN_STMT
  if (x_21 <= 9)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  pxNewTCB_27(D)->pcTaskName[9] = 0;
  goto <bb 12>; [INV]

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxNewTCB_27(D)->pcTaskName[0] = 0;

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

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

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

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

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

  <bb 17> :
  # uxPriority_20 = PHI <uxPriority_38(D)(15), uxPriority_39(16)>
  # DEBUG uxPriority => uxPriority_20
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxNewTCB_27(D)->uxPriority = uxPriority_20;
  # DEBUG BEGIN_STMT
  pxNewTCB_27(D)->uxBasePriority = uxPriority_20;
  # DEBUG BEGIN_STMT
  pxNewTCB_27(D)->uxMutexesHeld = 0;
  # DEBUG BEGIN_STMT
  _14 = &pxNewTCB_27(D)->xStateListItem;
  vListInitialiseItem (_14);
  # DEBUG BEGIN_STMT
  _15 = &pxNewTCB_27(D)->xEventListItem;
  vListInitialiseItem (_15);
  # DEBUG BEGIN_STMT
  pxNewTCB_27(D)->xStateListItem.pvOwner = pxNewTCB_27(D);
  # DEBUG BEGIN_STMT
  _16 = 5 - uxPriority_20;
  pxNewTCB_27(D)->xEventListItem.xItemValue = _16;
  # DEBUG BEGIN_STMT
  pxNewTCB_27(D)->xEventListItem.pvOwner = pxNewTCB_27(D);
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _17 = &pxNewTCB_27(D)->ulNotifiedValue[0];
  memset (_17, 0, 4);
  # DEBUG BEGIN_STMT
  _18 = &pxNewTCB_27(D)->ucNotifyState[0];
  memset (_18, 0, 1);
  # DEBUG BEGIN_STMT
  pxNewTCB_27(D)->ucDelayAborted = 0;
  # DEBUG BEGIN_STMT
  _19 = pxPortInitialiseStack (pxTopOfStack_31, pxTaskCode_51(D), pvParameters_52(D));
  pxNewTCB_27(D)->pxTopOfStack = _19;
  # DEBUG BEGIN_STMT
  if (pxCreatedTask_55(D) != 0B)
    goto <bb 18>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  *pxCreatedTask_55(D) = pxNewTCB_27(D);

  <bb 19> :
  # DEBUG BEGIN_STMT
  return;

}


xTaskCreate (void (*TaskFunction_t) (void *) pxTaskCode, const char * const pcName, const uint16_t usStackDepth, void * const pvParameters, UBaseType_t uxPriority, struct tskTaskControlBlock * * const pxCreatedTask)
{
  StackType_t * pxStack;
  BaseType_t xReturn;
  struct TCB_t * pxNewTCB;
  unsigned int _1;
  unsigned int _2;
  long unsigned int _3;
  BaseType_t _26;

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

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

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

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

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

  <bb 7> :
  # pxNewTCB_4 = PHI <pxNewTCB_14(5), pxNewTCB_12(6), pxNewTCB_14(4)>
  # DEBUG pxNewTCB => pxNewTCB_4
  # DEBUG BEGIN_STMT
  if (pxNewTCB_4 != 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  _3 = (long unsigned int) usStackDepth_8(D);
  prvInitialiseNewTask (pxTaskCode_18(D), pcName_19(D), _3, pvParameters_20(D), uxPriority_21(D), pxCreatedTask_22(D), pxNewTCB_4, 0B);
  # DEBUG BEGIN_STMT
  prvAddNewTaskToReadyList (pxNewTCB_4);
  # DEBUG BEGIN_STMT
  xReturn_25 = 1;
  # DEBUG xReturn => xReturn_25
  goto <bb 10>; [INV]

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

  <bb 10> :
  # xReturn_5 = PHI <xReturn_25(8), xReturn_17(9)>
  # DEBUG xReturn => xReturn_5
  # DEBUG BEGIN_STMT
  _26 = xReturn_5;
  return _26;

}


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

}


__attribute__((always_inline))
ulPortRaiseBASEPRI ()
{
  uint32_t ulNewBASEPRI;
  uint32_t ulOriginalBASEPRI;
  uint32_t _5;

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

}


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

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

}