prvAddCurrentTaskToDelayedList (TickType_t xTicksToWait, const BaseType_t xCanBlockIndefinitely)
{
  struct ListItem_t * const pxIndex;
  const TickType_t xConstTickCount;
  TickType_t xTimeToWake;
  struct TCB_t * pxCurrentTCB.152_1;
  struct TCB_t * pxCurrentTCB.153_2;
  struct ListItem_t * _3;
  long unsigned int _4;
  struct TCB_t * pxCurrentTCB.154_5;
  struct TCB_t * pxCurrentTCB.155_6;
  struct xLIST_ITEM * _7;
  struct TCB_t * pxCurrentTCB.156_8;
  struct xLIST_ITEM * _9;
  struct ListItem_t * _10;
  struct TCB_t * pxCurrentTCB.157_11;
  struct ListItem_t * _12;
  struct TCB_t * pxCurrentTCB.158_13;
  long unsigned int _14;
  long unsigned int _15;
  struct TCB_t * pxCurrentTCB.159_16;
  struct List_t * pxOverflowDelayedTaskList.160_17;
  struct TCB_t * pxCurrentTCB.161_18;
  struct ListItem_t * _19;
  struct List_t * pxDelayedTaskList.162_20;
  struct TCB_t * pxCurrentTCB.163_21;
  struct ListItem_t * _22;
  long unsigned int xNextTaskUnblockTime.164_23;

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

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

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

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

  <bb 6> :
  xTimeToWake_38 = xConstTickCount_26 + xTicksToWait_29(D);
  pxCurrentTCB.159_16 ={v} pxCurrentTCB;
  pxCurrentTCB.159_16->xStateListItem.xItemValue = xTimeToWake_38;
  if (xTimeToWake_38 < xConstTickCount_26)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

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

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

  <bb 9> :
  xNextTaskUnblockTime ={v} xTimeToWake_38;

  <bb 10> :
  return;

}


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

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

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

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

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

  <bb 6> :
<L3>:
  return _16;

}


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

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

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

  <bb 4> :

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

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

  <bb 7> :
  iftmp.150_9 ={v} pxCurrentTCB;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.150_7 = xTask_6(D);

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

  <bb 10> :
  pxTCB_10->ucNotifyState[uxIndexToClear_5(D)] ={v} 0;
  xReturn_14 = 1;
  goto <bb 12>; [INV]

  <bb 11> :
  xReturn_12 = 0;

  <bb 12> :
  # xReturn_2 = PHI <xReturn_14(10), xReturn_12(11)>
  vPortExitCritical ();
  _16 = xReturn_2;

  <bb 13> :
<L9>:
  return _16;

}


vTaskGenericNotifyGiveFromISR (struct tskTaskControlBlock * xTaskToNotify, UBaseType_t uxIndexToNotify, BaseType_t * pxHigherPriorityTaskWoken)
{
  uint32_t ulNewMaskValue;
  uint32_t ulNewBASEPRI;
  uint32_t D.8368;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.8367;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  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.147_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.148_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.149_34;
  long unsigned int _35;
  long unsigned int _78;

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

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

  <bb 4> :

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

  <bb 6> :
  if (uxIndexToNotify_42(D) != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 8> :

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

  <bb 10> :
  vPortValidateInterruptPriority ();
  pxTCB_45 = xTaskToNotify_41(D);
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_76, "=r" ulNewBASEPRI_77 : "i" 16 : "memory");
  _78 = ulOriginalBASEPRI_76;

  <bb 11> :
<L23>:
  _82 = _78;

  <bb 12> :
  uxSavedInterruptStatus_46 = _82;
  ucOriginalNotifyState_47 ={v} pxTCB_45->ucNotifyState[uxIndexToNotify_42(D)];
  pxTCB_45->ucNotifyState[uxIndexToNotify_42(D)] ={v} 2;
  _1 ={v} pxTCB_45->ulNotifiedValue[uxIndexToNotify_42(D)];
  _2 = _1 + 1;
  pxTCB_45->ulNotifiedValue[uxIndexToNotify_42(D)] ={v} _2;
  if (ucOriginalNotifyState_47 == 1)
    goto <bb 13>; [INV]
  else
    goto <bb 28>; [INV]

  <bb 13> :
  _3 = pxTCB_45->xEventListItem.pvContainer;
  if (_3 != 0B)
    goto <bb 14>; [INV]
  else
    goto <bb 17>; [INV]

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

  <bb 15> :

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

  <bb 17> :
  uxSchedulerSuspended.147_4 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.147_4 == 0)
    goto <bb 18>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 18> :
  pxList_57 = pxTCB_45->xStateListItem.pvContainer;
  _5 = pxTCB_45->xStateListItem.pxNext;
  _6 = pxTCB_45->xStateListItem.pxPrevious;
  _5->pxPrevious = _6;
  _7 = pxTCB_45->xStateListItem.pxPrevious;
  _8 = pxTCB_45->xStateListItem.pxNext;
  _7->pxNext = _8;
  _9 = pxList_57->pxIndex;
  _10 = &pxTCB_45->xStateListItem;
  if (_9 == _10)
    goto <bb 19>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 19> :
  _11 = pxTCB_45->xStateListItem.pxPrevious;
  pxList_57->pxIndex = _11;

  <bb 20> :
  pxTCB_45->xStateListItem.pvContainer = 0B;
  _12 ={v} pxList_57->uxNumberOfItems;
  _13 = _12 + 4294967295;
  pxList_57->uxNumberOfItems ={v} _13;
  _14 = pxTCB_45->uxPriority;
  uxTopReadyPriority.148_15 ={v} uxTopReadyPriority;
  if (_14 > uxTopReadyPriority.148_15)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  _16 = pxTCB_45->uxPriority;
  uxTopReadyPriority ={v} _16;

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

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

  <bb 24> :
  _33 = pxTCB_45->uxPriority;
  pxCurrentTCB.149_34 ={v} pxCurrentTCB;
  _35 = pxCurrentTCB.149_34->uxPriority;
  if (_33 > _35)
    goto <bb 25>; [INV]
  else
    goto <bb 28>; [INV]

  <bb 25> :
  if (pxHigherPriorityTaskWoken_71(D) != 0B)
    goto <bb 26>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 26> :
  *pxHigherPriorityTaskWoken_71(D) = 1;

  <bb 27> :
  xYieldPending ={v} 1;

  <bb 28> :
  ulNewMaskValue_80 = uxSavedInterruptStatus_46;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_80 : "memory");

  <bb 29> :
  return;

}


xTaskGenericNotifyFromISR (struct tskTaskControlBlock * xTaskToNotify, UBaseType_t uxIndexToNotify, uint32_t ulValue, eNotifyAction eAction, uint32_t * pulPreviousNotificationValue, BaseType_t * pxHigherPriorityTaskWoken)
{
  uint32_t ulNewMaskValue;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.8358;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.8357;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  uint8_t ucOriginalNotifyState;
  struct TCB_t * pxTCB;
  BaseType_t D.8187;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  long unsigned int xTickCount.143_6;
  struct xLIST * _7;
  long unsigned int uxSchedulerSuspended.144_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.145_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.146_38;
  long unsigned int _39;
  BaseType_t _92;
  long unsigned int _97;

  <bb 2> :
  xReturn_50 = 1;
  if (xTaskToNotify_51(D) == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  if (uxIndexToNotify_52(D) != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 8> :

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

  <bb 10> :
  vPortValidateInterruptPriority ();
  pxTCB_55 = xTaskToNotify_51(D);
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_95, "=r" ulNewBASEPRI_96 : "i" 16 : "memory");
  _97 = ulOriginalBASEPRI_95;

  <bb 11> :
<L39>:
  _102 = _97;

  <bb 12> :
  uxSavedInterruptStatus_56 = _102;
  if (pulPreviousNotificationValue_57(D) != 0B)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  _1 ={v} pxTCB_55->ulNotifiedValue[uxIndexToNotify_52(D)];
  *pulPreviousNotificationValue_57(D) = _1;

  <bb 14> :
  ucOriginalNotifyState_59 ={v} pxTCB_55->ucNotifyState[uxIndexToNotify_52(D)];
  pxTCB_55->ucNotifyState[uxIndexToNotify_52(D)] ={v} 2;
  switch (eAction_61(D)) <default: <L16> [INV], case 0: <L15> [INV], case 1: <L8> [INV], case 2: <L9> [INV], case 3: <L10> [INV], case 4: <L11> [INV]>

  <bb 15> :
<L8>:
  _2 ={v} pxTCB_55->ulNotifiedValue[uxIndexToNotify_52(D)];
  _3 = ulValue_63(D) | _2;
  pxTCB_55->ulNotifiedValue[uxIndexToNotify_52(D)] ={v} _3;
  goto <bb 28>; [INV]

  <bb 16> :
<L9>:
  _4 ={v} pxTCB_55->ulNotifiedValue[uxIndexToNotify_52(D)];
  _5 = _4 + 1;
  pxTCB_55->ulNotifiedValue[uxIndexToNotify_52(D)] ={v} _5;
  goto <bb 28>; [INV]

  <bb 17> :
<L10>:
  pxTCB_55->ulNotifiedValue[uxIndexToNotify_52(D)] ={v} ulValue_63(D);
  goto <bb 28>; [INV]

  <bb 18> :
<L11>:
  if (ucOriginalNotifyState_59 != 2)
    goto <bb 19>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 19> :
  pxTCB_55->ulNotifiedValue[uxIndexToNotify_52(D)] ={v} ulValue_63(D);
  goto <bb 21>; [INV]

  <bb 20> :
  xReturn_62 = 0;

  <bb 21> :
  # xReturn_40 = PHI <xReturn_50(19), xReturn_62(20)>
  goto <bb 28>; [INV]

  <bb 22> :
<L15>:
  goto <bb 28>; [INV]

  <bb 23> :
<L16>:
  xTickCount.143_6 ={v} xTickCount;
  if (xTickCount.143_6 != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 27>; [INV]

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

  <bb 25> :

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

  <bb 27> :

  <bb 28> :
  # xReturn_41 = PHI <xReturn_50(15), xReturn_50(16), xReturn_50(17), xReturn_40(21), xReturn_50(22), xReturn_50(27)>
  if (ucOriginalNotifyState_59 == 1)
    goto <bb 29>; [INV]
  else
    goto <bb 44>; [INV]

  <bb 29> :
  _7 = pxTCB_55->xEventListItem.pvContainer;
  if (_7 != 0B)
    goto <bb 30>; [INV]
  else
    goto <bb 33>; [INV]

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

  <bb 31> :

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

  <bb 33> :
  uxSchedulerSuspended.144_8 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.144_8 == 0)
    goto <bb 34>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 34> :
  pxList_75 = pxTCB_55->xStateListItem.pvContainer;
  _9 = pxTCB_55->xStateListItem.pxNext;
  _10 = pxTCB_55->xStateListItem.pxPrevious;
  _9->pxPrevious = _10;
  _11 = pxTCB_55->xStateListItem.pxPrevious;
  _12 = pxTCB_55->xStateListItem.pxNext;
  _11->pxNext = _12;
  _13 = pxList_75->pxIndex;
  _14 = &pxTCB_55->xStateListItem;
  if (_13 == _14)
    goto <bb 35>; [INV]
  else
    goto <bb 36>; [INV]

  <bb 35> :
  _15 = pxTCB_55->xStateListItem.pxPrevious;
  pxList_75->pxIndex = _15;

  <bb 36> :
  pxTCB_55->xStateListItem.pvContainer = 0B;
  _16 ={v} pxList_75->uxNumberOfItems;
  _17 = _16 + 4294967295;
  pxList_75->uxNumberOfItems ={v} _17;
  _18 = pxTCB_55->uxPriority;
  uxTopReadyPriority.145_19 ={v} uxTopReadyPriority;
  if (_18 > uxTopReadyPriority.145_19)
    goto <bb 37>; [INV]
  else
    goto <bb 38>; [INV]

  <bb 37> :
  _20 = pxTCB_55->uxPriority;
  uxTopReadyPriority ={v} _20;

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

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

  <bb 40> :
  _37 = pxTCB_55->uxPriority;
  pxCurrentTCB.146_38 ={v} pxCurrentTCB;
  _39 = pxCurrentTCB.146_38->uxPriority;
  if (_37 > _39)
    goto <bb 41>; [INV]
  else
    goto <bb 44>; [INV]

  <bb 41> :
  if (pxHigherPriorityTaskWoken_89(D) != 0B)
    goto <bb 42>; [INV]
  else
    goto <bb 43>; [INV]

  <bb 42> :
  *pxHigherPriorityTaskWoken_89(D) = 1;

  <bb 43> :
  xYieldPending ={v} 1;

  <bb 44> :
  ulNewMaskValue_100 = uxSavedInterruptStatus_56;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_100 : "memory");

  <bb 45> :
  _92 = xReturn_41;

  <bb 46> :
<L38>:
  return _92;

}


xTaskGenericNotify (struct tskTaskControlBlock * xTaskToNotify, UBaseType_t uxIndexToNotify, uint32_t ulValue, eNotifyAction eAction, uint32_t * pulPreviousNotificationValue)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  uint8_t ucOriginalNotifyState;
  BaseType_t xReturn;
  struct TCB_t * pxTCB;
  BaseType_t D.8158;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  long unsigned int xTickCount.140_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.141_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.142_31;
  long unsigned int _32;
  volatile uint32_t * _33;
  BaseType_t _77;

  <bb 2> :
  xReturn_42 = 1;
  if (uxIndexToNotify_43(D) != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  if (xTaskToNotify_44(D) == 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 8> :

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

  <bb 10> :
  pxTCB_45 = xTaskToNotify_44(D);
  vPortEnterCritical ();
  if (pulPreviousNotificationValue_48(D) != 0B)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  _1 ={v} pxTCB_45->ulNotifiedValue[uxIndexToNotify_43(D)];
  *pulPreviousNotificationValue_48(D) = _1;

  <bb 12> :
  ucOriginalNotifyState_50 ={v} pxTCB_45->ucNotifyState[uxIndexToNotify_43(D)];
  pxTCB_45->ucNotifyState[uxIndexToNotify_43(D)] ={v} 2;
  switch (eAction_52(D)) <default: <L16> [INV], case 0: <L15> [INV], case 1: <L8> [INV], case 2: <L9> [INV], case 3: <L10> [INV], case 4: <L11> [INV]>

  <bb 13> :
<L8>:
  _2 ={v} pxTCB_45->ulNotifiedValue[uxIndexToNotify_43(D)];
  _3 = ulValue_54(D) | _2;
  pxTCB_45->ulNotifiedValue[uxIndexToNotify_43(D)] ={v} _3;
  goto <bb 26>; [INV]

  <bb 14> :
<L9>:
  _4 ={v} pxTCB_45->ulNotifiedValue[uxIndexToNotify_43(D)];
  _5 = _4 + 1;
  pxTCB_45->ulNotifiedValue[uxIndexToNotify_43(D)] ={v} _5;
  goto <bb 26>; [INV]

  <bb 15> :
<L10>:
  pxTCB_45->ulNotifiedValue[uxIndexToNotify_43(D)] ={v} ulValue_54(D);
  goto <bb 26>; [INV]

  <bb 16> :
<L11>:
  if (ucOriginalNotifyState_50 != 2)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  pxTCB_45->ulNotifiedValue[uxIndexToNotify_43(D)] ={v} ulValue_54(D);
  goto <bb 19>; [INV]

  <bb 18> :
  xReturn_53 = 0;

  <bb 19> :
  # xReturn_34 = PHI <xReturn_42(17), xReturn_53(18)>
  goto <bb 26>; [INV]

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

  <bb 21> :
<L16>:
  xTickCount.140_6 ={v} xTickCount;
  if (xTickCount.140_6 != 0)
    goto <bb 22>; [INV]
  else
    goto <bb 25>; [INV]

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

  <bb 23> :

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

  <bb 25> :

  <bb 26> :
  # xReturn_35 = PHI <xReturn_42(13), xReturn_42(14), xReturn_42(15), xReturn_34(19), xReturn_42(20), xReturn_42(25)>
  if (ucOriginalNotifyState_50 == 1)
    goto <bb 27>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 27> :
  pxList_59 = pxTCB_45->xStateListItem.pvContainer;
  _7 = pxTCB_45->xStateListItem.pxNext;
  _8 = pxTCB_45->xStateListItem.pxPrevious;
  _7->pxPrevious = _8;
  _9 = pxTCB_45->xStateListItem.pxPrevious;
  _10 = pxTCB_45->xStateListItem.pxNext;
  _9->pxNext = _10;
  _11 = pxList_59->pxIndex;
  _12 = &pxTCB_45->xStateListItem;
  if (_11 == _12)
    goto <bb 28>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 28> :
  _13 = pxTCB_45->xStateListItem.pxPrevious;
  pxList_59->pxIndex = _13;

  <bb 29> :
  pxTCB_45->xStateListItem.pvContainer = 0B;
  _14 ={v} pxList_59->uxNumberOfItems;
  _15 = _14 + 4294967295;
  pxList_59->uxNumberOfItems ={v} _15;
  _16 = pxTCB_45->uxPriority;
  uxTopReadyPriority.141_17 ={v} uxTopReadyPriority;
  if (_16 > uxTopReadyPriority.141_17)
    goto <bb 30>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 30> :
  _18 = pxTCB_45->uxPriority;
  uxTopReadyPriority ={v} _18;

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

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

  <bb 33> :

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

  <bb 35> :
  _30 = pxTCB_45->uxPriority;
  pxCurrentTCB.142_31 ={v} pxCurrentTCB;
  _32 = pxCurrentTCB.142_31->uxPriority;
  if (_30 > _32)
    goto <bb 36>; [INV]
  else
    goto <bb 37>; [INV]

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

  <bb 37> :
  vPortExitCritical ();
  _77 = xReturn_35;

  <bb 38> :
<L34>:
  return _77;

}


xTaskGenericNotifyWait (UBaseType_t uxIndexToWait, uint32_t ulBitsToClearOnEntry, uint32_t ulBitsToClearOnExit, uint32_t * pulNotificationValue, TickType_t xTicksToWait)
{
  uint32_t ulNewBASEPRI;
  BaseType_t xReturn;
  BaseType_t D.8133;
  struct TCB_t * pxCurrentTCB.138;
  struct TCB_t * pxCurrentTCB.134;
  struct TCB_t * pxCurrentTCB.133_1;
  unsigned char _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  struct TCB_t * pxCurrentTCB.135_6;
  volatile uint32_t * _7;
  struct TCB_t * pxCurrentTCB.136_8;
  long unsigned int _9;
  struct TCB_t * pxCurrentTCB.137_10;
  unsigned char _11;
  long unsigned int _12;
  long unsigned int _13;
  long unsigned int _14;
  struct TCB_t * pxCurrentTCB.139_15;
  struct TCB_t * pxCurrentTCB.134_23;
  struct TCB_t * pxCurrentTCB.138_36;
  BaseType_t _43;

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

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

  <bb 4> :

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

  <bb 6> :
  vPortEnterCritical ();
  pxCurrentTCB.133_1 ={v} pxCurrentTCB;
  _2 ={v} pxCurrentTCB.133_1->ucNotifyState[uxIndexToWait_20(D)];
  if (_2 != 2)
    goto <bb 7>; [INV]
  else
    goto <bb 9>; [INV]

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

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

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

  <bb 10> :
  pxCurrentTCB.136_8 ={v} pxCurrentTCB;
  _9 ={v} pxCurrentTCB.136_8->ulNotifiedValue[uxIndexToWait_20(D)];
  *pulNotificationValue_34(D) = _9;

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

  <bb 12> :
  xReturn_40 = 0;
  goto <bb 14>; [INV]

  <bb 13> :
  pxCurrentTCB.138_36 ={v} pxCurrentTCB;
  _12 ={v} pxCurrentTCB.138_36->ulNotifiedValue[uxIndexToWait_20(D)];
  _13 = ~ulBitsToClearOnExit_37(D);
  _14 = _12 & _13;
  pxCurrentTCB.138_36->ulNotifiedValue[uxIndexToWait_20(D)] ={v} _14;
  xReturn_39 = 1;

  <bb 14> :
  # xReturn_16 = PHI <xReturn_40(12), xReturn_39(13)>
  pxCurrentTCB.139_15 ={v} pxCurrentTCB;
  pxCurrentTCB.139_15->ucNotifyState[uxIndexToWait_20(D)] ={v} 0;
  vPortExitCritical ();
  _43 = xReturn_16;

  <bb 15> :
<L14>:
  return _43;

}


ulTaskGenericNotifyTake (UBaseType_t uxIndexToWait, BaseType_t xClearCountOnExit, TickType_t xTicksToWait)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulReturn;
  uint32_t D.8116;
  struct TCB_t * pxCurrentTCB.127_1;
  long unsigned int _2;
  struct TCB_t * pxCurrentTCB.128_3;
  volatile uint32_t * _4;
  struct TCB_t * pxCurrentTCB.129_5;
  struct TCB_t * pxCurrentTCB.130_6;
  struct TCB_t * pxCurrentTCB.131_7;
  long unsigned int _8;
  struct TCB_t * pxCurrentTCB.132_9;
  uint32_t _29;

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

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

  <bb 4> :

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

  <bb 6> :
  vPortEnterCritical ();
  pxCurrentTCB.127_1 ={v} pxCurrentTCB;
  _2 ={v} pxCurrentTCB.127_1->ulNotifiedValue[uxIndexToWait_12(D)];
  if (_2 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 9>; [INV]

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

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

  <bb 9> :
  vPortExitCritical ();
  vPortEnterCritical ();
  pxCurrentTCB.129_5 ={v} pxCurrentTCB;
  ulReturn_23 ={v} pxCurrentTCB.129_5->ulNotifiedValue[uxIndexToWait_12(D)];
  if (ulReturn_23 != 0)
    goto <bb 10>; [INV]
  else
    goto <bb 13>; [INV]

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

  <bb 11> :
  pxCurrentTCB.130_6 ={v} pxCurrentTCB;
  pxCurrentTCB.130_6->ulNotifiedValue[uxIndexToWait_12(D)] ={v} 0;
  goto <bb 13>; [INV]

  <bb 12> :
  pxCurrentTCB.131_7 ={v} pxCurrentTCB;
  _8 = ulReturn_23 + 4294967295;
  pxCurrentTCB.131_7->ulNotifiedValue[uxIndexToWait_12(D)] ={v} _8;

  <bb 13> :
  pxCurrentTCB.132_9 ={v} pxCurrentTCB;
  pxCurrentTCB.132_9->ucNotifyState[uxIndexToWait_12(D)] ={v} 0;
  vPortExitCritical ();
  _29 = ulReturn_23;

  <bb 14> :
<L15>:
  return _29;

}


pvTaskIncrementMutexHeldCount ()
{
  struct tskTaskControlBlock * D.8100;
  struct TCB_t * pxCurrentTCB.125_1;
  struct TCB_t * pxCurrentTCB.126_2;
  long unsigned int _3;
  long unsigned int _4;
  struct tskTaskControlBlock * _8;

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

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

  <bb 4> :
  _8 ={v} pxCurrentTCB;

  <bb 5> :
<L2>:
  return _8;

}


uxTaskResetEventItemValue ()
{
  TickType_t uxReturn;
  TickType_t D.8096;
  struct TCB_t * pxCurrentTCB.122_1;
  struct TCB_t * pxCurrentTCB.123_2;
  long unsigned int _3;
  struct TCB_t * pxCurrentTCB.124_4;
  long unsigned int _5;
  TickType_t _9;

  <bb 2> :
  pxCurrentTCB.122_1 ={v} pxCurrentTCB;
  uxReturn_7 = pxCurrentTCB.122_1->xEventListItem.xItemValue;
  pxCurrentTCB.123_2 ={v} pxCurrentTCB;
  _3 = pxCurrentTCB.123_2->uxPriority;
  pxCurrentTCB.124_4 ={v} pxCurrentTCB;
  _5 = 5 - _3;
  pxCurrentTCB.124_4->xEventListItem.xItemValue = _5;
  _9 = uxReturn_7;

  <bb 3> :
<L0>:
  return _9;

}


vTaskList (char * pcWriteBuffer)
{
  char cStatus;
  UBaseType_t x;
  UBaseType_t uxArraySize;
  struct TaskStatus_t * pxTaskStatusArray;
  long unsigned int uxCurrentNumberOfTasks.121_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> :
  *pcWriteBuffer_27(D) = 0;
  uxArraySize_29 ={v} uxCurrentNumberOfTasks;
  uxCurrentNumberOfTasks.121_1 ={v} uxCurrentNumberOfTasks;
  _2 = uxCurrentNumberOfTasks.121_1 * 36;
  pxTaskStatusArray_31 = pvPortMalloc (_2);
  if (pxTaskStatusArray_31 != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 14>; [INV]

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

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

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

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

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

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

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

  <bb 11> :
  # cStatus_23 = PHI <cStatus_40(5), cStatus_39(6), cStatus_38(7), cStatus_37(8), cStatus_36(9), cStatus_41(10)>
  _6 = x_22 * 36;
  _7 = pxTaskStatusArray_31 + _6;
  _8 = _7->pcTaskName;
  pcWriteBuffer_43 = prvWriteNameToBuffer (pcWriteBuffer_21, _8);
  _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);
  _20 = strlen (pcWriteBuffer_43);
  pcWriteBuffer_45 = pcWriteBuffer_43 + _20;
  x_46 = x_22 + 1;

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

  <bb 13> :
  vPortFree (pxTaskStatusArray_31);

  <bb 14> :
  return;

}


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

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

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

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

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

  <bb 6> :
<L3>:
  return _11;

}


vTaskPriorityDisinheritAfterTimeout (struct tskTaskControlBlock * const pxMutexHolder, UBaseType_t uxHighestPriorityWaitingTask)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  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.119_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.120_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> :
  pxTCB_31 = pxMutexHolder_30(D);
  uxOnlyOneMutexHeld_32 = 1;
  if (pxMutexHolder_30(D) != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 23>; [INV]

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

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

  <bb 5> :

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

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

  <bb 8> :
  uxPriorityToUse_36 = uxHighestPriorityWaitingTask_34(D);
  goto <bb 10>; [INV]

  <bb 9> :
  uxPriorityToUse_35 = pxTCB_31->uxBasePriority;

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

  <bb 11> :
  _4 = pxTCB_31->uxMutexesHeld;
  if (uxOnlyOneMutexHeld_32 == _4)
    goto <bb 12>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 12> :
  pxCurrentTCB.119_5 ={v} pxCurrentTCB;
  if (pxTCB_31 == pxCurrentTCB.119_5)
    goto <bb 13>; [INV]
  else
    goto <bb 16>; [INV]

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

  <bb 14> :

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

  <bb 16> :
  uxPriorityUsedOnEntry_37 = pxTCB_31->uxPriority;
  pxTCB_31->uxPriority = uxPriorityToUse_26;
  _6 = pxTCB_31->xEventListItem.xItemValue;
  _7 = (signed int) _6;
  if (_7 >= 0)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  _8 = 5 - uxPriorityToUse_26;
  pxTCB_31->xEventListItem.xItemValue = _8;

  <bb 18> :
  _9 = pxTCB_31->xStateListItem.pvContainer;
  _10 = &pxReadyTasksLists[uxPriorityUsedOnEntry_37];
  if (_9 == _10)
    goto <bb 19>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 19> :
  _11 = &pxTCB_31->xStateListItem;
  _12 = uxListRemove (_11);

  <bb 20> :
  _13 = pxTCB_31->uxPriority;
  uxTopReadyPriority.120_14 ={v} uxTopReadyPriority;
  if (_13 > uxTopReadyPriority.120_14)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  _15 = pxTCB_31->uxPriority;
  uxTopReadyPriority ={v} _15;

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

  <bb 23> :
  return;

}


xTaskPriorityDisinherit (struct tskTaskControlBlock * const pxMutexHolder)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  BaseType_t xReturn;
  struct TCB_t * const pxTCB;
  BaseType_t D.8062;
  struct TCB_t * pxCurrentTCB.117_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.118_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 _46;

  <bb 2> :
  pxTCB_30 = pxMutexHolder_29(D);
  xReturn_31 = 0;
  if (pxMutexHolder_29(D) != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 3> :
  pxCurrentTCB.117_1 ={v} pxCurrentTCB;
  if (pxTCB_30 != pxCurrentTCB.117_1)
    goto <bb 4>; [INV]
  else
    goto <bb 7>; [INV]

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

  <bb 5> :

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

  <bb 7> :
  _2 = pxTCB_30->uxMutexesHeld;
  if (_2 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 11>; [INV]

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

  <bb 9> :

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

  <bb 11> :
  _3 = pxTCB_30->uxMutexesHeld;
  _4 = _3 + 4294967295;
  pxTCB_30->uxMutexesHeld = _4;
  _5 = pxTCB_30->uxPriority;
  _6 = pxTCB_30->uxBasePriority;
  if (_5 != _6)
    goto <bb 12>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 12> :
  _7 = pxTCB_30->uxMutexesHeld;
  if (_7 == 0)
    goto <bb 13>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 13> :
  _8 = &pxTCB_30->xStateListItem;
  _9 = uxListRemove (_8);

  <bb 14> :
  _10 = pxTCB_30->uxBasePriority;
  pxTCB_30->uxPriority = _10;
  _11 = pxTCB_30->uxPriority;
  _12 = 5 - _11;
  pxTCB_30->xEventListItem.xItemValue = _12;
  _13 = pxTCB_30->uxPriority;
  uxTopReadyPriority.118_14 ={v} uxTopReadyPriority;
  if (_13 > uxTopReadyPriority.118_14)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  _15 = pxTCB_30->uxPriority;
  uxTopReadyPriority ={v} _15;

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

  <bb 17> :
  # xReturn_26 = PHI <xReturn_31(2), xReturn_45(16), xReturn_31(11), xReturn_31(12)>
  _46 = xReturn_26;

  <bb 18> :
<L20>:
  return _46;

}


xTaskPriorityInherit (struct tskTaskControlBlock * const pxMutexHolder)
{
  struct ListItem_t * const pxIndex;
  BaseType_t xReturn;
  struct TCB_t * const pxMutexHolderTCB;
  BaseType_t D.8042;
  long unsigned int _1;
  struct TCB_t * pxCurrentTCB.111_2;
  long unsigned int _3;
  long unsigned int _4;
  signed int _5;
  struct TCB_t * pxCurrentTCB.112_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.113_14;
  long unsigned int _15;
  long unsigned int _16;
  long unsigned int uxTopReadyPriority.114_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.115_29;
  long unsigned int _30;
  long unsigned int _31;
  struct TCB_t * pxCurrentTCB.116_32;
  long unsigned int _33;
  BaseType_t _57;

  <bb 2> :
  pxMutexHolderTCB_40 = pxMutexHolder_39(D);
  xReturn_41 = 0;
  if (pxMutexHolder_39(D) != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 15>; [INV]

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

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

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

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

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

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

  <bb 9> :
  _18 = pxMutexHolderTCB_40->uxPriority;
  uxTopReadyPriority ={v} _18;

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

  <bb 11> :
  pxCurrentTCB.115_29 ={v} pxCurrentTCB;
  _30 = pxCurrentTCB.115_29->uxPriority;
  pxMutexHolderTCB_40->uxPriority = _30;

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

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

  <bb 14> :
  xReturn_43 = 1;

  <bb 15> :
  # xReturn_34 = PHI <xReturn_41(2), xReturn_41(13), xReturn_56(12), xReturn_43(14)>
  _57 = xReturn_34;

  <bb 16> :
<L20>:
  return _57;

}


xTaskGetSchedulerState ()
{
  BaseType_t xReturn;
  BaseType_t D.8020;
  long int xSchedulerRunning.109_1;
  long unsigned int uxSchedulerSuspended.110_2;
  BaseType_t _8;

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

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

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

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

  <bb 6> :
  xReturn_5 = 0;

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

  <bb 8> :
<L6>:
  return _8;

}


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

  <bb 2> :
  xReturn_2 ={v} pxCurrentTCB;
  _3 = xReturn_2;

  <bb 3> :
<L0>:
  return _3;

}


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

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

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

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

  <bb 5> :
  return;

}


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

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

}


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

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

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

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

  <bb 5> :
  # iftmp.106_2 = PHI <iftmp.106_6(3), iftmp.106_4(4)>
  pxTCB_7 = iftmp.106_2;
  pucEndOfStack_8 = pxTCB_7->pxStack;
  _1 = prvTaskCheckFreeStackSpace (pucEndOfStack_8);
  uxReturn_10 = (UBaseType_t) _1;
  _11 = uxReturn_10;

  <bb 6> :
<L3>:
  return _11;

}


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

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

  <bb 3> :
  pucStackByte_9 = pucStackByte_2 + 1;
  ulCount_10 = ulCount_3 + 1;

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

  <bb 5> :
  ulCount_7 = ulCount_3 / 4;
  _8 = (uint16_t) ulCount_7;

  <bb 6> :
<L3>:
  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;
  UBaseType_t D.7999;
  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> :
  uxTask_24 = 0;
  _1 ={v} pxList_26(D)->uxNumberOfItems;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 9>; [INV]

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

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

  <bb 5> :
  _8 = pxConstList_27->pxIndex;
  pxFirstTCB_30 = _8->pvOwner;

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

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

  <bb 8> :
  _15 = pxConstList_31->pxIndex;
  pxNextTCB_34 = _15->pvOwner;
  _16 = uxTask_18 * 36;
  _17 = pxTaskStatusArray_35(D) + _16;
  vTaskGetInfo (pxNextTCB_34, _17, 1, eState_36(D));
  uxTask_38 = uxTask_18 + 1;
  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)>
  _39 = uxTask_19;

  <bb 10> :
<L9>:
  return _39;

}


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

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

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

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

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

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

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

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

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

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

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

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

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

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

  <bb 15> :
  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.101_3;
  long unsigned int _4;
  long unsigned int uxDeletedTasksWaitingCleanUp.102_5;
  long unsigned int _6;
  long unsigned int uxDeletedTasksWaitingCleanUp.103_7;

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

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

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

  <bb 5> :
  return;

}


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

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

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

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

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

}


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

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

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

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

}


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

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

  <bb 3> :
  pxTCB_4 = xTask_2(D);
  pxTCB_4->uxTaskNumber = uxHandle_5(D);

  <bb 4> :
  return;

}


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

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

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

  <bb 4> :
  uxReturn_3 = 0;

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

  <bb 6> :
<L3>:
  return _7;

}


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

}


xTaskCheckForTimeOut (struct TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  const TickType_t xElapsedTime;
  const TickType_t xConstTickCount;
  BaseType_t xReturn;
  BaseType_t D.7963;
  long unsigned int _1;
  struct TCB_t * pxCurrentTCB.98_2;
  unsigned char _3;
  struct TCB_t * pxCurrentTCB.99_4;
  long unsigned int _5;
  long int _6;
  long int xNumOfOverflows.100_7;
  long unsigned int _8;
  long unsigned int _9;
  long unsigned int _10;
  long unsigned int _11;
  BaseType_t _31;

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

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

  <bb 4> :

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

  <bb 6> :
  if (pxTicksToWait_15(D) == 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 8> :

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

  <bb 10> :
  vPortEnterCritical ();
  xConstTickCount_18 ={v} xTickCount;
  _1 = pxTimeOut_14(D)->xTimeOnEntering;
  xElapsedTime_19 = xConstTickCount_18 - _1;
  pxCurrentTCB.98_2 ={v} pxCurrentTCB;
  _3 = pxCurrentTCB.98_2->ucDelayAborted;
  if (_3 != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  pxCurrentTCB.99_4 ={v} pxCurrentTCB;
  pxCurrentTCB.99_4->ucDelayAborted = 0;
  xReturn_29 = 1;
  goto <bb 20>; [INV]

  <bb 12> :
  _5 = *pxTicksToWait_15(D);
  if (_5 == 4294967295)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  xReturn_27 = 0;
  goto <bb 20>; [INV]

  <bb 14> :
  _6 = pxTimeOut_14(D)->xOverflowCount;
  xNumOfOverflows.100_7 ={v} xNumOfOverflows;
  if (_6 != xNumOfOverflows.100_7)
    goto <bb 15>; [INV]
  else
    goto <bb 17>; [INV]

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

  <bb 16> :
  xReturn_20 = 1;
  *pxTicksToWait_15(D) = 0;
  goto <bb 20>; [INV]

  <bb 17> :
  _9 = *pxTicksToWait_15(D);
  if (xElapsedTime_19 < _9)
    goto <bb 18>; [INV]
  else
    goto <bb 19>; [INV]

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

  <bb 19> :
  *pxTicksToWait_15(D) = 0;
  xReturn_23 = 1;

  <bb 20> :
  # xReturn_12 = PHI <xReturn_29(11), xReturn_27(13), xReturn_20(16), xReturn_26(18), xReturn_23(19)>
  vPortExitCritical ();
  _31 = xReturn_12;

  <bb 21> :
<L19>:
  return _31;

}


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

  <bb 2> :
  xNumOfOverflows.96_1 ={v} xNumOfOverflows;
  pxTimeOut_4(D)->xOverflowCount = xNumOfOverflows.96_1;
  xTickCount.97_2 ={v} xTickCount;
  pxTimeOut_4(D)->xTimeOnEntering = xTickCount.97_2;
  return;

}


vTaskSetTimeOutState (struct TimeOut_t * const pxTimeOut)
{
  uint32_t ulNewBASEPRI;
  long int xNumOfOverflows.94_1;
  long unsigned int xTickCount.95_2;

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

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

  <bb 4> :

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

  <bb 6> :
  vPortEnterCritical ();
  xNumOfOverflows.94_1 ={v} xNumOfOverflows;
  pxTimeOut_3(D)->xOverflowCount = xNumOfOverflows.94_1;
  xTickCount.95_2 ={v} xTickCount;
  pxTimeOut_3(D)->xTimeOnEntering = xTickCount.95_2;
  vPortExitCritical ();
  return;

}


vTaskRemoveFromUnorderedEventList (struct ListItem_t * pxEventListItem, const TickType_t xItemValue)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  struct List_t * const pxList;
  struct TCB_t * pxUnblockedTCB;
  long unsigned int uxSchedulerSuspended.91_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.92_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.93_34;
  long unsigned int _35;

  <bb 2> :
  uxSchedulerSuspended.91_1 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.91_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  _2 = xItemValue_41(D) | 2147483648;
  pxEventListItem_42(D)->xItemValue = _2;
  pxUnblockedTCB_44 = pxEventListItem_42(D)->pvOwner;
  if (pxUnblockedTCB_44 == 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 8> :

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

  <bb 10> :
  pxList_45 = pxEventListItem_42(D)->pvContainer;
  _3 = pxEventListItem_42(D)->pxNext;
  _4 = pxEventListItem_42(D)->pxPrevious;
  _3->pxPrevious = _4;
  _5 = pxEventListItem_42(D)->pxPrevious;
  _6 = pxEventListItem_42(D)->pxNext;
  _5->pxNext = _6;
  _7 = pxList_45->pxIndex;
  if (pxEventListItem_42(D) == _7)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  _8 = pxEventListItem_42(D)->pxPrevious;
  pxList_45->pxIndex = _8;

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

  <bb 13> :
  _17 = pxUnblockedTCB_44->xStateListItem.pxPrevious;
  pxList_51->pxIndex = _17;

  <bb 14> :
  pxUnblockedTCB_44->xStateListItem.pvContainer = 0B;
  _18 ={v} pxList_51->uxNumberOfItems;
  _19 = _18 + 4294967295;
  pxList_51->uxNumberOfItems ={v} _19;
  _20 = pxUnblockedTCB_44->uxPriority;
  uxTopReadyPriority.92_21 ={v} uxTopReadyPriority;
  if (_20 > uxTopReadyPriority.92_21)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  _22 = pxUnblockedTCB_44->uxPriority;
  uxTopReadyPriority ={v} _22;

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

  <bb 17> :
  xYieldPending ={v} 1;

  <bb 18> :
  return;

}


xTaskRemoveFromEventList (const struct List_t * const pxEventList)
{
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  struct List_t * const pxList;
  BaseType_t xReturn;
  struct TCB_t * pxUnblockedTCB;
  BaseType_t D.7930;
  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.88_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.89_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.90_41;
  long unsigned int _42;
  BaseType_t _82;

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

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

  <bb 4> :

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

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

  <bb 7> :
  _8 = pxUnblockedTCB_51->xEventListItem.pxPrevious;
  pxList_52->pxIndex = _8;

  <bb 8> :
  pxUnblockedTCB_51->xEventListItem.pvContainer = 0B;
  _9 ={v} pxList_52->uxNumberOfItems;
  _10 = _9 + 4294967295;
  pxList_52->uxNumberOfItems ={v} _10;
  uxSchedulerSuspended.88_11 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.88_11 == 0)
    goto <bb 9>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 10> :
  _18 = pxUnblockedTCB_51->xStateListItem.pxPrevious;
  pxList_65->pxIndex = _18;

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

  <bb 12> :
  _23 = pxUnblockedTCB_51->uxPriority;
  uxTopReadyPriority ={v} _23;

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

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

  <bb 15> :
  _40 = pxUnblockedTCB_51->uxPriority;
  pxCurrentTCB.90_41 ={v} pxCurrentTCB;
  _42 = pxCurrentTCB.90_41->uxPriority;
  if (_40 > _42)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  xReturn_80 = 1;
  xYieldPending ={v} 1;
  goto <bb 18>; [INV]

  <bb 17> :
  xReturn_79 = 0;

  <bb 18> :
  # xReturn_43 = PHI <xReturn_80(16), xReturn_79(17)>
  _82 = xReturn_43;

  <bb 19> :
<L15>:
  return _82;

}


vTaskPlaceOnEventListRestricted (struct List_t * const pxEventList, TickType_t xTicksToWait, const BaseType_t xWaitIndefinitely)
{
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  struct TCB_t * pxCurrentTCB.83_1;
  struct TCB_t * pxCurrentTCB.84_2;
  struct xLIST_ITEM * _3;
  struct TCB_t * pxCurrentTCB.85_4;
  struct xLIST_ITEM * _5;
  struct ListItem_t * _6;
  struct TCB_t * pxCurrentTCB.86_7;
  struct ListItem_t * _8;
  struct TCB_t * pxCurrentTCB.87_9;
  long unsigned int _10;
  long unsigned int _11;

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

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

  <bb 4> :

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

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

  <bb 7> :
  xTicksToWait_24 = 4294967295;

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

}


vTaskPlaceOnUnorderedEventList (struct List_t * pxEventList, const TickType_t xItemValue, const TickType_t xTicksToWait)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  long unsigned int uxSchedulerSuspended.76_1;
  struct TCB_t * pxCurrentTCB.77_2;
  long unsigned int _3;
  struct TCB_t * pxCurrentTCB.78_4;
  struct TCB_t * pxCurrentTCB.79_5;
  struct xLIST_ITEM * _6;
  struct TCB_t * pxCurrentTCB.80_7;
  struct xLIST_ITEM * _8;
  struct ListItem_t * _9;
  struct TCB_t * pxCurrentTCB.81_10;
  struct ListItem_t * _11;
  struct TCB_t * pxCurrentTCB.82_12;
  long unsigned int _13;
  long unsigned int _14;

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

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

  <bb 4> :

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

  <bb 6> :
  uxSchedulerSuspended.76_1 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.76_1 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 8> :

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

  <bb 10> :
  pxCurrentTCB.77_2 ={v} pxCurrentTCB;
  _3 = xItemValue_17(D) | 2147483648;
  pxCurrentTCB.77_2->xEventListItem.xItemValue = _3;
  pxIndex_19 = pxEventList_15(D)->pxIndex;
  pxCurrentTCB.78_4 ={v} pxCurrentTCB;
  pxCurrentTCB.78_4->xEventListItem.pxNext = pxIndex_19;
  pxCurrentTCB.79_5 ={v} pxCurrentTCB;
  _6 = pxIndex_19->pxPrevious;
  pxCurrentTCB.79_5->xEventListItem.pxPrevious = _6;
  pxCurrentTCB.80_7 ={v} pxCurrentTCB;
  _8 = pxIndex_19->pxPrevious;
  _9 = &pxCurrentTCB.80_7->xEventListItem;
  _8->pxNext = _9;
  pxCurrentTCB.81_10 ={v} pxCurrentTCB;
  _11 = &pxCurrentTCB.81_10->xEventListItem;
  pxIndex_19->pxPrevious = _11;
  pxCurrentTCB.82_12 ={v} pxCurrentTCB;
  pxCurrentTCB.82_12->xEventListItem.pvContainer = pxEventList_15(D);
  _13 ={v} pxEventList_15(D)->uxNumberOfItems;
  _14 = _13 + 1;
  pxEventList_15(D)->uxNumberOfItems ={v} _14;
  prvAddCurrentTaskToDelayedList (xTicksToWait_26(D), 1);
  return;

}


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

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

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

  <bb 4> :

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

  <bb 6> :
  pxCurrentTCB.75_1 ={v} pxCurrentTCB;
  _2 = &pxCurrentTCB.75_1->xEventListItem;
  vListInsert (pxEventList_3(D), _2);
  prvAddCurrentTaskToDelayedList (xTicksToWait_6(D), 1);
  return;

}


__attribute__((used))
vTaskSwitchContext ()
{
  uint32_t ulNewBASEPRI;
  struct List_t * const pxConstList;
  UBaseType_t uxTopPriority;
  long unsigned int uxSchedulerSuspended.74_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> :
  uxSchedulerSuspended.74_1 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.74_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  xYieldPending ={v} 1;
  goto <bb 14>; [INV]

  <bb 4> :
  xYieldPending ={v} 0;
  uxTopPriority_16 ={v} uxTopReadyPriority;
  goto <bb 10>; [INV]

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

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

  <bb 7> :

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

  <bb 9> :
  uxTopPriority_22 = uxTopPriority_11 + 4294967295;

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

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

  <bb 12> :
  _7 = pxConstList_17->pxIndex;
  _8 = _7->pxNext;
  pxConstList_17->pxIndex = _8;

  <bb 13> :
  _9 = pxConstList_17->pxIndex;
  _10 = _9->pvOwner;
  pxCurrentTCB ={v} _10;
  uxTopReadyPriority ={v} uxTopPriority_11;

  <bb 14> :
  return;

}


xTaskIncrementTick ()
{
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  struct List_t * const pxList;
  struct List_t * pxTemp;
  const TickType_t xConstTickCount;
  BaseType_t xSwitchRequired;
  TickType_t xItemValue;
  struct TCB_t * pxTCB;
  BaseType_t D.7897;
  long unsigned int uxSchedulerSuspended.61_1;
  long unsigned int xTickCount.62_2;
  struct List_t * pxDelayedTaskList.63_3;
  long unsigned int _4;
  struct List_t * pxOverflowDelayedTaskList.64_5;
  long int xNumOfOverflows.65_6;
  long int _7;
  long unsigned int xNextTaskUnblockTime.66_8;
  struct List_t * pxDelayedTaskList.67_9;
  long unsigned int _10;
  struct List_t * pxDelayedTaskList.68_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.69_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.70_46;
  long unsigned int _47;
  struct TCB_t * pxCurrentTCB.71_48;
  long unsigned int _49;
  long unsigned int _50;
  long int xYieldPending.72_51;
  long unsigned int xPendedTicks.73_52;
  long unsigned int _53;
  BaseType_t _104;

  <bb 2> :
  xSwitchRequired_67 = 0;
  uxSchedulerSuspended.61_1 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.61_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 3> :
  xTickCount.62_2 ={v} xTickCount;
  xConstTickCount_70 = xTickCount.62_2 + 1;
  xTickCount ={v} xConstTickCount_70;
  if (xConstTickCount_70 == 0)
    goto <bb 4>; [INV]
  else
    goto <bb 9>; [INV]

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

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

  <bb 6> :

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

  <bb 8> :
  pxTemp_72 ={v} pxDelayedTaskList;
  pxOverflowDelayedTaskList.64_5 ={v} pxOverflowDelayedTaskList;
  pxDelayedTaskList ={v} pxOverflowDelayedTaskList.64_5;
  pxOverflowDelayedTaskList ={v} pxTemp_72;
  xNumOfOverflows.65_6 ={v} xNumOfOverflows;
  _7 = xNumOfOverflows.65_6 + 1;
  xNumOfOverflows ={v} _7;
  prvResetNextTaskUnblockTime ();

  <bb 9> :
  xNextTaskUnblockTime.66_8 ={v} xNextTaskUnblockTime;
  if (xConstTickCount_70 >= xNextTaskUnblockTime.66_8)
    goto <bb 10>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 10> :
  # xSwitchRequired_54 = PHI <xSwitchRequired_67(9), xSwitchRequired_55(24)>
  pxDelayedTaskList.67_9 ={v} pxDelayedTaskList;
  _10 ={v} pxDelayedTaskList.67_9->uxNumberOfItems;
  if (_10 == 0)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  xNextTaskUnblockTime ={v} 4294967295;
  goto <bb 25>; [INV]

  <bb 12> :
  pxDelayedTaskList.68_11 ={v} pxDelayedTaskList;
  _12 = pxDelayedTaskList.68_11->xListEnd.pxNext;
  pxTCB_77 = _12->pvOwner;
  xItemValue_78 = pxTCB_77->xStateListItem.xItemValue;
  if (xConstTickCount_70 < xItemValue_78)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  xNextTaskUnblockTime ={v} xItemValue_78;
  goto <bb 25>; [INV]

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

  <bb 15> :
  _19 = pxTCB_77->xStateListItem.pxPrevious;
  pxList_79->pxIndex = _19;

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

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

  <bb 18> :
  _29 = pxTCB_77->xEventListItem.pxPrevious;
  pxList_85->pxIndex = _29;

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

  <bb 20> :
  _32 = pxTCB_77->uxPriority;
  uxTopReadyPriority.69_33 ={v} uxTopReadyPriority;
  if (_32 > uxTopReadyPriority.69_33)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  _34 = pxTCB_77->uxPriority;
  uxTopReadyPriority ={v} _34;

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

  <bb 23> :
  xSwitchRequired_99 = 1;

  <bb 24> :
  # xSwitchRequired_55 = PHI <xSwitchRequired_54(22), xSwitchRequired_99(23)>
  goto <bb 10>; [INV]

  <bb 25> :
  # xSwitchRequired_56 = PHI <xSwitchRequired_67(9), xSwitchRequired_54(11), xSwitchRequired_54(13)>
  pxCurrentTCB.71_48 ={v} pxCurrentTCB;
  _49 = pxCurrentTCB.71_48->uxPriority;
  _50 ={v} pxReadyTasksLists[_49].uxNumberOfItems;
  if (_50 > 1)
    goto <bb 26>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 26> :
  xSwitchRequired_102 = 1;

  <bb 27> :
  # xSwitchRequired_57 = PHI <xSwitchRequired_56(25), xSwitchRequired_102(26)>
  xYieldPending.72_51 ={v} xYieldPending;
  if (xYieldPending.72_51 != 0)
    goto <bb 28>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 28> :
  xSwitchRequired_103 = 1;
  goto <bb 30>; [INV]

  <bb 29> :
  xPendedTicks.73_52 ={v} xPendedTicks;
  _53 = xPendedTicks.73_52 + 1;
  xPendedTicks ={v} _53;

  <bb 30> :
  # xSwitchRequired_58 = PHI <xSwitchRequired_103(28), xSwitchRequired_67(29), xSwitchRequired_57(27)>
  _104 = xSwitchRequired_58;

  <bb 31> :
<L35>:
  return _104;

}


xTaskAbortDelay (struct tskTaskControlBlock * xTask)
{
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  BaseType_t xReturn;
  struct TCB_t * pxTCB;
  BaseType_t D.7863;
  <unnamed type> _1;
  struct ListItem_t * _2;
  struct xLIST * _3;
  struct ListItem_t * _4;
  long unsigned int _5;
  long unsigned int uxTopReadyPriority.59_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.60_19;
  long unsigned int _20;
  BaseType_t _47;

  <bb 2> :
  pxTCB_26 = xTask_25(D);
  if (pxTCB_26 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  vTaskSuspendAll ();
  _1 = eTaskGetState (xTask_25(D));
  if (_1 == 2)
    goto <bb 7>; [INV]
  else
    goto <bb 13>; [INV]

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

  <bb 8> :
  _4 = &pxTCB_26->xEventListItem;
  uxListRemove (_4);
  pxTCB_26->ucDelayAborted = 1;

  <bb 9> :
  vPortExitCritical ();
  _5 = pxTCB_26->uxPriority;
  uxTopReadyPriority.59_6 ={v} uxTopReadyPriority;
  if (_5 > uxTopReadyPriority.59_6)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  _7 = pxTCB_26->uxPriority;
  uxTopReadyPriority ={v} _7;

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

  <bb 12> :
  xYieldPending ={v} 1;
  goto <bb 14>; [INV]

  <bb 13> :
  xReturn_30 = 0;

  <bb 14> :
  # xReturn_21 = PHI <xReturn_31(12), xReturn_30(13), xReturn_31(11)>
  xTaskResumeAll ();
  _47 = xReturn_21;

  <bb 15> :
<L14>:
  return _47;

}


xTaskCatchUpTicks (TickType_t xTicksToCatchUp)
{
  uint32_t ulNewBASEPRI;
  BaseType_t xYieldOccurred;
  BaseType_t D.7848;
  long unsigned int uxSchedulerSuspended.57_1;
  long unsigned int xPendedTicks.58_2;
  long unsigned int _3;
  BaseType_t _10;

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

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

  <bb 4> :

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

  <bb 6> :
  vTaskSuspendAll ();
  xPendedTicks.58_2 ={v} xPendedTicks;
  _3 = xTicksToCatchUp_6(D) + xPendedTicks.58_2;
  xPendedTicks ={v} _3;
  xYieldOccurred_9 = xTaskResumeAll ();
  _10 = xYieldOccurred_9;

  <bb 7> :
<L3>:
  return _10;

}


uxTaskGetSystemState (struct TaskStatus_t * const pxTaskStatusArray, const UBaseType_t uxArraySize, uint32_t * const pulTotalRunTime)
{
  UBaseType_t uxQueue;
  UBaseType_t uxTask;
  UBaseType_t D.7844;
  long unsigned int D.7840;
  long unsigned int D.7839;
  long unsigned int D.7838;
  long unsigned int D.7837;
  long unsigned int D.7836;
  long unsigned int uxCurrentNumberOfTasks.54_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.55_7;
  long unsigned int _8;
  struct TaskStatus_t * _9;
  struct List_t * pxOverflowDelayedTaskList.56_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> :
  uxTask_20 = 0;
  uxQueue_21 = 5;
  vTaskSuspendAll ();
  uxCurrentNumberOfTasks.54_1 ={v} uxCurrentNumberOfTasks;
  if (uxArraySize_24(D) >= uxCurrentNumberOfTasks.54_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)>
  uxQueue_25 = uxQueue_17 + 4294967295;
  _2 = uxTask_15 * 36;
  _3 = pxTaskStatusArray_26(D) + _2;
  _4 = &pxReadyTasksLists[uxQueue_25];
  _28 = prvListTasksWithinSingleList (_3, _4, 1);
  uxTask_29 = _28 + uxTask_15;
  if (uxQueue_25 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

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

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

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

  <bb 7> :
<L7>:
  return _45;

}


xTaskGetHandle (const char * pcNameToQuery)
{
  uint32_t ulNewBASEPRI;
  struct TCB_t * pxTCB;
  UBaseType_t uxQueue;
  struct tskTaskControlBlock * D.7832;
  unsigned int _1;
  struct List_t * _2;
  struct List_t * pxDelayedTaskList.52_3;
  struct List_t * pxOverflowDelayedTaskList.53_4;
  struct tskTaskControlBlock * _31;

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

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

  <bb 4> :

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

  <bb 6> :
  vTaskSuspendAll ();

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

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

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

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

  <bb 11> :
  pxDelayedTaskList.52_3 ={v} pxDelayedTaskList;
  pxTCB_23 = prvSearchForNameWithinSingleList (pxDelayedTaskList.52_3, pcNameToQuery_17(D));

  <bb 12> :
  # pxTCB_6 = PHI <pxTCB_21(10), pxTCB_23(11)>
  if (pxTCB_6 == 0B)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  pxOverflowDelayedTaskList.53_4 ={v} pxOverflowDelayedTaskList;
  pxTCB_25 = prvSearchForNameWithinSingleList (pxOverflowDelayedTaskList.53_4, pcNameToQuery_17(D));

  <bb 14> :
  # pxTCB_7 = PHI <pxTCB_6(12), pxTCB_25(13)>
  if (pxTCB_7 == 0B)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  pxTCB_27 = prvSearchForNameWithinSingleList (&xSuspendedTaskList, pcNameToQuery_17(D));

  <bb 16> :
  # pxTCB_8 = PHI <pxTCB_7(14), pxTCB_27(15)>
  if (pxTCB_8 == 0B)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  pxTCB_29 = prvSearchForNameWithinSingleList (&xTasksWaitingTermination, pcNameToQuery_17(D));

  <bb 18> :
  # pxTCB_9 = PHI <pxTCB_8(16), pxTCB_29(17)>
  xTaskResumeAll ();
  _31 = pxTCB_9;

  <bb 19> :
<L15>:
  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;
  struct TCB_t * D.7818;
  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> :
  pxReturn_30 = 0B;
  _1 ={v} pxList_32(D)->uxNumberOfItems;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 21>; [INV]

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

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

  <bb 5> :
  _8 = pxConstList_33->pxIndex;
  pxFirstTCB_36 = _8->pvOwner;

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

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

  <bb 8> :
  _15 = pxConstList_37->pxIndex;
  pxNextTCB_40 = _15->pvOwner;
  xBreakLoop_41 = 0;
  x_42 = 0;
  goto <bb 16>; [INV]

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

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

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

  <bb 12> :
  pxReturn_45 = pxNextTCB_40;
  xBreakLoop_46 = 1;

  <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)>
  if (xBreakLoop_24 != 0)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

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

  <bb 15> :
  x_48 = x_23 + 1;

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

  <bb 17> :
  # pxReturn_21 = PHI <pxReturn_19(14), pxReturn_20(16)>
  if (pxReturn_21 != 0B)
    goto <bb 18>; [INV]
  else
    goto <bb 19>; [INV]

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

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

  <bb 20> :

  <bb 21> :
  # pxReturn_22 = PHI <pxReturn_30(2), pxReturn_21(20)>
  _49 = pxReturn_22;

  <bb 22> :
<L22>:
  return _49;

}


pcTaskGetName (struct tskTaskControlBlock * xTaskToQuery)
{
  uint32_t ulNewBASEPRI;
  struct TCB_t * pxTCB;
  char * D.7799;
  struct TCB_t * iftmp.51;
  struct TCB_t * iftmp.51_1;
  struct TCB_t * iftmp.51_3;
  struct TCB_t * iftmp.51_5;
  char * _7;

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

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

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

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

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

  <bb 7> :

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

  <bb 9> :
  _7 = &pxTCB_6->pcTaskName[0];

  <bb 10> :
<L6>:
  return _7;

}


uxTaskGetNumberOfTasks ()
{
  UBaseType_t D.7791;
  UBaseType_t _2;

  <bb 2> :
  _2 ={v} uxCurrentNumberOfTasks;

  <bb 3> :
<L0>:
  return _2;

}


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

  <bb 2> :
  vPortValidateInterruptPriority ();
  uxSavedInterruptStatus_3 = 0;
  xReturn_4 ={v} xTickCount;
  _5 = xReturn_4;

  <bb 3> :
<L0>:
  return _5;

}


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

  <bb 2> :
  xTicks_2 ={v} xTickCount;
  _3 = xTicks_2;

  <bb 3> :
<L0>:
  return _3;

}


xTaskResumeAll ()
{
  uint32_t ulNewBASEPRI;
  TickType_t xPendedCounts;
  struct ListItem_t * const pxIndex;
  struct List_t * const pxList;
  struct List_t * const pxList;
  BaseType_t xAlreadyYielded;
  struct TCB_t * pxTCB;
  BaseType_t D.7785;
  long unsigned int uxSchedulerSuspended.44_1;
  long unsigned int uxSchedulerSuspended.45_2;
  long unsigned int _3;
  long unsigned int uxSchedulerSuspended.46_4;
  long unsigned int uxCurrentNumberOfTasks.47_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.48_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.49_39;
  long unsigned int _40;
  long unsigned int _41;
  long int _42;
  long int xYieldPending.50_43;
  volatile uint32_t * _44;
  BaseType_t _96;

  <bb 2> :
  pxTCB_57 = 0B;
  xAlreadyYielded_58 = 0;
  uxSchedulerSuspended.44_1 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.44_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  vPortEnterCritical ();
  uxSchedulerSuspended.45_2 ={v} uxSchedulerSuspended;
  _3 = uxSchedulerSuspended.45_2 + 4294967295;
  uxSchedulerSuspended ={v} _3;
  uxSchedulerSuspended.46_4 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.46_4 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 7> :
  uxCurrentNumberOfTasks.47_5 ={v} uxCurrentNumberOfTasks;
  if (uxCurrentNumberOfTasks.47_5 != 0)
    goto <bb 8>; [INV]
  else
    goto <bb 27>; [INV]

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

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

  <bb 10> :
  _13 = pxTCB_72->xEventListItem.pxPrevious;
  pxList_73->pxIndex = _13;

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

  <bb 12> :
  _22 = pxTCB_72->xStateListItem.pxPrevious;
  pxList_80->pxIndex = _22;

  <bb 13> :
  pxTCB_72->xStateListItem.pvContainer = 0B;
  _23 ={v} pxList_80->uxNumberOfItems;
  _24 = _23 + 4294967295;
  pxList_80->uxNumberOfItems ={v} _24;
  _25 = pxTCB_72->uxPriority;
  uxTopReadyPriority.48_26 ={v} uxTopReadyPriority;
  if (_25 > uxTopReadyPriority.48_26)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  _27 = pxTCB_72->uxPriority;
  uxTopReadyPriority ={v} _27;

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

  <bb 16> :
  xYieldPending ={v} 1;

  <bb 17> :
  # pxTCB_45 = PHI <pxTCB_57(8), pxTCB_72(15), pxTCB_72(16)>
  _41 ={v} xPendingReadyList.uxNumberOfItems;
  if (_41 != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 18>; [INV]

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

  <bb 19> :
  prvResetNextTaskUnblockTime ();

  <bb 20> :
  xPendedCounts_63 ={v} xPendedTicks;
  if (xPendedCounts_63 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 21> :
  # xPendedCounts_47 = PHI <xPendedCounts_63(20), xPendedCounts_66(23)>
  _42 = xTaskIncrementTick ();
  if (_42 != 0)
    goto <bb 22>; [INV]
  else
    goto <bb 23>; [INV]

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

  <bb 23> :
  xPendedCounts_66 = xPendedCounts_47 + 4294967295;
  if (xPendedCounts_66 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 24> :
  xPendedTicks ={v} 0;

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

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

  <bb 27> :
  # xAlreadyYielded_46 = PHI <xAlreadyYielded_58(6), xAlreadyYielded_58(25), xAlreadyYielded_58(7), xAlreadyYielded_68(26)>
  vPortExitCritical ();
  _96 = xAlreadyYielded_46;

  <bb 28> :
<L33>:
  return _96;

}


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

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

}


vTaskEndScheduler ()
{
  uint32_t ulNewBASEPRI;

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

  <bb 3> :
  xSchedulerRunning ={v} 0;
  vPortEndScheduler ();
  return;

}


vTaskStartScheduler ()
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  BaseType_t xReturn;
  long unsigned int vol.42;
  long int _1;
  long unsigned int vol.42_14;

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

  <bb 3> :
  xReturn_9 = xTimerCreateTimerTask ();

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

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

  <bb 6> :
  xNextTaskUnblockTime ={v} 4294967295;
  xSchedulerRunning ={v} 1;
  xTickCount ={v} 0;
  _1 = xPortStartScheduler ();
  goto <bb 11>; [INV]

  <bb 7> :
  if (xReturn_2 == -1)
    goto <bb 8>; [INV]
  else
    goto <bb 11>; [INV]

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

  <bb 9> :

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

  <bb 11> :
  vol.42_14 ={v} uxTopUsedPriority;
  return;

}


xTaskResumeFromISR (struct tskTaskControlBlock * xTaskToResume)
{
  uint32_t ulNewMaskValue;
  uint32_t D.8324;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.8323;
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  UBaseType_t uxSavedInterruptStatus;
  struct TCB_t * const pxTCB;
  BaseType_t xYieldRequired;
  BaseType_t D.7744;
  long int _1;
  long unsigned int uxSchedulerSuspended.39_2;
  long unsigned int _3;
  struct TCB_t * pxCurrentTCB.40_4;
  long unsigned int _5;
  struct ListItem_t * _6;
  long unsigned int _7;
  long unsigned int uxTopReadyPriority.41_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 _45;
  long unsigned int _49;

  <bb 2> :
  xYieldRequired_26 = 0;
  pxTCB_28 = xTaskToResume_27(D);
  if (xTaskToResume_27(D) == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  vPortValidateInterruptPriority ();
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_47, "=r" ulNewBASEPRI_48 : "i" 16 : "memory");
  _49 = ulOriginalBASEPRI_47;

  <bb 7> :
<L15>:
  _52 = _49;

  <bb 8> :
  uxSavedInterruptStatus_31 = _52;
  _1 = prvTaskIsTaskSuspended (pxTCB_28);
  if (_1 != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 9> :
  uxSchedulerSuspended.39_2 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.39_2 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 10> :
  _3 = pxTCB_28->uxPriority;
  pxCurrentTCB.40_4 ={v} pxCurrentTCB;
  _5 = pxCurrentTCB.40_4->uxPriority;
  if (_3 >= _5)
    goto <bb 11>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 11> :
  xYieldRequired_34 = 1;
  xYieldPending ={v} 1;

  <bb 12> :
  # xYieldRequired_21 = PHI <xYieldRequired_26(10), xYieldRequired_34(11)>
  _6 = &pxTCB_28->xStateListItem;
  uxListRemove (_6);
  _7 = pxTCB_28->uxPriority;
  uxTopReadyPriority.41_8 ={v} uxTopReadyPriority;
  if (_7 > uxTopReadyPriority.41_8)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  _9 = pxTCB_28->uxPriority;
  uxTopReadyPriority ={v} _9;

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

  <bb 15> :
  _20 = &pxTCB_28->xEventListItem;
  vListInsertEnd (&xPendingReadyList, _20);

  <bb 16> :
  # xYieldRequired_22 = PHI <xYieldRequired_26(8), xYieldRequired_26(15), xYieldRequired_21(14)>
  ulNewMaskValue_50 = uxSavedInterruptStatus_31;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_50 : "memory");

  <bb 17> :
  _45 = xYieldRequired_22;

  <bb 18> :
<L14>:
  return _45;

}


vTaskResume (struct tskTaskControlBlock * xTaskToResume)
{
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  struct TCB_t * const pxTCB;
  struct TCB_t * pxCurrentTCB.36_1;
  long int _2;
  struct ListItem_t * _3;
  long unsigned int _4;
  long unsigned int uxTopReadyPriority.37_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.38_18;
  long unsigned int _19;
  volatile uint32_t * _20;

  <bb 2> :
  pxTCB_25 = xTaskToResume_24(D);
  if (xTaskToResume_24(D) == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  pxCurrentTCB.36_1 ={v} pxCurrentTCB;
  if (pxTCB_25 != pxCurrentTCB.36_1)
    goto <bb 7>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 8> :
  vPortEnterCritical ();
  _2 = prvTaskIsTaskSuspended (pxTCB_25);
  if (_2 != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 13>; [INV]

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

  <bb 10> :
  _6 = pxTCB_25->uxPriority;
  uxTopReadyPriority ={v} _6;

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

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

  <bb 13> :
  vPortExitCritical ();

  <bb 14> :
  return;

}


prvTaskIsTaskSuspended (struct tskTaskControlBlock * const xTask)
{
  uint32_t ulNewBASEPRI;
  const struct TCB_t * const pxTCB;
  BaseType_t xReturn;
  BaseType_t D.7714;
  struct xLIST * _1;
  struct xLIST * _2;
  struct xLIST * _3;
  BaseType_t _10;

  <bb 2> :
  xReturn_5 = 0;
  pxTCB_7 = xTask_6(D);
  if (xTask_6(D) == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  _1 = pxTCB_7->xStateListItem.pvContainer;
  if (_1 == &xSuspendedTaskList)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 7> :
  _2 = pxTCB_7->xEventListItem.pvContainer;
  if (_2 != &xPendingReadyList)
    goto <bb 8>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 9> :
  xReturn_9 = 1;

  <bb 10> :
  # xReturn_4 = PHI <xReturn_5(6), xReturn_9(9), xReturn_5(7), xReturn_5(8)>
  _10 = xReturn_4;

  <bb 11> :
<L12>:
  return _10;

}


vTaskSuspend (struct tskTaskControlBlock * xTaskToSuspend)
{
  uint32_t ulNewBASEPRI;
  BaseType_t x;
  struct TCB_t * pxTCB;
  struct TCB_t * iftmp.30;
  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.31_7;
  struct TCB_t * pxCurrentTCB.32_8;
  long int xSchedulerRunning.33_9;
  long unsigned int uxSchedulerSuspended.34_10;
  volatile uint32_t * _11;
  long unsigned int _12;
  long unsigned int uxCurrentNumberOfTasks.35_13;
  struct TCB_t * iftmp.30_15;
  struct TCB_t * iftmp.30_24;
  struct TCB_t * iftmp.30_25;

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

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

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

  <bb 5> :
  # iftmp.30_15 = PHI <iftmp.30_25(3), iftmp.30_24(4)>
  pxTCB_26 = iftmp.30_15;
  _1 = &pxTCB_26->xStateListItem;
  _2 = uxListRemove (_1);

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

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

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

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

  <bb 10> :
  pxTCB_26->ucNotifyState[x_14] ={v} 0;

  <bb 11> :
  x_41 = x_14 + 1;

  <bb 12> :
  # x_14 = PHI <x_30(8), x_41(11)>
  if (x_14 <= 0)
    goto <bb 9>; [INV]
  else
    goto <bb 13>; [INV]

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

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

  <bb 15> :
  pxCurrentTCB.32_8 ={v} pxCurrentTCB;
  if (pxTCB_26 == pxCurrentTCB.32_8)
    goto <bb 16>; [INV]
  else
    goto <bb 25>; [INV]

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

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

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

  <bb 19> :

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

  <bb 21> :
  _11 = 3758157060B;
  *_11 ={v} 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 25>; [INV]

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

  <bb 23> :
  pxCurrentTCB ={v} 0B;
  goto <bb 25>; [INV]

  <bb 24> :
  vTaskSwitchContext ();

  <bb 25> :
  return;

}


vTaskPrioritySet (struct tskTaskControlBlock * xTask, UBaseType_t uxNewPriority)
{
  uint32_t ulNewBASEPRI;
  struct ListItem_t * const pxIndex;
  BaseType_t xYieldRequired;
  UBaseType_t uxPriorityUsedOnEntry;
  UBaseType_t uxCurrentBasePriority;
  struct TCB_t * pxTCB;
  struct TCB_t * iftmp.25;
  struct TCB_t * pxCurrentTCB.26_1;
  struct TCB_t * pxCurrentTCB.27_2;
  long unsigned int _3;
  struct TCB_t * pxCurrentTCB.28_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.29_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.25_30;
  struct TCB_t * iftmp.25_42;
  struct TCB_t * iftmp.25_43;

  <bb 2> :
  xYieldRequired_36 = 0;
  if (uxNewPriority_37(D) > 4)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  if (uxNewPriority_37(D) > 4)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  uxNewPriority_38 = 4;

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

  <bb 9> :
  iftmp.25_43 ={v} pxCurrentTCB;
  goto <bb 11>; [INV]

  <bb 10> :
  iftmp.25_42 = xTask_41(D);

  <bb 11> :
  # iftmp.25_30 = PHI <iftmp.25_43(9), iftmp.25_42(10)>
  pxTCB_44 = iftmp.25_30;
  uxCurrentBasePriority_45 = pxTCB_44->uxBasePriority;
  if (uxCurrentBasePriority_45 != uxNewPriority_28)
    goto <bb 12>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 12> :
  if (uxNewPriority_28 > uxCurrentBasePriority_45)
    goto <bb 13>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 13> :
  pxCurrentTCB.26_1 ={v} pxCurrentTCB;
  if (pxTCB_44 != pxCurrentTCB.26_1)
    goto <bb 14>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 14> :
  pxCurrentTCB.27_2 ={v} pxCurrentTCB;
  _3 = pxCurrentTCB.27_2->uxPriority;
  if (uxNewPriority_28 >= _3)
    goto <bb 15>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 15> :
  xYieldRequired_47 = 1;
  goto <bb 18>; [INV]

  <bb 16> :
  pxCurrentTCB.28_4 ={v} pxCurrentTCB;
  if (pxTCB_44 == pxCurrentTCB.28_4)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  xYieldRequired_46 = 1;

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

  <bb 19> :
  pxTCB_44->uxPriority = uxNewPriority_28;

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

  <bb 21> :
  _9 = 5 - uxNewPriority_28;
  pxTCB_44->xEventListItem.xItemValue = _9;

  <bb 22> :
  _10 = pxTCB_44->xStateListItem.pvContainer;
  _11 = &pxReadyTasksLists[uxPriorityUsedOnEntry_48];
  if (_10 == _11)
    goto <bb 23>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 23> :
  _12 = &pxTCB_44->xStateListItem;
  _13 = uxListRemove (_12);

  <bb 24> :
  _14 = pxTCB_44->uxPriority;
  uxTopReadyPriority.29_15 ={v} uxTopReadyPriority;
  if (_14 > uxTopReadyPriority.29_15)
    goto <bb 25>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 25> :
  _16 = pxTCB_44->uxPriority;
  uxTopReadyPriority ={v} _16;

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

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

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

  <bb 29> :
  vPortExitCritical ();
  return;

}


uxTaskPriorityGetFromISR (struct tskTaskControlBlock * const xTask)
{
  uint32_t ulNewMaskValue;
  uint32_t D.8314;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.8313;
  UBaseType_t uxSavedInterruptState;
  UBaseType_t uxReturn;
  const struct TCB_t * pxTCB;
  UBaseType_t D.7633;
  const struct TCB_t * iftmp.24;
  const struct TCB_t * iftmp.24_1;
  const struct TCB_t * iftmp.24_6;
  const struct TCB_t * iftmp.24_7;
  UBaseType_t _10;
  long unsigned int _13;

  <bb 2> :
  vPortValidateInterruptPriority ();
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_11, "=r" ulNewBASEPRI_12 : "i" 16 : "memory");
  _13 = ulOriginalBASEPRI_11;

  <bb 3> :
<L4>:
  _16 = _13;

  <bb 4> :
  uxSavedInterruptState_4 = _16;
  if (xTask_5(D) == 0B)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  iftmp.24_7 ={v} pxCurrentTCB;
  goto <bb 7>; [INV]

  <bb 6> :
  iftmp.24_6 = xTask_5(D);

  <bb 7> :
  # iftmp.24_1 = PHI <iftmp.24_7(5), iftmp.24_6(6)>
  pxTCB_8 = iftmp.24_1;
  uxReturn_9 = pxTCB_8->uxPriority;
  ulNewMaskValue_14 = uxSavedInterruptState_4;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_14 : "memory");

  <bb 8> :
  _10 = uxReturn_9;

  <bb 9> :
<L3>:
  return _10;

}


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

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

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

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

  <bb 5> :
  # iftmp.23_1 = PHI <iftmp.23_6(3), iftmp.23_5(4)>
  pxTCB_7 = iftmp.23_1;
  uxReturn_8 = pxTCB_7->uxPriority;
  vPortExitCritical ();
  _10 = uxReturn_8;

  <bb 6> :
<L3>:
  return _10;

}


eTaskGetState (struct tskTaskControlBlock * xTask)
{
  uint32_t ulNewBASEPRI;
  BaseType_t x;
  const struct TCB_t * const pxTCB;
  const struct List_t * pxOverflowedDelayedList;
  const struct List_t * pxDelayedList;
  const struct List_t * pxStateList;
  eTaskState eReturn;
  eTaskState D.7621;
  struct TCB_t * pxCurrentTCB.22_1;
  struct xLIST * _2;
  unsigned char _3;
  eTaskState _25;

  <bb 2> :
  pxTCB_9 = xTask_8(D);
  if (pxTCB_9 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  pxCurrentTCB.22_1 ={v} pxCurrentTCB;
  if (pxTCB_9 == pxCurrentTCB.22_1)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  eReturn_24 = 0;
  goto <bb 24>; [INV]

  <bb 8> :
  vPortEnterCritical ();
  pxStateList_12 = pxTCB_9->xStateListItem.pvContainer;
  pxDelayedList_13 ={v} pxDelayedTaskList;
  pxOverflowedDelayedList_14 ={v} pxOverflowDelayedTaskList;
  vPortExitCritical ();
  if (pxStateList_12 == pxDelayedList_13)
    goto <bb 10>; [INV]
  else
    goto <bb 9>; [INV]

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

  <bb 10> :
  eReturn_23 = 2;
  goto <bb 24>; [INV]

  <bb 11> :
  if (pxStateList_12 == &xSuspendedTaskList)
    goto <bb 12>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 12> :
  _2 = pxTCB_9->xEventListItem.pvContainer;
  if (_2 == 0B)
    goto <bb 13>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 13> :
  eReturn_19 = 3;
  x_20 = 0;
  goto <bb 17>; [INV]

  <bb 14> :
  _3 ={v} pxTCB_9->ucNotifyState[x_6];
  if (_3 == 1)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  eReturn_22 = 2;
  goto <bb 18>; [INV]

  <bb 16> :
  x_21 = x_6 + 1;

  <bb 17> :
  # x_6 = PHI <x_20(13), x_21(16)>
  if (x_6 <= 0)
    goto <bb 14>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 18> :
  # eReturn_4 = PHI <eReturn_22(15), eReturn_19(17)>
  goto <bb 24>; [INV]

  <bb 19> :
  eReturn_18 = 2;
  goto <bb 24>; [INV]

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

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

  <bb 22> :
  eReturn_17 = 4;
  goto <bb 24>; [INV]

  <bb 23> :
  eReturn_16 = 1;

  <bb 24> :
  # eReturn_5 = PHI <eReturn_24(7), eReturn_23(10), eReturn_18(19), eReturn_17(22), eReturn_16(23), eReturn_4(18)>
  _25 = eReturn_5;

  <bb 25> :
<L25>:
  return _25;

}


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

  <bb 2> :
  xAlreadyYielded_6 = 0;
  if (xTicksToDelay_7(D) != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 8>; [INV]

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

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

  <bb 5> :

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

  <bb 7> :
  vTaskSuspendAll ();
  prvAddCurrentTaskToDelayedList (xTicksToDelay_7(D), 0);
  xAlreadyYielded_12 = xTaskResumeAll ();

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

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

  <bb 10> :
  return;

}


xTaskDelayUntil (TickType_t * const pxPreviousWakeTime, const TickType_t xTimeIncrement)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  const TickType_t xConstTickCount;
  BaseType_t xShouldDelay;
  BaseType_t xAlreadyYielded;
  TickType_t xTimeToWake;
  BaseType_t D.7590;
  long unsigned int uxSchedulerSuspended.20_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> :
  xShouldDelay_11 = 0;
  if (pxPreviousWakeTime_12(D) == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  if (xTimeIncrement_13(D) == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 8> :

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

  <bb 10> :
  uxSchedulerSuspended.20_1 ={v} uxSchedulerSuspended;
  if (uxSchedulerSuspended.20_1 != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 12> :

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

  <bb 14> :
  vTaskSuspendAll ();
  xConstTickCount_16 ={v} xTickCount;
  _2 = *pxPreviousWakeTime_12(D);
  xTimeToWake_17 = xTimeIncrement_13(D) + _2;
  _3 = *pxPreviousWakeTime_12(D);
  if (xConstTickCount_16 < _3)
    goto <bb 15>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 15> :
  _4 = *pxPreviousWakeTime_12(D);
  if (xTimeToWake_17 < _4)
    goto <bb 16>; [INV]
  else
    goto <bb 21>; [INV]

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

  <bb 17> :
  xShouldDelay_19 = 1;
  goto <bb 21>; [INV]

  <bb 18> :
  _5 = *pxPreviousWakeTime_12(D);
  if (xTimeToWake_17 < _5)
    goto <bb 20>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 19> :
  if (xTimeToWake_17 > xConstTickCount_16)
    goto <bb 20>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 20> :
  xShouldDelay_18 = 1;

  <bb 21> :
  # xShouldDelay_8 = PHI <xShouldDelay_11(16), xShouldDelay_11(19), xShouldDelay_18(20), xShouldDelay_11(15), xShouldDelay_19(17)>
  *pxPreviousWakeTime_12(D) = xTimeToWake_17;
  if (xShouldDelay_8 != 0)
    goto <bb 22>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 22> :
  _6 = xTimeToWake_17 - xConstTickCount_16;
  prvAddCurrentTaskToDelayedList (_6, 0);

  <bb 23> :
  xAlreadyYielded_23 = xTaskResumeAll ();
  if (xAlreadyYielded_23 == 0)
    goto <bb 24>; [INV]
  else
    goto <bb 25>; [INV]

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

  <bb 25> :
  _27 = xShouldDelay_8;

  <bb 26> :
<L26>:
  return _27;

}


vTaskDelete (struct tskTaskControlBlock * xTaskToDelete)
{
  uint32_t ulNewBASEPRI;
  struct TCB_t * pxTCB;
  struct TCB_t * iftmp.12;
  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> :
  vPortEnterCritical ();
  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;
  _1 = &pxTCB_26->xStateListItem;
  _2 = uxListRemove (_1);

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

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

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

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

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

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

  <bb 12> :
  pxCurrentTCB.18_14 ={v} pxCurrentTCB;
  if (pxTCB_26 == pxCurrentTCB.18_14)
    goto <bb 13>; [INV]
  else
    goto <bb 18>; [INV]

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

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

  <bb 15> :

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

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

  <bb 18> :
  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> :
  vPortEnterCritical ();
  uxCurrentNumberOfTasks.2_1 ={v} uxCurrentNumberOfTasks;
  _2 = uxCurrentNumberOfTasks.2_1 + 1;
  uxCurrentNumberOfTasks ={v} _2;
  pxCurrentTCB.3_3 ={v} pxCurrentTCB;
  if (pxCurrentTCB.3_3 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

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

  <bb 6> :
  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> :
  pxCurrentTCB ={v} pxNewTCB_36(D);

  <bb 8> :
  uxTaskNumber.7_9 = uxTaskNumber;
  _10 = uxTaskNumber.7_9 + 1;
  uxTaskNumber = _10;
  uxTaskNumber.8_11 = uxTaskNumber;
  pxNewTCB_36(D)->uxTCBNumber = uxTaskNumber.8_11;
  _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> :
  _14 = pxNewTCB_36(D)->uxPriority;
  uxTopReadyPriority ={v} _14;

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

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

  <bb 13> :
  return;

}


prvInitialiseNewTask (void (*TaskFunction_t) (void *) pxTaskCode, const char * const pcName, const uint32_t ulStackDepth, void * const pvParameters, UBaseType_t uxPriority, struct tskTaskControlBlock * * const pxCreatedTask, struct TCB_t * pxNewTCB, const struct MemoryRegion_t * const xRegions)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  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> :
  _1 = pxNewTCB_27(D)->pxStack;
  _2 = ulStackDepth_28(D) * 4;
  memset (_1, 165, _2);
  _3 = pxNewTCB_27(D)->pxStack;
  _4 = ulStackDepth_28(D) + 1073741823;
  _5 = _4 * 4;
  pxTopOfStack_30 = _3 + _5;
  pxTopOfStack.0_6 = (long unsigned int) pxTopOfStack_30;
  _7 = pxTopOfStack.0_6 & 4294967288;
  pxTopOfStack_31 = (StackType_t *) _7;
  pxTopOfStack.1_8 = (long unsigned int) pxTopOfStack_31;
  _9 = pxTopOfStack.1_8 & 7;
  if (_9 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  pxNewTCB_27(D)->pxEndOfStack = pxTopOfStack_31;
  if (pcName_33(D) != 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 7> :
  x_35 = 0;
  goto <bb 11>; [INV]

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

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

  <bb 10> :
  x_37 = x_21 + 1;

  <bb 11> :
  # x_21 = PHI <x_35(7), x_37(10)>
  if (x_21 <= 9)
    goto <bb 8>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 12> :
  pxNewTCB_27(D)->pcTaskName[9] = 0;
  goto <bb 14>; [INV]

  <bb 13> :
  pxNewTCB_27(D)->pcTaskName[0] = 0;

  <bb 14> :
  if (uxPriority_39(D) > 4)
    goto <bb 15>; [INV]
  else
    goto <bb 18>; [INV]

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

  <bb 16> :

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

  <bb 18> :
  if (uxPriority_39(D) > 4)
    goto <bb 19>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 19> :
  uxPriority_40 = 4;

  <bb 20> :
  # uxPriority_20 = PHI <uxPriority_39(D)(18), uxPriority_40(19)>
  pxNewTCB_27(D)->uxPriority = uxPriority_20;
  pxNewTCB_27(D)->uxBasePriority = uxPriority_20;
  pxNewTCB_27(D)->uxMutexesHeld = 0;
  _14 = &pxNewTCB_27(D)->xStateListItem;
  vListInitialiseItem (_14);
  _15 = &pxNewTCB_27(D)->xEventListItem;
  vListInitialiseItem (_15);
  pxNewTCB_27(D)->xStateListItem.pvOwner = pxNewTCB_27(D);
  _16 = 5 - uxPriority_20;
  pxNewTCB_27(D)->xEventListItem.xItemValue = _16;
  pxNewTCB_27(D)->xEventListItem.pvOwner = pxNewTCB_27(D);
  _17 = &pxNewTCB_27(D)->ulNotifiedValue[0];
  memset (_17, 0, 4);
  _18 = &pxNewTCB_27(D)->ucNotifyState[0];
  memset (_18, 0, 1);
  pxNewTCB_27(D)->ucDelayAborted = 0;
  _19 = pxPortInitialiseStack (pxTopOfStack_31, pxTaskCode_52(D), pvParameters_53(D));
  pxNewTCB_27(D)->pxTopOfStack = _19;
  if (pxCreatedTask_56(D) != 0B)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  *pxCreatedTask_56(D) = pxNewTCB_27(D);

  <bb 22> :
  return;

}


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

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

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

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

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

  <bb 6> :
  pxNewTCB_12 = 0B;

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

  <bb 8> :
  _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);
  prvAddNewTaskToReadyList (pxNewTCB_4);
  xReturn_25 = 1;
  goto <bb 10>; [INV]

  <bb 9> :
  xReturn_17 = -1;

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

  <bb 11> :
<L9>:
  return _26;

}