vTimerSetTimerNumber (struct tmrTimerControl * xTimer, UBaseType_t uxTimerNumber)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  MEM[(struct Timer_t *)xTimer_2(D)].uxTimerNumber = uxTimerNumber_3(D);
  return;

}


uxTimerGetTimerNumber (struct tmrTimerControl * xTimer)
{
  UBaseType_t _3;

  <bb 2> :
  # DEBUG BEGIN_STMT
  _3 = MEM[(struct Timer_t *)xTimer_2(D)].uxTimerNumber;
  return _3;

}


xTimerPendFunctionCall (void (*PendedFunction_t) (void *, uint32_t) xFunctionToPend, void * pvParameter1, uint32_t ulParameter2, TickType_t xTicksToWait)
{
  BaseType_t xReturn;
  struct DaemonTaskMessage_t xMessage;
  struct QueueDefinition * xTimerQueue.26_1;
  struct QueueDefinition * xTimerQueue.27_2;
  BaseType_t _14;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xTimerQueue.26_1 = xTimerQueue;
  if (xTimerQueue.26_1 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xMessage.xMessageID = -1;
  # DEBUG BEGIN_STMT
  xMessage.u.xCallbackParameters.pxCallbackFunction = xFunctionToPend_5(D);
  # DEBUG BEGIN_STMT
  xMessage.u.xCallbackParameters.pvParameter1 = pvParameter1_7(D);
  # DEBUG BEGIN_STMT
  xMessage.u.xCallbackParameters.ulParameter2 = ulParameter2_9(D);
  # DEBUG BEGIN_STMT
  xTimerQueue.27_2 = xTimerQueue;
  xReturn_13 = xQueueGenericSend (xTimerQueue.27_2, &xMessage, xTicksToWait_11(D), 0);
  # DEBUG xReturn => xReturn_13
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _14 = xReturn_13;
  xMessage ={v} {CLOBBER};
  return _14;

}


xTimerPendFunctionCallFromISR (void (*PendedFunction_t) (void *, uint32_t) xFunctionToPend, void * pvParameter1, uint32_t ulParameter2, BaseType_t * pxHigherPriorityTaskWoken)
{
  BaseType_t xReturn;
  struct DaemonTaskMessage_t xMessage;
  struct QueueDefinition * xTimerQueue.25_1;
  BaseType_t _13;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xMessage.xMessageID = -2;
  # DEBUG BEGIN_STMT
  xMessage.u.xCallbackParameters.pxCallbackFunction = xFunctionToPend_4(D);
  # DEBUG BEGIN_STMT
  xMessage.u.xCallbackParameters.pvParameter1 = pvParameter1_6(D);
  # DEBUG BEGIN_STMT
  xMessage.u.xCallbackParameters.ulParameter2 = ulParameter2_8(D);
  # DEBUG BEGIN_STMT
  xTimerQueue.25_1 = xTimerQueue;
  xReturn_12 = xQueueGenericSendFromISR (xTimerQueue.25_1, &xMessage, pxHigherPriorityTaskWoken_10(D), 0);
  # DEBUG xReturn => xReturn_12
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _13 = xReturn_12;
  xMessage ={v} {CLOBBER};
  return _13;

}


vTimerSetTimerID (struct tmrTimerControl * xTimer, void * pvNewID)
{
  struct Timer_t * const pxTimer;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  pxTimer_2->pvTimerID = pvNewID_5(D);
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  return;

}


pvTimerGetTimerID (struct tmrTimerControl * const xTimer)
{
  void * pvReturn;
  struct Timer_t * const pxTimer;
  void * _7;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  pvReturn_5 = pxTimer_2->pvTimerID;
  # DEBUG pvReturn => pvReturn_5
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _7 = pvReturn_5;
  return _7;

}


xTimerIsTimerActive (struct tmrTimerControl * xTimer)
{
  struct Timer_t * pxTimer;
  BaseType_t xReturn;
  unsigned char _1;
  int _2;
  int _3;
  BaseType_t _12;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _1 = pxTimer_6->ucStatus;
  _2 = (int) _1;
  _3 = _2 & 1;
  if (_3 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  xReturn_10 = 0;
  # DEBUG xReturn => xReturn_10
  goto <bb 8>; [INV]

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

  <bb 8> :
  # xReturn_4 = PHI <xReturn_10(6), xReturn_9(7)>
  # DEBUG xReturn => xReturn_4
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _12 = xReturn_4;
  return _12;

}


prvCheckForValidListAndQueue ()
{
  struct QueueDefinition * xTimerQueue.17_1;
  struct QueueDefinition * _2;
  struct QueueDefinition * xTimerQueue.18_3;
  struct QueueDefinition * xTimerQueue.19_4;

  <bb 2> :
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  xTimerQueue.17_1 = xTimerQueue;
  if (xTimerQueue.17_1 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  vListInitialise (&xActiveTimerList1);
  # DEBUG BEGIN_STMT
  vListInitialise (&xActiveTimerList2);
  # DEBUG BEGIN_STMT
  pxCurrentTimerList = &xActiveTimerList1;
  # DEBUG BEGIN_STMT
  pxOverflowTimerList = &xActiveTimerList2;
  # DEBUG BEGIN_STMT
  _2 = xQueueGenericCreate (10, 16, 0);
  xTimerQueue = _2;
  # DEBUG BEGIN_STMT
  xTimerQueue.18_3 = xTimerQueue;
  if (xTimerQueue.18_3 != 0B)
    goto <bb 4>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  xTimerQueue.19_4 = xTimerQueue;
  vQueueAddToRegistry (xTimerQueue.19_4, "TmrQ");

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

}


prvSwitchTimerLists ()
{
  struct List_t * pxTemp;
  TickType_t xNextExpireTime;
  struct List_t * pxCurrentTimerList.10_1;
  struct xLIST_ITEM * _2;
  struct List_t * pxCurrentTimerList.11_3;
  long unsigned int _4;
  struct List_t * pxOverflowTimerList.12_5;

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

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxCurrentTimerList.10_1 = pxCurrentTimerList;
  _2 = pxCurrentTimerList.10_1->xListEnd.pxNext;
  xNextExpireTime_11 = _2->xItemValue;
  # DEBUG xNextExpireTime => xNextExpireTime_11
  # DEBUG BEGIN_STMT
  prvProcessExpiredTimer (xNextExpireTime_11, 4294967295);

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  pxTemp_8 = pxCurrentTimerList;
  # DEBUG pxTemp => pxTemp_8
  # DEBUG BEGIN_STMT
  pxOverflowTimerList.12_5 = pxOverflowTimerList;
  pxCurrentTimerList = pxOverflowTimerList.12_5;
  # DEBUG BEGIN_STMT
  pxOverflowTimerList = pxTemp_8;
  return;

}


prvProcessReceivedCommands ()
{
  const struct CallbackParameters_t * const pxCallback;
  TickType_t xTimeNow;
  BaseType_t xTimerListsWereSwitched;
  struct Timer_t * pxTimer;
  struct DaemonTaskMessage_t xMessage;
  long int _1;
  void (*<T68e>) (void *, uint32_t) _2;
  void * _3;
  long unsigned int _4;
  long int _5;
  struct xLIST * _6;
  struct ListItem_t * _7;
  long int _8;
  unsigned char _9;
  unsigned char _10;
  long unsigned int _11;
  long unsigned int _12;
  long unsigned int _13;
  long unsigned int _14;
  long int _15;
  unsigned char _16;
  int _17;
  int _18;
  long unsigned int _19;
  long unsigned int _20;
  long unsigned int _21;
  unsigned char _22;
  unsigned char _23;
  void (*<T689>) (struct tmrTimerControl *) _24;
  unsigned char _25;
  unsigned char _26;
  unsigned char _27;
  unsigned char _28;
  long unsigned int _29;
  long unsigned int _30;
  long unsigned int _31;
  long unsigned int _32;
  unsigned char _33;
  int _34;
  int _35;
  unsigned char _36;
  unsigned char _37;
  struct QueueDefinition * xTimerQueue.16_38;
  long int _39;

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

  <bb 3> :
  # DEBUG BEGIN_STMT
  _1 = xMessage.xMessageID;
  if (_1 < 0)
    goto <bb 4>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  pxCallback_48 = &xMessage.u.xCallbackParameters;
  # DEBUG pxCallback => pxCallback_48
  # DEBUG BEGIN_STMT
  if (pxCallback_48 == 0B)
    goto <bb 5>; [INV]
  else
    goto <bb 7>; [INV]

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

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _2 = pxCallback_48->pxCallbackFunction;
  _3 = pxCallback_48->pvParameter1;
  _4 = pxCallback_48->ulParameter2;
  _2 (_3, _4);

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _5 = xMessage.xMessageID;
  if (_5 >= 0)
    goto <bb 9>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxTimer_51 = xMessage.u.xTimerParameters.pxTimer;
  # DEBUG pxTimer => pxTimer_51
  # DEBUG BEGIN_STMT
  _6 = pxTimer_51->xTimerListItem.pvContainer;
  if (_6 != 0B)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  _7 = &pxTimer_51->xTimerListItem;
  uxListRemove (_7);

  <bb 11> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xTimeNow_54 = prvSampleTimeNow (&xTimerListsWereSwitched);
  # DEBUG xTimeNow => xTimeNow_54
  # DEBUG BEGIN_STMT
  _8 = xMessage.xMessageID;
  switch (_8) <default: <L37> [INV], case 1 ... 2: <L11> [INV], case 3: <L21> [INV], case 4: <L23> [INV], case 5: <L28> [INV], case 6 ... 7: <L11> [INV], case 8: <L21> [INV], case 9: <L23> [INV]>

  <bb 12> :
<L11>:
  # DEBUG BEGIN_STMT
  _9 = pxTimer_51->ucStatus;
  _10 = _9 | 1;
  pxTimer_51->ucStatus = _10;
  # DEBUG BEGIN_STMT
  _11 = xMessage.u.xTimerParameters.xMessageValue;
  _12 = pxTimer_51->xTimerPeriodInTicks;
  _13 = _11 + _12;
  _14 = xMessage.u.xTimerParameters.xMessageValue;
  _15 = prvInsertTimerInActiveList (pxTimer_51, _13, xTimeNow_54, _14);
  if (_15 != 0)
    goto <bb 13>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  _16 = pxTimer_51->ucStatus;
  _17 = (int) _16;
  _18 = _17 & 4;
  if (_18 != 0)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  _19 = xMessage.u.xTimerParameters.xMessageValue;
  _20 = pxTimer_51->xTimerPeriodInTicks;
  _21 = _19 + _20;
  prvReloadTimer (pxTimer_51, _21, xTimeNow_54);
  goto <bb 16>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  _22 = pxTimer_51->ucStatus;
  _23 = _22 & 254;
  pxTimer_51->ucStatus = _23;

  <bb 16> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _24 = pxTimer_51->pxCallbackFunction;
  _24 (pxTimer_51);
  goto <bb 25>; [INV]

  <bb 17> :
<L21>:
  # DEBUG BEGIN_STMT
  _25 = pxTimer_51->ucStatus;
  _26 = _25 & 254;
  pxTimer_51->ucStatus = _26;
  # DEBUG BEGIN_STMT
  goto <bb 25>; [INV]

  <bb 18> :
<L23>:
  # DEBUG BEGIN_STMT
  _27 = pxTimer_51->ucStatus;
  _28 = _27 | 1;
  pxTimer_51->ucStatus = _28;
  # DEBUG BEGIN_STMT
  _29 = xMessage.u.xTimerParameters.xMessageValue;
  pxTimer_51->xTimerPeriodInTicks = _29;
  # DEBUG BEGIN_STMT
  _30 = pxTimer_51->xTimerPeriodInTicks;
  if (_30 == 0)
    goto <bb 19>; [INV]
  else
    goto <bb 21>; [INV]

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

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

  <bb 21> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _31 = pxTimer_51->xTimerPeriodInTicks;
  _32 = xTimeNow_54 + _31;
  prvInsertTimerInActiveList (pxTimer_51, _32, xTimeNow_54, xTimeNow_54);
  # DEBUG BEGIN_STMT
  goto <bb 25>; [INV]

  <bb 22> :
<L28>:
  # DEBUG BEGIN_STMT
  _33 = pxTimer_51->ucStatus;
  _34 = (int) _33;
  _35 = _34 & 2;
  if (_35 == 0)
    goto <bb 23>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 23> :
  # DEBUG BEGIN_STMT
  vPortFree (pxTimer_51);
  goto <bb 25>; [INV]

  <bb 24> :
  # DEBUG BEGIN_STMT
  _36 = pxTimer_51->ucStatus;
  _37 = _36 & 254;
  pxTimer_51->ucStatus = _37;

  <bb 25> :
<L37>:
  # DEBUG BEGIN_STMT
  xTimerQueue.16_38 = xTimerQueue;
  _39 = xQueueReceive (xTimerQueue.16_38, &xMessage, 0);
  if (_39 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 26> :
  xMessage ={v} {CLOBBER};
  xTimerListsWereSwitched ={v} {CLOBBER};
  return;

}


prvInsertTimerInActiveList (struct Timer_t * const pxTimer, const TickType_t xNextExpiryTime, const TickType_t xTimeNow, const TickType_t xCommandTime)
{
  BaseType_t xProcessTimerNow;
  long unsigned int _1;
  long unsigned int _2;
  struct List_t * pxOverflowTimerList.14_3;
  struct ListItem_t * _4;
  struct List_t * pxCurrentTimerList.15_5;
  struct ListItem_t * _6;
  BaseType_t _21;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xProcessTimerNow_9 = 0;
  # DEBUG xProcessTimerNow => xProcessTimerNow_9
  # DEBUG BEGIN_STMT
  pxTimer_11(D)->xTimerListItem.xItemValue = xNextExpiryTime_12(D);
  # DEBUG BEGIN_STMT
  pxTimer_11(D)->xTimerListItem.pvOwner = pxTimer_11(D);
  # DEBUG BEGIN_STMT
  if (xNextExpiryTime_12(D) <= xTimeNow_15(D))
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  _1 = xTimeNow_15(D) - xCommandTime_16(D);
  _2 = pxTimer_11(D)->xTimerPeriodInTicks;
  if (_1 >= _2)
    goto <bb 4>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  xProcessTimerNow_20 = 1;
  # DEBUG xProcessTimerNow => xProcessTimerNow_20
  goto <bb 10>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  pxOverflowTimerList.14_3 = pxOverflowTimerList;
  _4 = &pxTimer_11(D)->xTimerListItem;
  vListInsert (pxOverflowTimerList.14_3, _4);
  goto <bb 10>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  if (xTimeNow_15(D) < xCommandTime_16(D))
    goto <bb 7>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 7> :
  if (xNextExpiryTime_12(D) >= xCommandTime_16(D))
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  xProcessTimerNow_17 = 1;
  # DEBUG xProcessTimerNow => xProcessTimerNow_17
  goto <bb 10>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  pxCurrentTimerList.15_5 = pxCurrentTimerList;
  _6 = &pxTimer_11(D)->xTimerListItem;
  vListInsert (pxCurrentTimerList.15_5, _6);

  <bb 10> :
  # xProcessTimerNow_7 = PHI <xProcessTimerNow_9(5), xProcessTimerNow_17(8), xProcessTimerNow_9(9), xProcessTimerNow_20(4)>
  # DEBUG xProcessTimerNow => xProcessTimerNow_7
  # DEBUG BEGIN_STMT
  _21 = xProcessTimerNow_7;
  return _21;

}


prvSampleTimeNow (BaseType_t * const pxTimerListsWereSwitched)
{
  static TickType_t xLastTime = 0;
  TickType_t xTimeNow;
  long unsigned int xLastTime.9_1;
  TickType_t _11;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xTimeNow_5 = xTaskGetTickCount ();
  # DEBUG xTimeNow => xTimeNow_5
  # DEBUG BEGIN_STMT
  xLastTime.9_1 = xLastTime;
  if (xTimeNow_5 < xLastTime.9_1)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  prvSwitchTimerLists ();
  # DEBUG BEGIN_STMT
  *pxTimerListsWereSwitched_6(D) = 1;
  goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  *pxTimerListsWereSwitched_6(D) = 0;

  <bb 5> :
  # DEBUG BEGIN_STMT
  xLastTime = xTimeNow_5;
  # DEBUG BEGIN_STMT
  _11 = xTimeNow_5;
  return _11;

}


prvGetNextExpireTime (BaseType_t * const pxListWasEmpty)
{
  TickType_t xNextExpireTime;
  struct List_t * pxCurrentTimerList.3_1;
  long unsigned int _2;
  long int _3;
  struct List_t * pxCurrentTimerList.4_4;
  struct xLIST_ITEM * _5;
  long int iftmp.2_7;
  long int iftmp.2_9;
  long int iftmp.2_10;
  TickType_t _15;

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

  <bb 3> :
  iftmp.2_10 = 1;
  goto <bb 5>; [INV]

  <bb 4> :
  iftmp.2_9 = 0;

  <bb 5> :
  # iftmp.2_7 = PHI <iftmp.2_10(3), iftmp.2_9(4)>
  *pxListWasEmpty_11(D) = iftmp.2_7;
  # DEBUG BEGIN_STMT
  _3 = *pxListWasEmpty_11(D);
  if (_3 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxCurrentTimerList.4_4 = pxCurrentTimerList;
  _5 = pxCurrentTimerList.4_4->xListEnd.pxNext;
  xNextExpireTime_14 = _5->xItemValue;
  # DEBUG xNextExpireTime => xNextExpireTime_14
  goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  xNextExpireTime_13 = 0;
  # DEBUG xNextExpireTime => xNextExpireTime_13

  <bb 8> :
  # xNextExpireTime_6 = PHI <xNextExpireTime_14(6), xNextExpireTime_13(7)>
  # DEBUG xNextExpireTime => xNextExpireTime_6
  # DEBUG BEGIN_STMT
  _15 = xNextExpireTime_6;
  return _15;

}


prvProcessTimerOrBlockTask (const TickType_t xNextExpireTime, BaseType_t xListWasEmpty)
{
  BaseType_t xTimerListsWereSwitched;
  TickType_t xTimeNow;
  long int xTimerListsWereSwitched.5_1;
  struct List_t * pxOverflowTimerList.7_2;
  long unsigned int _3;
  struct QueueDefinition * xTimerQueue.8_4;
  long unsigned int _5;
  long int _6;
  volatile uint32_t * _7;
  long int iftmp.6_9;
  long int iftmp.6_20;
  long int iftmp.6_21;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  xTimeNow_14 = prvSampleTimeNow (&xTimerListsWereSwitched);
  # DEBUG xTimeNow => xTimeNow_14
  # DEBUG BEGIN_STMT
  xTimerListsWereSwitched.5_1 = xTimerListsWereSwitched;
  if (xTimerListsWereSwitched.5_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 13>; [INV]

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

  <bb 4> :
  if (xNextExpireTime_17(D) <= xTimeNow_14)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  prvProcessExpiredTimer (xNextExpireTime_17(D), xTimeNow_14);
  goto <bb 14>; [INV]

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  pxOverflowTimerList.7_2 = pxOverflowTimerList;
  _3 ={v} pxOverflowTimerList.7_2->uxNumberOfItems;
  if (_3 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  iftmp.6_21 = 1;
  goto <bb 10>; [INV]

  <bb 9> :
  iftmp.6_20 = 0;

  <bb 10> :
  # iftmp.6_9 = PHI <iftmp.6_21(8), iftmp.6_20(9)>
  xListWasEmpty_22 = iftmp.6_9;
  # DEBUG xListWasEmpty => xListWasEmpty_22

  <bb 11> :
  # xListWasEmpty_8 = PHI <xListWasEmpty_16(D)(6), xListWasEmpty_22(10)>
  # DEBUG xListWasEmpty => xListWasEmpty_8
  # DEBUG BEGIN_STMT
  xTimerQueue.8_4 = xTimerQueue;
  _5 = xNextExpireTime_17(D) - xTimeNow_14;
  vQueueWaitForMessageRestricted (xTimerQueue.8_4, _5, xListWasEmpty_8);
  # DEBUG BEGIN_STMT
  _6 = xTaskResumeAll ();
  if (_6 == 0)
    goto <bb 12>; [INV]
  else
    goto <bb 14>; [INV]

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

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

  <bb 14> :
  xTimerListsWereSwitched ={v} {CLOBBER};
  return;

}


prvTimerTask (void * pvParameters)
{
  BaseType_t xListWasEmpty;
  TickType_t xNextExpireTime;
  long int xListWasEmpty.1_1;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xNextExpireTime_5 = prvGetNextExpireTime (&xListWasEmpty);
  # DEBUG xNextExpireTime => xNextExpireTime_5
  # DEBUG BEGIN_STMT
  xListWasEmpty.1_1 = xListWasEmpty;
  prvProcessTimerOrBlockTask (xNextExpireTime_5, xListWasEmpty.1_1);
  # DEBUG BEGIN_STMT
  prvProcessReceivedCommands ();
  # DEBUG BEGIN_STMT
  goto <bb 2>; [INV]

}


prvProcessExpiredTimer (const TickType_t xNextExpireTime, const TickType_t xTimeNow)
{
  struct Timer_t * const pxTimer;
  struct List_t * pxCurrentTimerList.13_1;
  struct xLIST_ITEM * _2;
  struct ListItem_t * _3;
  unsigned char _4;
  int _5;
  int _6;
  unsigned char _7;
  unsigned char _8;
  void (*<T689>) (struct tmrTimerControl *) _9;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxCurrentTimerList.13_1 = pxCurrentTimerList;
  _2 = pxCurrentTimerList.13_1->xListEnd.pxNext;
  pxTimer_12 = _2->pvOwner;
  # DEBUG pxTimer => pxTimer_12
  # DEBUG BEGIN_STMT
  _3 = &pxTimer_12->xTimerListItem;
  uxListRemove (_3);
  # DEBUG BEGIN_STMT
  _4 = pxTimer_12->ucStatus;
  _5 = (int) _4;
  _6 = _5 & 4;
  if (_6 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  prvReloadTimer (pxTimer_12, xNextExpireTime_15(D), xTimeNow_16(D));
  goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  _7 = pxTimer_12->ucStatus;
  _8 = _7 & 254;
  pxTimer_12->ucStatus = _8;

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _9 = pxTimer_12->pxCallbackFunction;
  _9 (pxTimer_12);
  return;

}


prvReloadTimer (struct Timer_t * const pxTimer, TickType_t xExpiredTime, const TickType_t xTimeNow)
{
  long unsigned int _1;
  void (*<T689>) (struct tmrTimerControl *) _2;
  long unsigned int _3;
  long unsigned int _4;
  long int _5;

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

  <bb 3> :
  # DEBUG BEGIN_STMT
  _1 = pxTimer_10(D)->xTimerPeriodInTicks;
  xExpiredTime_13 = xExpiredTime_6 + _1;
  # DEBUG xExpiredTime => xExpiredTime_13
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _2 = pxTimer_10(D)->pxCallbackFunction;
  _2 (pxTimer_10(D));

  <bb 4> :
  # xExpiredTime_6 = PHI <xExpiredTime_8(D)(2), xExpiredTime_13(3)>
  # DEBUG xExpiredTime => xExpiredTime_6
  # DEBUG BEGIN_STMT
  _3 = pxTimer_10(D)->xTimerPeriodInTicks;
  _4 = xExpiredTime_6 + _3;
  _5 = prvInsertTimerInActiveList (pxTimer_10(D), _4, xTimeNow_11(D), xExpiredTime_6);
  if (_5 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 5> :
  return;

}


pcTimerGetName (struct tmrTimerControl * xTimer)
{
  struct Timer_t * pxTimer;
  const char * _4;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _4 = pxTimer_2->pcTimerName;
  return _4;

}


xTimerGetExpiryTime (struct tmrTimerControl * xTimer)
{
  TickType_t xReturn;
  struct Timer_t * pxTimer;
  TickType_t _5;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xReturn_4 = pxTimer_2->xTimerListItem.xItemValue;
  # DEBUG xReturn => xReturn_4
  # DEBUG BEGIN_STMT
  _5 = xReturn_4;
  return _5;

}


uxTimerGetReloadMode (struct tmrTimerControl * xTimer)
{
  UBaseType_t uxReturn;
  struct Timer_t * pxTimer;
  unsigned char _1;
  int _2;
  int _3;
  UBaseType_t _12;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _1 = pxTimer_6->ucStatus;
  _2 = (int) _1;
  _3 = _2 & 4;
  if (_3 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  uxReturn_10 = 0;
  # DEBUG uxReturn => uxReturn_10
  goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  uxReturn_9 = 1;
  # DEBUG uxReturn => uxReturn_9

  <bb 8> :
  # uxReturn_4 = PHI <uxReturn_10(6), uxReturn_9(7)>
  # DEBUG uxReturn => uxReturn_4
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _12 = uxReturn_4;
  return _12;

}


vTimerSetReloadMode (struct tmrTimerControl * xTimer, const UBaseType_t uxAutoReload)
{
  struct Timer_t * pxTimer;
  unsigned char _1;
  unsigned char _2;
  unsigned char _3;
  unsigned char _4;

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

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

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

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

  <bb 6> :
  # DEBUG BEGIN_STMT
  _1 = pxTimer_7->ucStatus;
  _2 = _1 | 4;
  pxTimer_7->ucStatus = _2;
  goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  _3 = pxTimer_7->ucStatus;
  _4 = _3 & 251;
  pxTimer_7->ucStatus = _4;

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

}


xTimerGetPeriod (struct tmrTimerControl * xTimer)
{
  struct Timer_t * pxTimer;
  TickType_t _4;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _4 = pxTimer_2->xTimerPeriodInTicks;
  return _4;

}


xTimerGetTimerDaemonTaskHandle ()
{
  struct tskTaskControlBlock * xTimerTaskHandle.24_1;
  struct tskTaskControlBlock * _3;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xTimerTaskHandle.24_1 = xTimerTaskHandle;
  if (xTimerTaskHandle.24_1 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _3 = xTimerTaskHandle;
  return _3;

}


xTimerGenericCommand (struct tmrTimerControl * xTimer, const BaseType_t xCommandID, const TickType_t xOptionalValue, BaseType_t * const pxHigherPriorityTaskWoken, const TickType_t xTicksToWait)
{
  struct DaemonTaskMessage_t xMessage;
  BaseType_t xReturn;
  struct QueueDefinition * xTimerQueue.20_1;
  long int _2;
  struct QueueDefinition * xTimerQueue.21_3;
  struct QueueDefinition * xTimerQueue.22_4;
  struct QueueDefinition * xTimerQueue.23_5;
  BaseType_t _25;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xTimerQueue.20_1 = xTimerQueue;
  if (xTimerQueue.20_1 != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  xMessage.xMessageID = xCommandID_11(D);
  # DEBUG BEGIN_STMT
  xMessage.u.xTimerParameters.xMessageValue = xOptionalValue_13(D);
  # DEBUG BEGIN_STMT
  xMessage.u.xTimerParameters.pxTimer = xTimer_9(D);
  # DEBUG BEGIN_STMT
  if (xCommandID_11(D) <= 5)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  _2 = xTaskGetSchedulerState ();
  if (_2 == 2)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  xTimerQueue.21_3 = xTimerQueue;
  xReturn_24 = xQueueGenericSend (xTimerQueue.21_3, &xMessage, xTicksToWait_22(D), 0);
  # DEBUG xReturn => xReturn_24
  goto <bb 11>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  xTimerQueue.22_4 = xTimerQueue;
  xReturn_21 = xQueueGenericSend (xTimerQueue.22_4, &xMessage, 0, 0);
  # DEBUG xReturn => xReturn_21
  goto <bb 11>; [INV]

  <bb 10> :
  # DEBUG BEGIN_STMT
  xTimerQueue.23_5 = xTimerQueue;
  xReturn_18 = xQueueGenericSendFromISR (xTimerQueue.23_5, &xMessage, pxHigherPriorityTaskWoken_16(D), 0);
  # DEBUG xReturn => xReturn_18

  <bb 11> :
  # xReturn_6 = PHI <xReturn_8(5), xReturn_18(10), xReturn_21(9), xReturn_24(8)>
  # DEBUG xReturn => xReturn_6
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _25 = xReturn_6;
  xMessage ={v} {CLOBBER};
  return _25;

}


prvInitialiseNewTimer (const char * const pcTimerName, const TickType_t xTimerPeriodInTicks, const UBaseType_t uxAutoReload, void * const pvTimerID, void (*TimerCallbackFunction_t) (struct tmrTimerControl *) pxCallbackFunction, struct Timer_t * pxNewTimer)
{
  struct ListItem_t * _1;
  unsigned char _2;
  unsigned char _3;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  prvCheckForValidListAndQueue ();
  # DEBUG BEGIN_STMT
  pxNewTimer_8(D)->pcTimerName = pcTimerName_9(D);
  # DEBUG BEGIN_STMT
  pxNewTimer_8(D)->xTimerPeriodInTicks = xTimerPeriodInTicks_5(D);
  # DEBUG BEGIN_STMT
  pxNewTimer_8(D)->pvTimerID = pvTimerID_12(D);
  # DEBUG BEGIN_STMT
  pxNewTimer_8(D)->pxCallbackFunction = pxCallbackFunction_14(D);
  # DEBUG BEGIN_STMT
  _1 = &pxNewTimer_8(D)->xTimerListItem;
  vListInitialiseItem (_1);
  # DEBUG BEGIN_STMT
  if (uxAutoReload_17(D) != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  _2 = pxNewTimer_8(D)->ucStatus;
  _3 = _2 | 4;
  pxNewTimer_8(D)->ucStatus = _3;

  <bb 7> :
  # DEBUG BEGIN_STMT
  return;

}


xTimerCreate (const char * const pcTimerName, const TickType_t xTimerPeriodInTicks, const UBaseType_t uxAutoReload, void * const pvTimerID, void (*TimerCallbackFunction_t) (struct tmrTimerControl *) pxCallbackFunction)
{
  struct Timer_t * pxNewTimer;
  struct tmrTimerControl * _12;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxNewTimer_4 = pvPortMalloc (44);
  # DEBUG pxNewTimer => pxNewTimer_4
  # DEBUG BEGIN_STMT
  if (pxNewTimer_4 != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxNewTimer_4->ucStatus = 0;
  # DEBUG BEGIN_STMT
  prvInitialiseNewTimer (pcTimerName_6(D), xTimerPeriodInTicks_7(D), uxAutoReload_8(D), pvTimerID_9(D), pxCallbackFunction_10(D), pxNewTimer_4);

  <bb 4> :
  # DEBUG BEGIN_STMT
  _12 = pxNewTimer_4;
  return _12;

}


xTimerCreateTimerTask ()
{
  BaseType_t xReturn;
  struct QueueDefinition * xTimerQueue.0_1;
  BaseType_t _9;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xReturn_4 = 0;
  # DEBUG xReturn => xReturn_4
  # DEBUG BEGIN_STMT
  prvCheckForValidListAndQueue ();
  # DEBUG BEGIN_STMT
  xTimerQueue.0_1 = xTimerQueue;
  if (xTimerQueue.0_1 != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  xReturn_8 = xTaskCreate (prvTimerTask, "Tmr Svc", 180, 0B, 2, &xTimerTaskHandle);
  # DEBUG xReturn => xReturn_8

  <bb 4> :
  # xReturn_2 = PHI <xReturn_4(2), xReturn_8(3)>
  # DEBUG xReturn => xReturn_2
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xReturn_2 == 0)
    goto <bb 5>; [INV]
  else
    goto <bb 7>; [INV]

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

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _9 = xReturn_2;
  return _9;

}


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

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

}