vQueueWaitForMessageRestricted (struct QueueDefinition * xQueue, TickType_t xTicksToWait, const BaseType_t xWaitIndefinitely)
{
  struct Queue_t * const pxQueue;
  signed char _1;
  signed char _2;
  long unsigned int _3;
  struct List_t * _4;

  <bb 2> :
  pxQueue_9 = xQueue_8(D);
  vPortEnterCritical ();
  _1 ={v} pxQueue_9->cRxLock;
  if (_1 == -1)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  pxQueue_9->cRxLock ={v} 0;

  <bb 4> :
  _2 ={v} pxQueue_9->cTxLock;
  if (_2 == -1)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  pxQueue_9->cTxLock ={v} 0;

  <bb 6> :
  vPortExitCritical ();
  _3 ={v} pxQueue_9->uxMessagesWaiting;
  if (_3 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  _4 = &pxQueue_9->xTasksWaitingToReceive;
  vTaskPlaceOnEventListRestricted (_4, xTicksToWait_15(D), xWaitIndefinitely_16(D));

  <bb 8> :
  prvUnlockQueue (pxQueue_9);
  return;

}


vQueueUnregisterQueue (struct QueueDefinition * xQueue)
{
  uint32_t ulNewBASEPRI;
  UBaseType_t ux;
  struct QueueDefinition * _1;

  <bb 2> :
  if (xQueue_4(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_10 : "i" 16 : "memory");

  <bb 4> :

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

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

  <bb 7> :
  _1 = xQueueRegistry[ux_2].xHandle;
  if (xQueue_4(D) == _1)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  xQueueRegistry[ux_2].pcQueueName = 0B;
  xQueueRegistry[ux_2].xHandle = 0B;
  goto <bb 11>; [INV]

  <bb 9> :
  ux_7 = ux_2 + 1;

  <bb 10> :
  # ux_2 = PHI <ux_5(6), ux_7(9)>
  if (ux_2 <= 1)
    goto <bb 7>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 11> :
  return;

}


pcQueueGetName (struct QueueDefinition * xQueue)
{
  uint32_t ulNewBASEPRI;
  const char * pcReturn;
  UBaseType_t ux;
  const char * D.7264;
  struct QueueDefinition * _1;
  const char * _10;

  <bb 2> :
  pcReturn_4 = 0B;
  if (xQueue_5(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> :
  ux_6 = 0;
  goto <bb 10>; [INV]

  <bb 7> :
  _1 = xQueueRegistry[ux_2].xHandle;
  if (xQueue_5(D) == _1)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  pcReturn_9 = xQueueRegistry[ux_2].pcQueueName;
  goto <bb 11>; [INV]

  <bb 9> :
  ux_8 = ux_2 + 1;

  <bb 10> :
  # ux_2 = PHI <ux_6(6), ux_8(9)>
  if (ux_2 <= 1)
    goto <bb 7>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 11> :
  # pcReturn_3 = PHI <pcReturn_9(8), pcReturn_4(10)>
  _10 = pcReturn_3;

  <bb 12> :
<L8>:
  return _10;

}


vQueueAddToRegistry (struct QueueDefinition * xQueue, const char * pcQueueName)
{
  uint32_t ulNewBASEPRI;
  struct QueueRegistryItem_t * pxEntryToWrite;
  UBaseType_t ux;
  struct QueueDefinition * _1;
  const char * _2;

  <bb 2> :
  if (xQueue_8(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_18 : "i" 16 : "memory");

  <bb 4> :

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

  <bb 6> :
  pxEntryToWrite_9 = 0B;
  if (pcQueueName_10(D) != 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 7> :
  ux_11 = 0;
  goto <bb 14>; [INV]

  <bb 8> :
  _1 = xQueueRegistry[ux_3].xHandle;
  if (xQueue_8(D) == _1)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  pxEntryToWrite_15 = &xQueueRegistry[ux_3];
  goto <bb 15>; [INV]

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

  <bb 11> :
  _2 = xQueueRegistry[ux_3].pcQueueName;
  if (_2 == 0B)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  pxEntryToWrite_13 = &xQueueRegistry[ux_3];

  <bb 13> :
  # pxEntryToWrite_4 = PHI <pxEntryToWrite_5(10), pxEntryToWrite_5(11), pxEntryToWrite_13(12)>
  ux_14 = ux_3 + 1;

  <bb 14> :
  # ux_3 = PHI <ux_11(7), ux_14(13)>
  # pxEntryToWrite_5 = PHI <pxEntryToWrite_9(7), pxEntryToWrite_4(13)>
  if (ux_3 <= 1)
    goto <bb 8>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 15> :
  # pxEntryToWrite_6 = PHI <pxEntryToWrite_9(6), pxEntryToWrite_15(9), pxEntryToWrite_5(14)>
  if (pxEntryToWrite_6 != 0B)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  pxEntryToWrite_6->pcQueueName = pcQueueName_10(D);
  pxEntryToWrite_6->xHandle = xQueue_8(D);

  <bb 17> :
  return;

}


xQueueIsQueueFullFromISR (struct QueueDefinition * const xQueue)
{
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  BaseType_t D.7245;
  long unsigned int _1;
  long unsigned int _2;
  BaseType_t _9;

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

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

  <bb 4> :

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

  <bb 6> :
  _1 ={v} pxQueue_5->uxMessagesWaiting;
  _2 = pxQueue_5->uxLength;
  if (_1 == _2)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  xReturn_8 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  xReturn_7 = 0;

  <bb 9> :
  # xReturn_3 = PHI <xReturn_8(7), xReturn_7(8)>
  _9 = xReturn_3;

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

}


prvIsQueueFull (const struct Queue_t * pxQueue)
{
  BaseType_t xReturn;
  BaseType_t D.7238;
  long unsigned int _1;
  long unsigned int _2;
  BaseType_t _10;

  <bb 2> :
  vPortEnterCritical ();
  _1 ={v} pxQueue_6(D)->uxMessagesWaiting;
  _2 = pxQueue_6(D)->uxLength;
  if (_1 == _2)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  xReturn_8 = 1;
  goto <bb 5>; [INV]

  <bb 4> :
  xReturn_7 = 0;

  <bb 5> :
  # xReturn_3 = PHI <xReturn_8(3), xReturn_7(4)>
  vPortExitCritical ();
  _10 = xReturn_3;

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

}


xQueueIsQueueEmptyFromISR (struct QueueDefinition * const xQueue)
{
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  BaseType_t D.7233;
  long unsigned int _1;
  BaseType_t _8;

  <bb 2> :
  pxQueue_4 = xQueue_3(D);
  if (pxQueue_4 == 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> :
  _1 ={v} pxQueue_4->uxMessagesWaiting;
  if (_1 == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

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

  <bb 8> :
  xReturn_6 = 0;

  <bb 9> :
  # xReturn_2 = PHI <xReturn_7(7), xReturn_6(8)>
  _8 = xReturn_2;

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

}


prvIsQueueEmpty (const struct Queue_t * pxQueue)
{
  BaseType_t xReturn;
  BaseType_t D.7226;
  long unsigned int _1;
  BaseType_t _9;

  <bb 2> :
  vPortEnterCritical ();
  _1 ={v} pxQueue_5(D)->uxMessagesWaiting;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

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

  <bb 4> :
  xReturn_6 = 0;

  <bb 5> :
  # xReturn_2 = PHI <xReturn_7(3), xReturn_6(4)>
  vPortExitCritical ();
  _9 = xReturn_2;

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

}


prvUnlockQueue (struct Queue_t * const pxQueue)
{
  int8_t cRxLock;
  int8_t cTxLock;
  long unsigned int _1;
  struct List_t * _2;
  long int _3;
  unsigned char cTxLock.28_4;
  unsigned char _5;
  long unsigned int _6;
  struct List_t * _7;
  long int _8;
  unsigned char cRxLock.29_9;
  unsigned char _10;

  <bb 2> :
  vPortEnterCritical ();
  cTxLock_20 ={v} pxQueue_19(D)->cTxLock;
  goto <bb 8>; [INV]

  <bb 3> :
  _1 ={v} pxQueue_19(D)->xTasksWaitingToReceive.uxNumberOfItems;
  if (_1 != 0)
    goto <bb 4>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 4> :
  _2 = &pxQueue_19(D)->xTasksWaitingToReceive;
  _3 = xTaskRemoveFromEventList (_2);
  if (_3 != 0)
    goto <bb 5>; [INV]
  else
    goto <bb 7>; [INV]

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

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

  <bb 7> :
  cTxLock.28_4 = (unsigned char) cTxLock_11;
  _5 = cTxLock.28_4 + 255;
  cTxLock_23 = (int8_t) _5;

  <bb 8> :
  # cTxLock_11 = PHI <cTxLock_20(2), cTxLock_23(7)>
  if (cTxLock_11 > 0)
    goto <bb 3>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 9> :
  pxQueue_19(D)->cTxLock ={v} -1;
  vPortExitCritical ();
  vPortEnterCritical ();
  cRxLock_27 ={v} pxQueue_19(D)->cRxLock;
  goto <bb 15>; [INV]

  <bb 10> :
  _6 ={v} pxQueue_19(D)->xTasksWaitingToSend.uxNumberOfItems;
  if (_6 != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 11> :
  _7 = &pxQueue_19(D)->xTasksWaitingToSend;
  _8 = xTaskRemoveFromEventList (_7);
  if (_8 != 0)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  vTaskMissedYield ();

  <bb 13> :
  cRxLock.29_9 = (unsigned char) cRxLock_12;
  _10 = cRxLock.29_9 + 255;
  cRxLock_30 = (int8_t) _10;
  goto <bb 15>; [INV]

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

  <bb 15> :
  # cRxLock_12 = PHI <cRxLock_27(9), cRxLock_30(13)>
  if (cRxLock_12 > 0)
    goto <bb 10>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 16> :
  pxQueue_19(D)->cRxLock ={v} -1;
  vPortExitCritical ();
  return;

}


prvCopyDataFromQueue (struct Queue_t * const pxQueue, void * const pvBuffer)
{
  long unsigned int _1;
  int8_t * _2;
  long unsigned int _3;
  int8_t * _4;
  int8_t * _5;
  int8_t * _6;
  int8_t * _7;
  int8_t * _8;
  long unsigned int _9;

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

  <bb 3> :
  _2 = pxQueue_13(D)->u.xQueue.pcReadFrom;
  _3 = pxQueue_13(D)->uxItemSize;
  _4 = _2 + _3;
  pxQueue_13(D)->u.xQueue.pcReadFrom = _4;
  _5 = pxQueue_13(D)->u.xQueue.pcReadFrom;
  _6 = pxQueue_13(D)->u.xQueue.pcTail;
  if (_5 >= _6)
    goto <bb 4>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 4> :
  _7 = pxQueue_13(D)->pcHead;
  pxQueue_13(D)->u.xQueue.pcReadFrom = _7;

  <bb 5> :
  _8 = pxQueue_13(D)->u.xQueue.pcReadFrom;
  _9 = pxQueue_13(D)->uxItemSize;
  memcpy (pvBuffer_16(D), _8, _9);

  <bb 6> :
  return;

}


prvCopyDataToQueue (struct Queue_t * const pxQueue, const void * pvItemToQueue, const BaseType_t xPosition)
{
  UBaseType_t uxMessagesWaiting;
  BaseType_t xReturn;
  BaseType_t D.7204;
  long unsigned int _1;
  int8_t * _2;
  struct tskTaskControlBlock * _3;
  int8_t * _4;
  long unsigned int _5;
  int8_t * _6;
  long unsigned int _7;
  int8_t * _8;
  int8_t * _9;
  int8_t * _10;
  int8_t * _11;
  int8_t * _12;
  long unsigned int _13;
  int8_t * _14;
  long unsigned int _15;
  sizetype _16;
  int8_t * _17;
  int8_t * _18;
  int8_t * _19;
  int8_t * _20;
  long unsigned int _21;
  sizetype _22;
  int8_t * _23;
  long unsigned int _24;
  BaseType_t _46;

  <bb 2> :
  xReturn_29 = 0;
  uxMessagesWaiting_32 ={v} pxQueue_31(D)->uxMessagesWaiting;
  _1 = pxQueue_31(D)->uxItemSize;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  _2 = pxQueue_31(D)->pcHead;
  if (_2 == 0B)
    goto <bb 4>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 4> :
  _3 = pxQueue_31(D)->u.xSemaphore.xMutexHolder;
  xReturn_43 = xTaskPriorityDisinherit (_3);
  pxQueue_31(D)->u.xSemaphore.xMutexHolder = 0B;
  goto <bb 13>; [INV]

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

  <bb 6> :
  _4 = pxQueue_31(D)->pcWriteTo;
  _5 = pxQueue_31(D)->uxItemSize;
  memcpy (_4, pvItemToQueue_34(D), _5);
  _6 = pxQueue_31(D)->pcWriteTo;
  _7 = pxQueue_31(D)->uxItemSize;
  _8 = _6 + _7;
  pxQueue_31(D)->pcWriteTo = _8;
  _9 = pxQueue_31(D)->pcWriteTo;
  _10 = pxQueue_31(D)->u.xQueue.pcTail;
  if (_9 >= _10)
    goto <bb 7>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 7> :
  _11 = pxQueue_31(D)->pcHead;
  pxQueue_31(D)->pcWriteTo = _11;
  goto <bb 13>; [INV]

  <bb 8> :
  _12 = pxQueue_31(D)->u.xQueue.pcReadFrom;
  _13 = pxQueue_31(D)->uxItemSize;
  memcpy (_12, pvItemToQueue_34(D), _13);
  _14 = pxQueue_31(D)->u.xQueue.pcReadFrom;
  _15 = pxQueue_31(D)->uxItemSize;
  _16 = -_15;
  _17 = _14 + _16;
  pxQueue_31(D)->u.xQueue.pcReadFrom = _17;
  _18 = pxQueue_31(D)->u.xQueue.pcReadFrom;
  _19 = pxQueue_31(D)->pcHead;
  if (_18 < _19)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  _20 = pxQueue_31(D)->u.xQueue.pcTail;
  _21 = pxQueue_31(D)->uxItemSize;
  _22 = -_21;
  _23 = _20 + _22;
  pxQueue_31(D)->u.xQueue.pcReadFrom = _23;

  <bb 10> :
  if (xPosition_33(D) == 2)
    goto <bb 11>; [INV]
  else
    goto <bb 13>; [INV]

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

  <bb 12> :
  uxMessagesWaiting_38 = uxMessagesWaiting_32 + 4294967295;

  <bb 13> :
  # xReturn_25 = PHI <xReturn_43(4), xReturn_29(7), xReturn_29(10), xReturn_29(12), xReturn_29(3), xReturn_29(6), xReturn_29(11)>
  # uxMessagesWaiting_26 = PHI <uxMessagesWaiting_32(4), uxMessagesWaiting_32(7), uxMessagesWaiting_32(10), uxMessagesWaiting_38(12), uxMessagesWaiting_32(3), uxMessagesWaiting_32(6), uxMessagesWaiting_32(11)>
  _24 = uxMessagesWaiting_26 + 1;
  pxQueue_31(D)->uxMessagesWaiting ={v} _24;
  _46 = xReturn_25;

  <bb 14> :
<L21>:
  return _46;

}


prvGetDisinheritPriorityAfterTimeout (const struct Queue_t * const pxQueue)
{
  UBaseType_t uxHighestPriorityOfWaitingTasks;
  UBaseType_t D.7181;
  long unsigned int _1;
  struct xLIST_ITEM * _2;
  long unsigned int _3;
  UBaseType_t _9;

  <bb 2> :
  _1 ={v} pxQueue_6(D)->xTasksWaitingToReceive.uxNumberOfItems;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  _2 = pxQueue_6(D)->xTasksWaitingToReceive.xListEnd.pxNext;
  _3 = _2->xItemValue;
  uxHighestPriorityOfWaitingTasks_8 = 5 - _3;
  goto <bb 5>; [INV]

  <bb 4> :
  uxHighestPriorityOfWaitingTasks_7 = 0;

  <bb 5> :
  # uxHighestPriorityOfWaitingTasks_4 = PHI <uxHighestPriorityOfWaitingTasks_8(3), uxHighestPriorityOfWaitingTasks_7(4)>
  _9 = uxHighestPriorityOfWaitingTasks_4;

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

}


ucQueueGetQueueType (struct QueueDefinition * xQueue)
{
  uint8_t D.7176;
  uint8_t _3;

  <bb 2> :
  _3 = MEM[(struct Queue_t *)xQueue_2(D)].ucQueueType;

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

}


vQueueSetQueueNumber (struct QueueDefinition * xQueue, UBaseType_t uxQueueNumber)
{
  <bb 2> :
  MEM[(struct Queue_t *)xQueue_2(D)].uxQueueNumber = uxQueueNumber_3(D);
  return;

}


uxQueueGetQueueNumber (struct QueueDefinition * xQueue)
{
  UBaseType_t D.7174;
  UBaseType_t _3;

  <bb 2> :
  _3 = MEM[(struct Queue_t *)xQueue_2(D)].uxQueueNumber;

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

}


vQueueDelete (struct QueueDefinition * xQueue)
{
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxQueue;

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

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

  <bb 4> :

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

  <bb 6> :
  vQueueUnregisterQueue (pxQueue_2);
  vPortFree (pxQueue_2);
  return;

}


uxQueueMessagesWaitingFromISR (struct QueueDefinition * const xQueue)
{
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxQueue;
  UBaseType_t uxReturn;
  UBaseType_t D.7170;
  UBaseType_t _5;

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

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

  <bb 4> :

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

  <bb 6> :
  uxReturn_4 ={v} pxQueue_2->uxMessagesWaiting;
  _5 = uxReturn_4;

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

}


uxQueueSpacesAvailable (struct QueueDefinition * const xQueue)
{
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxQueue;
  UBaseType_t uxReturn;
  UBaseType_t D.7166;
  long unsigned int _1;
  long unsigned int _2;
  UBaseType_t _9;

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

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

  <bb 4> :

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

  <bb 6> :
  vPortEnterCritical ();
  _1 = pxQueue_4->uxLength;
  _2 ={v} pxQueue_4->uxMessagesWaiting;
  uxReturn_7 = _1 - _2;
  vPortExitCritical ();
  _9 = uxReturn_7;

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

}


uxQueueMessagesWaiting (struct QueueDefinition * const xQueue)
{
  uint32_t ulNewBASEPRI;
  UBaseType_t uxReturn;
  UBaseType_t D.7162;
  UBaseType_t _6;

  <bb 2> :
  if (xQueue_1(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_7 : "i" 16 : "memory");

  <bb 4> :

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

  <bb 6> :
  vPortEnterCritical ();
  uxReturn_4 ={v} MEM[(struct Queue_t *)xQueue_1(D)].uxMessagesWaiting;
  vPortExitCritical ();
  _6 = uxReturn_4;

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

}


xQueuePeekFromISR (struct QueueDefinition * xQueue, void * const pvBuffer)
{
  uint32_t ulNewMaskValue;
  uint32_t D.7361;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.7360;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxQueue;
  int8_t * pcOriginalReadPosition;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  BaseType_t D.7158;
  int iftmp.27;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  int iftmp.27_5;
  int iftmp.27_11;
  int iftmp.27_12;
  BaseType_t _20;
  long unsigned int _26;

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

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

  <bb 4> :

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

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

  <bb 7> :
  _1 = pxQueue_8->uxItemSize;
  if (_1 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  iftmp.27_12 = 1;
  goto <bb 10>; [INV]

  <bb 9> :
  iftmp.27_11 = 0;

  <bb 10> :
  # iftmp.27_5 = PHI <iftmp.27_12(8), iftmp.27_11(9)>
  if (iftmp.27_5 == 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 12> :

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

  <bb 14> :
  _2 = pxQueue_8->uxItemSize;
  if (_2 == 0)
    goto <bb 15>; [INV]
  else
    goto <bb 18>; [INV]

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

  <bb 16> :

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

  <bb 18> :
  vPortValidateInterruptPriority ();
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_24, "=r" ulNewBASEPRI_25 : "i" 16 : "memory");
  _26 = ulOriginalBASEPRI_24;

  <bb 19> :
<L17>:
  _29 = _26;

  <bb 20> :
  uxSavedInterruptStatus_14 = _29;
  _3 ={v} pxQueue_8->uxMessagesWaiting;
  if (_3 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  pcOriginalReadPosition_16 = pxQueue_8->u.xQueue.pcReadFrom;
  prvCopyDataFromQueue (pxQueue_8, pvBuffer_9(D));
  pxQueue_8->u.xQueue.pcReadFrom = pcOriginalReadPosition_16;
  xReturn_19 = 1;
  goto <bb 23>; [INV]

  <bb 22> :
  xReturn_15 = 0;

  <bb 23> :
  # xReturn_4 = PHI <xReturn_19(21), xReturn_15(22)>
  ulNewMaskValue_27 = uxSavedInterruptStatus_14;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_27 : "memory");

  <bb 24> :
  _20 = xReturn_4;

  <bb 25> :
<L16>:
  return _20;

}


xQueueReceiveFromISR (struct QueueDefinition * xQueue, void * const pvBuffer, BaseType_t * const pxHigherPriorityTaskWoken)
{
  uint32_t ulNewMaskValue;
  uint32_t ulNewBASEPRI;
  uint32_t D.7351;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.7350;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  const int8_t cRxLock;
  const UBaseType_t uxMessagesWaiting;
  struct Queue_t * const pxQueue;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  BaseType_t D.7142;
  int iftmp.25;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  struct List_t * _4;
  long int _5;
  unsigned char cRxLock.26_6;
  unsigned char _7;
  signed char _8;
  int iftmp.25_10;
  int iftmp.25_17;
  int iftmp.25_18;
  BaseType_t _31;
  long unsigned int _36;

  <bb 2> :
  pxQueue_14 = xQueue_13(D);
  if (pxQueue_14 == 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 (pvBuffer_15(D) != 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 7> :
  _1 = pxQueue_14->uxItemSize;
  if (_1 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

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

  <bb 9> :
  iftmp.25_17 = 0;

  <bb 10> :
  # iftmp.25_10 = PHI <iftmp.25_18(8), iftmp.25_17(9)>
  if (iftmp.25_10 == 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 12> :

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

  <bb 14> :
  vPortValidateInterruptPriority ();
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_34, "=r" ulNewBASEPRI_35 : "i" 16 : "memory");
  _36 = ulOriginalBASEPRI_34;

  <bb 15> :
<L29>:
  _40 = _36;

  <bb 16> :
  uxSavedInterruptStatus_20 = _40;
  uxMessagesWaiting_21 ={v} pxQueue_14->uxMessagesWaiting;
  if (uxMessagesWaiting_21 != 0)
    goto <bb 17>; [INV]
  else
    goto <bb 28>; [INV]

  <bb 17> :
  cRxLock_23 ={v} pxQueue_14->cRxLock;
  prvCopyDataFromQueue (pxQueue_14, pvBuffer_15(D));
  _2 = uxMessagesWaiting_21 + 4294967295;
  pxQueue_14->uxMessagesWaiting ={v} _2;
  if (cRxLock_23 == -1)
    goto <bb 18>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 18> :
  _3 ={v} pxQueue_14->xTasksWaitingToSend.uxNumberOfItems;
  if (_3 != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 19> :
  _4 = &pxQueue_14->xTasksWaitingToSend;
  _5 = xTaskRemoveFromEventList (_4);
  if (_5 != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 20> :
  if (pxHigherPriorityTaskWoken_28(D) != 0B)
    goto <bb 21>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 21> :
  *pxHigherPriorityTaskWoken_28(D) = 1;
  goto <bb 27>; [INV]

  <bb 22> :
  if (cRxLock_23 == 127)
    goto <bb 23>; [INV]
  else
    goto <bb 26>; [INV]

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

  <bb 24> :

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

  <bb 26> :
  cRxLock.26_6 = (unsigned char) cRxLock_23;
  _7 = cRxLock.26_6 + 1;
  _8 = (signed char) _7;
  pxQueue_14->cRxLock ={v} _8;

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

  <bb 28> :
  xReturn_22 = 0;

  <bb 29> :
  # xReturn_9 = PHI <xReturn_30(27), xReturn_22(28)>
  ulNewMaskValue_38 = uxSavedInterruptStatus_20;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_38 : "memory");

  <bb 30> :
  _31 = xReturn_9;

  <bb 31> :
<L28>:
  return _31;

}


xQueuePeek (struct QueueDefinition * xQueue, void * const pvBuffer, TickType_t xTicksToWait)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  const UBaseType_t uxMessagesWaiting;
  struct Queue_t * const pxQueue;
  int8_t * pcOriginalReadPosition;
  struct TimeOut_t xTimeOut;
  BaseType_t xEntryTimeSet;
  BaseType_t D.7093;
  int iftmp.21;
  int iftmp.20;
  long unsigned int _1;
  long int _2;
  long unsigned int xTicksToWait.22_3;
  long unsigned int _4;
  struct List_t * _5;
  long int _6;
  volatile uint32_t * _7;
  long unsigned int xTicksToWait.23_8;
  signed char _9;
  signed char _10;
  long int _11;
  long int _12;
  struct List_t * _13;
  long unsigned int xTicksToWait.24_14;
  long int _15;
  volatile uint32_t * _16;
  long int _17;
  int iftmp.20_20;
  int iftmp.21_21;
  BaseType_t _22;
  int iftmp.20_35;
  int iftmp.20_36;
  int iftmp.21_38;
  int iftmp.21_39;
  BaseType_t _54;
  BaseType_t _65;
  BaseType_t _74;

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

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

  <bb 4> :

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

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

  <bb 7> :
  _1 = pxQueue_32->uxItemSize;
  if (_1 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  iftmp.20_36 = 1;
  goto <bb 10>; [INV]

  <bb 9> :
  iftmp.20_35 = 0;

  <bb 10> :
  # iftmp.20_20 = PHI <iftmp.20_36(8), iftmp.20_35(9)>
  if (iftmp.20_20 == 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 12> :

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

  <bb 14> :
  _2 = xTaskGetSchedulerState ();
  if (_2 != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 15> :
  xTicksToWait.22_3 = xTicksToWait;
  if (xTicksToWait.22_3 == 0)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  iftmp.21_39 = 1;
  goto <bb 18>; [INV]

  <bb 17> :
  iftmp.21_38 = 0;

  <bb 18> :
  # iftmp.21_21 = PHI <iftmp.21_39(16), iftmp.21_38(17)>
  if (iftmp.21_21 == 0)
    goto <bb 19>; [INV]
  else
    goto <bb 22>; [INV]

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

  <bb 20> :

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

  <bb 22> :
  # xEntryTimeSet_18 = PHI <xEntryTimeSet_30(18), xEntryTimeSet_19(42)>
  vPortEnterCritical ();
  uxMessagesWaiting_41 ={v} pxQueue_32->uxMessagesWaiting;
  if (uxMessagesWaiting_41 != 0)
    goto <bb 23>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 23> :
  pcOriginalReadPosition_66 = pxQueue_32->u.xQueue.pcReadFrom;
  prvCopyDataFromQueue (pxQueue_32, pvBuffer_33(D));
  pxQueue_32->u.xQueue.pcReadFrom = pcOriginalReadPosition_66;
  _4 ={v} pxQueue_32->xTasksWaitingToReceive.uxNumberOfItems;
  if (_4 != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 24> :
  _5 = &pxQueue_32->xTasksWaitingToReceive;
  _6 = xTaskRemoveFromEventList (_5);
  if (_6 != 0)
    goto <bb 25>; [INV]
  else
    goto <bb 26>; [INV]

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

  <bb 26> :
  vPortExitCritical ();
  _74 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 43>; [INV]

  <bb 27> :
  xTicksToWait.23_8 = xTicksToWait;
  if (xTicksToWait.23_8 == 0)
    goto <bb 28>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 28> :
  vPortExitCritical ();
  _65 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 43>; [INV]

  <bb 29> :
  if (xEntryTimeSet_18 == 0)
    goto <bb 30>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 30> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet_43 = 1;

  <bb 31> :
  # xEntryTimeSet_19 = PHI <xEntryTimeSet_18(29), xEntryTimeSet_43(30)>
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _9 ={v} pxQueue_32->cRxLock;
  if (_9 == -1)
    goto <bb 32>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 32> :
  pxQueue_32->cRxLock ={v} 0;

  <bb 33> :
  _10 ={v} pxQueue_32->cTxLock;
  if (_10 == -1)
    goto <bb 34>; [INV]
  else
    goto <bb 35>; [INV]

  <bb 34> :
  pxQueue_32->cTxLock ={v} 0;

  <bb 35> :
  vPortExitCritical ();
  _11 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_11 == 0)
    goto <bb 36>; [INV]
  else
    goto <bb 40>; [INV]

  <bb 36> :
  _12 = prvIsQueueEmpty (pxQueue_32);
  if (_12 != 0)
    goto <bb 37>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 37> :
  _13 = &pxQueue_32->xTasksWaitingToReceive;
  xTicksToWait.24_14 = xTicksToWait;
  vTaskPlaceOnEventList (_13, xTicksToWait.24_14);
  prvUnlockQueue (pxQueue_32);
  _15 = xTaskResumeAll ();
  if (_15 == 0)
    goto <bb 38>; [INV]
  else
    goto <bb 42>; [INV]

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

  <bb 39> :
  prvUnlockQueue (pxQueue_32);
  xTaskResumeAll ();
  goto <bb 42>; [INV]

  <bb 40> :
  prvUnlockQueue (pxQueue_32);
  xTaskResumeAll ();
  _17 = prvIsQueueEmpty (pxQueue_32);
  if (_17 != 0)
    goto <bb 41>; [INV]
  else
    goto <bb 42>; [INV]

  <bb 41> :
  _54 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 43>; [INV]

  <bb 42> :
  goto <bb 22>; [INV]

  <bb 43> :
  # _22 = PHI <_74(26), _65(28), _54(41)>
  xTimeOut ={v} {CLOBBER};

  <bb 44> :
<L47>:
  return _22;

}


xQueueSemaphoreTake (struct QueueDefinition * xQueue, TickType_t xTicksToWait)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  UBaseType_t uxHighestWaitingPriority;
  const UBaseType_t uxSemaphoreCount;
  BaseType_t xInheritanceOccurred;
  struct Queue_t * const pxQueue;
  struct TimeOut_t xTimeOut;
  BaseType_t xEntryTimeSet;
  BaseType_t D.7039;
  int iftmp.16;
  long unsigned int _1;
  long int _2;
  long unsigned int xTicksToWait.17_3;
  long unsigned int _4;
  int8_t * _5;
  struct tskTaskControlBlock * _6;
  long unsigned int _7;
  struct List_t * _8;
  long int _9;
  volatile uint32_t * _10;
  long unsigned int xTicksToWait.18_11;
  signed char _12;
  signed char _13;
  long int _14;
  long int _15;
  int8_t * _16;
  struct tskTaskControlBlock * _17;
  struct List_t * _18;
  long unsigned int xTicksToWait.19_19;
  long int _20;
  volatile uint32_t * _21;
  long int _22;
  struct tskTaskControlBlock * _23;
  int iftmp.16_29;
  BaseType_t _30;
  int iftmp.16_47;
  int iftmp.16_48;
  BaseType_t _68;
  BaseType_t _83;
  BaseType_t _92;

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

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

  <bb 4> :

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

  <bb 6> :
  _1 = pxQueue_43->uxItemSize;
  if (_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_95 : "i" 16 : "memory");

  <bb 8> :

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

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

  <bb 11> :
  xTicksToWait.17_3 = xTicksToWait;
  if (xTicksToWait.17_3 == 0)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  iftmp.16_48 = 1;
  goto <bb 14>; [INV]

  <bb 13> :
  iftmp.16_47 = 0;

  <bb 14> :
  # iftmp.16_29 = PHI <iftmp.16_48(12), iftmp.16_47(13)>
  if (iftmp.16_29 == 0)
    goto <bb 15>; [INV]
  else
    goto <bb 18>; [INV]

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

  <bb 16> :

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

  <bb 18> :
  # xEntryTimeSet_24 = PHI <xEntryTimeSet_41(14), xEntryTimeSet_25(48)>
  # xInheritanceOccurred_26 = PHI <xInheritanceOccurred_44(14), xInheritanceOccurred_28(48)>
  vPortEnterCritical ();
  uxSemaphoreCount_50 ={v} pxQueue_43->uxMessagesWaiting;
  if (uxSemaphoreCount_50 != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 19> :
  _4 = uxSemaphoreCount_50 + 4294967295;
  pxQueue_43->uxMessagesWaiting ={v} _4;
  _5 = pxQueue_43->pcHead;
  if (_5 == 0B)
    goto <bb 20>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 20> :
  _6 = pvTaskIncrementMutexHeldCount ();
  pxQueue_43->u.xSemaphore.xMutexHolder = _6;

  <bb 21> :
  _7 ={v} pxQueue_43->xTasksWaitingToSend.uxNumberOfItems;
  if (_7 != 0)
    goto <bb 22>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 22> :
  _8 = &pxQueue_43->xTasksWaitingToSend;
  _9 = xTaskRemoveFromEventList (_8);
  if (_9 != 0)
    goto <bb 23>; [INV]
  else
    goto <bb 24>; [INV]

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

  <bb 24> :
  vPortExitCritical ();
  _92 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 49>; [INV]

  <bb 25> :
  xTicksToWait.18_11 = xTicksToWait;
  if (xTicksToWait.18_11 == 0)
    goto <bb 26>; [INV]
  else
    goto <bb 31>; [INV]

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

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

  <bb 28> :

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

  <bb 30> :
  vPortExitCritical ();
  _83 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 49>; [INV]

  <bb 31> :
  if (xEntryTimeSet_24 == 0)
    goto <bb 32>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 32> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet_52 = 1;

  <bb 33> :
  # xEntryTimeSet_25 = PHI <xEntryTimeSet_24(31), xEntryTimeSet_52(32)>
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _12 ={v} pxQueue_43->cRxLock;
  if (_12 == -1)
    goto <bb 34>; [INV]
  else
    goto <bb 35>; [INV]

  <bb 34> :
  pxQueue_43->cRxLock ={v} 0;

  <bb 35> :
  _13 ={v} pxQueue_43->cTxLock;
  if (_13 == -1)
    goto <bb 36>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 36> :
  pxQueue_43->cTxLock ={v} 0;

  <bb 37> :
  vPortExitCritical ();
  _14 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_14 == 0)
    goto <bb 38>; [INV]
  else
    goto <bb 44>; [INV]

  <bb 38> :
  _15 = prvIsQueueEmpty (pxQueue_43);
  if (_15 != 0)
    goto <bb 39>; [INV]
  else
    goto <bb 43>; [INV]

  <bb 39> :
  _16 = pxQueue_43->pcHead;
  if (_16 == 0B)
    goto <bb 40>; [INV]
  else
    goto <bb 41>; [INV]

  <bb 40> :
  vPortEnterCritical ();
  _17 = pxQueue_43->u.xSemaphore.xMutexHolder;
  xInheritanceOccurred_74 = xTaskPriorityInherit (_17);
  vPortExitCritical ();

  <bb 41> :
  # xInheritanceOccurred_27 = PHI <xInheritanceOccurred_26(39), xInheritanceOccurred_74(40)>
  _18 = &pxQueue_43->xTasksWaitingToReceive;
  xTicksToWait.19_19 = xTicksToWait;
  vTaskPlaceOnEventList (_18, xTicksToWait.19_19);
  prvUnlockQueue (pxQueue_43);
  _20 = xTaskResumeAll ();
  if (_20 == 0)
    goto <bb 42>; [INV]
  else
    goto <bb 48>; [INV]

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

  <bb 43> :
  prvUnlockQueue (pxQueue_43);
  xTaskResumeAll ();
  goto <bb 48>; [INV]

  <bb 44> :
  prvUnlockQueue (pxQueue_43);
  xTaskResumeAll ();
  _22 = prvIsQueueEmpty (pxQueue_43);
  if (_22 != 0)
    goto <bb 45>; [INV]
  else
    goto <bb 48>; [INV]

  <bb 45> :
  if (xInheritanceOccurred_26 != 0)
    goto <bb 46>; [INV]
  else
    goto <bb 47>; [INV]

  <bb 46> :
  vPortEnterCritical ();
  uxHighestWaitingPriority_65 = prvGetDisinheritPriorityAfterTimeout (pxQueue_43);
  _23 = pxQueue_43->u.xSemaphore.xMutexHolder;
  vTaskPriorityDisinheritAfterTimeout (_23, uxHighestWaitingPriority_65);
  vPortExitCritical ();

  <bb 47> :
  _68 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 49>; [INV]

  <bb 48> :
  # xInheritanceOccurred_28 = PHI <xInheritanceOccurred_26(43), xInheritanceOccurred_26(44), xInheritanceOccurred_27(42), xInheritanceOccurred_27(41)>
  goto <bb 18>; [INV]

  <bb 49> :
  # _30 = PHI <_92(24), _83(30), _68(47)>
  xTimeOut ={v} {CLOBBER};

  <bb 50> :
<L54>:
  return _30;

}


xQueueReceive (struct QueueDefinition * xQueue, void * const pvBuffer, TickType_t xTicksToWait)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  const UBaseType_t uxMessagesWaiting;
  struct Queue_t * const pxQueue;
  struct TimeOut_t xTimeOut;
  BaseType_t xEntryTimeSet;
  BaseType_t D.6994;
  int iftmp.12;
  int iftmp.11;
  long unsigned int _1;
  long int _2;
  long unsigned int xTicksToWait.13_3;
  long unsigned int _4;
  long unsigned int _5;
  struct List_t * _6;
  long int _7;
  volatile uint32_t * _8;
  long unsigned int xTicksToWait.14_9;
  signed char _10;
  signed char _11;
  long int _12;
  long int _13;
  struct List_t * _14;
  long unsigned int xTicksToWait.15_15;
  long int _16;
  volatile uint32_t * _17;
  long int _18;
  int iftmp.11_21;
  int iftmp.12_22;
  BaseType_t _23;
  int iftmp.11_36;
  int iftmp.11_37;
  int iftmp.12_39;
  int iftmp.12_40;
  BaseType_t _55;
  BaseType_t _66;
  BaseType_t _74;

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

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

  <bb 4> :

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

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

  <bb 7> :
  _1 = pxQueue_33->uxItemSize;
  if (_1 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  iftmp.11_37 = 1;
  goto <bb 10>; [INV]

  <bb 9> :
  iftmp.11_36 = 0;

  <bb 10> :
  # iftmp.11_21 = PHI <iftmp.11_37(8), iftmp.11_36(9)>
  if (iftmp.11_21 == 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 12> :

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

  <bb 14> :
  _2 = xTaskGetSchedulerState ();
  if (_2 != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 15> :
  xTicksToWait.13_3 = xTicksToWait;
  if (xTicksToWait.13_3 == 0)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  iftmp.12_40 = 1;
  goto <bb 18>; [INV]

  <bb 17> :
  iftmp.12_39 = 0;

  <bb 18> :
  # iftmp.12_22 = PHI <iftmp.12_40(16), iftmp.12_39(17)>
  if (iftmp.12_22 == 0)
    goto <bb 19>; [INV]
  else
    goto <bb 22>; [INV]

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

  <bb 20> :

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

  <bb 22> :
  # xEntryTimeSet_19 = PHI <xEntryTimeSet_31(18), xEntryTimeSet_20(42)>
  vPortEnterCritical ();
  uxMessagesWaiting_42 ={v} pxQueue_33->uxMessagesWaiting;
  if (uxMessagesWaiting_42 != 0)
    goto <bb 23>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 23> :
  prvCopyDataFromQueue (pxQueue_33, pvBuffer_34(D));
  _4 = uxMessagesWaiting_42 + 4294967295;
  pxQueue_33->uxMessagesWaiting ={v} _4;
  _5 ={v} pxQueue_33->xTasksWaitingToSend.uxNumberOfItems;
  if (_5 != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 24> :
  _6 = &pxQueue_33->xTasksWaitingToSend;
  _7 = xTaskRemoveFromEventList (_6);
  if (_7 != 0)
    goto <bb 25>; [INV]
  else
    goto <bb 26>; [INV]

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

  <bb 26> :
  vPortExitCritical ();
  _74 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 43>; [INV]

  <bb 27> :
  xTicksToWait.14_9 = xTicksToWait;
  if (xTicksToWait.14_9 == 0)
    goto <bb 28>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 28> :
  vPortExitCritical ();
  _66 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 43>; [INV]

  <bb 29> :
  if (xEntryTimeSet_19 == 0)
    goto <bb 30>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 30> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet_44 = 1;

  <bb 31> :
  # xEntryTimeSet_20 = PHI <xEntryTimeSet_19(29), xEntryTimeSet_44(30)>
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _10 ={v} pxQueue_33->cRxLock;
  if (_10 == -1)
    goto <bb 32>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 32> :
  pxQueue_33->cRxLock ={v} 0;

  <bb 33> :
  _11 ={v} pxQueue_33->cTxLock;
  if (_11 == -1)
    goto <bb 34>; [INV]
  else
    goto <bb 35>; [INV]

  <bb 34> :
  pxQueue_33->cTxLock ={v} 0;

  <bb 35> :
  vPortExitCritical ();
  _12 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_12 == 0)
    goto <bb 36>; [INV]
  else
    goto <bb 40>; [INV]

  <bb 36> :
  _13 = prvIsQueueEmpty (pxQueue_33);
  if (_13 != 0)
    goto <bb 37>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 37> :
  _14 = &pxQueue_33->xTasksWaitingToReceive;
  xTicksToWait.15_15 = xTicksToWait;
  vTaskPlaceOnEventList (_14, xTicksToWait.15_15);
  prvUnlockQueue (pxQueue_33);
  _16 = xTaskResumeAll ();
  if (_16 == 0)
    goto <bb 38>; [INV]
  else
    goto <bb 42>; [INV]

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

  <bb 39> :
  prvUnlockQueue (pxQueue_33);
  xTaskResumeAll ();
  goto <bb 42>; [INV]

  <bb 40> :
  prvUnlockQueue (pxQueue_33);
  xTaskResumeAll ();
  _18 = prvIsQueueEmpty (pxQueue_33);
  if (_18 != 0)
    goto <bb 41>; [INV]
  else
    goto <bb 42>; [INV]

  <bb 41> :
  _55 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 43>; [INV]

  <bb 42> :
  goto <bb 22>; [INV]

  <bb 43> :
  # _23 = PHI <_74(26), _66(28), _55(41)>
  xTimeOut ={v} {CLOBBER};

  <bb 44> :
<L47>:
  return _23;

}


xQueueGiveFromISR (struct QueueDefinition * xQueue, BaseType_t * const pxHigherPriorityTaskWoken)
{
  uint32_t ulNewMaskValue;
  uint32_t ulNewBASEPRI;
  uint32_t D.7329;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.7328;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  const int8_t cTxLock;
  const UBaseType_t uxMessagesWaiting;
  struct Queue_t * const pxQueue;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  BaseType_t D.6968;
  int iftmp.9;
  long unsigned int _1;
  int8_t * _2;
  struct tskTaskControlBlock * _3;
  long unsigned int _4;
  long unsigned int _5;
  long unsigned int _6;
  struct List_t * _7;
  long int _8;
  unsigned char cTxLock.10_9;
  unsigned char _10;
  signed char _11;
  int iftmp.9_13;
  int iftmp.9_19;
  int iftmp.9_20;
  BaseType_t _32;
  long unsigned int _38;

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

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

  <bb 4> :

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

  <bb 6> :
  _1 = pxQueue_17->uxItemSize;
  if (_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_34 : "i" 16 : "memory");

  <bb 8> :

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

  <bb 10> :
  _2 = pxQueue_17->pcHead;
  if (_2 != 0B)
    goto <bb 12>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 11> :
  _3 = pxQueue_17->u.xSemaphore.xMutexHolder;
  if (_3 == 0B)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  iftmp.9_20 = 1;
  goto <bb 14>; [INV]

  <bb 13> :
  iftmp.9_19 = 0;

  <bb 14> :
  # iftmp.9_13 = PHI <iftmp.9_20(12), iftmp.9_19(13)>
  if (iftmp.9_13 == 0)
    goto <bb 15>; [INV]
  else
    goto <bb 18>; [INV]

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

  <bb 16> :

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

  <bb 18> :
  vPortValidateInterruptPriority ();
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_36, "=r" ulNewBASEPRI_37 : "i" 16 : "memory");
  _38 = ulOriginalBASEPRI_36;

  <bb 19> :
<L32>:
  _42 = _38;

  <bb 20> :
  uxSavedInterruptStatus_22 = _42;
  uxMessagesWaiting_23 ={v} pxQueue_17->uxMessagesWaiting;
  _4 = pxQueue_17->uxLength;
  if (uxMessagesWaiting_23 < _4)
    goto <bb 21>; [INV]
  else
    goto <bb 32>; [INV]

  <bb 21> :
  cTxLock_25 ={v} pxQueue_17->cTxLock;
  _5 = uxMessagesWaiting_23 + 1;
  pxQueue_17->uxMessagesWaiting ={v} _5;
  if (cTxLock_25 == -1)
    goto <bb 22>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 22> :
  _6 ={v} pxQueue_17->xTasksWaitingToReceive.uxNumberOfItems;
  if (_6 != 0)
    goto <bb 23>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 23> :
  _7 = &pxQueue_17->xTasksWaitingToReceive;
  _8 = xTaskRemoveFromEventList (_7);
  if (_8 != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 24> :
  if (pxHigherPriorityTaskWoken_29(D) != 0B)
    goto <bb 25>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 25> :
  *pxHigherPriorityTaskWoken_29(D) = 1;
  goto <bb 31>; [INV]

  <bb 26> :
  if (cTxLock_25 == 127)
    goto <bb 27>; [INV]
  else
    goto <bb 30>; [INV]

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

  <bb 28> :

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

  <bb 30> :
  cTxLock.10_9 = (unsigned char) cTxLock_25;
  _10 = cTxLock.10_9 + 1;
  _11 = (signed char) _10;
  pxQueue_17->cTxLock ={v} _11;

  <bb 31> :
  xReturn_31 = 1;
  goto <bb 33>; [INV]

  <bb 32> :
  xReturn_24 = 0;

  <bb 33> :
  # xReturn_12 = PHI <xReturn_31(31), xReturn_24(32)>
  ulNewMaskValue_40 = uxSavedInterruptStatus_22;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_40 : "memory");

  <bb 34> :
  _32 = xReturn_12;

  <bb 35> :
<L31>:
  return _32;

}


xQueueGenericSendFromISR (struct QueueDefinition * xQueue, const void * const pvItemToQueue, BaseType_t * const pxHigherPriorityTaskWoken, const BaseType_t xCopyPosition)
{
  uint32_t ulNewMaskValue;
  uint32_t ulNewBASEPRI;
  uint32_t D.7342;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.7341;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  const UBaseType_t uxPreviousMessagesWaiting;
  const int8_t cTxLock;
  struct Queue_t * const pxQueue;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  BaseType_t D.6936;
  int iftmp.7;
  int iftmp.6;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  struct List_t * _6;
  long int _7;
  unsigned char cTxLock.8_8;
  unsigned char _9;
  signed char _10;
  int iftmp.6_12;
  int iftmp.7_13;
  int iftmp.6_20;
  int iftmp.6_21;
  int iftmp.7_23;
  int iftmp.7_24;
  BaseType_t _36;
  long unsigned int _42;

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

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

  <bb 4> :

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

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

  <bb 7> :
  _1 = pxQueue_17->uxItemSize;
  if (_1 == 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_12 = PHI <iftmp.6_21(8), iftmp.6_20(9)>
  if (iftmp.6_12 == 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 12> :

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

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

  <bb 15> :
  _2 = pxQueue_17->uxLength;
  if (_2 == 1)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  iftmp.7_24 = 1;
  goto <bb 18>; [INV]

  <bb 17> :
  iftmp.7_23 = 0;

  <bb 18> :
  # iftmp.7_13 = PHI <iftmp.7_24(16), iftmp.7_23(17)>
  if (iftmp.7_13 == 0)
    goto <bb 19>; [INV]
  else
    goto <bb 22>; [INV]

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

  <bb 20> :

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

  <bb 22> :
  vPortValidateInterruptPriority ();
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_40, "=r" ulNewBASEPRI_41 : "i" 16 : "memory");
  _42 = ulOriginalBASEPRI_40;

  <bb 23> :
<L37>:
  _46 = _42;

  <bb 24> :
  uxSavedInterruptStatus_26 = _46;
  _3 ={v} pxQueue_17->uxMessagesWaiting;
  _4 = pxQueue_17->uxLength;
  if (_3 < _4)
    goto <bb 26>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 25> :
  if (xCopyPosition_22(D) == 2)
    goto <bb 26>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 26> :
  cTxLock_28 ={v} pxQueue_17->cTxLock;
  uxPreviousMessagesWaiting_29 ={v} pxQueue_17->uxMessagesWaiting;
  prvCopyDataToQueue (pxQueue_17, pvItemToQueue_18(D), xCopyPosition_22(D));
  if (cTxLock_28 == -1)
    goto <bb 27>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 27> :
  _5 ={v} pxQueue_17->xTasksWaitingToReceive.uxNumberOfItems;
  if (_5 != 0)
    goto <bb 28>; [INV]
  else
    goto <bb 36>; [INV]

  <bb 28> :
  _6 = &pxQueue_17->xTasksWaitingToReceive;
  _7 = xTaskRemoveFromEventList (_6);
  if (_7 != 0)
    goto <bb 29>; [INV]
  else
    goto <bb 36>; [INV]

  <bb 29> :
  if (pxHigherPriorityTaskWoken_33(D) != 0B)
    goto <bb 30>; [INV]
  else
    goto <bb 36>; [INV]

  <bb 30> :
  *pxHigherPriorityTaskWoken_33(D) = 1;
  goto <bb 36>; [INV]

  <bb 31> :
  if (cTxLock_28 == 127)
    goto <bb 32>; [INV]
  else
    goto <bb 35>; [INV]

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

  <bb 33> :

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

  <bb 35> :
  cTxLock.8_8 = (unsigned char) cTxLock_28;
  _9 = cTxLock.8_8 + 1;
  _10 = (signed char) _9;
  pxQueue_17->cTxLock ={v} _10;

  <bb 36> :
  xReturn_35 = 1;
  goto <bb 38>; [INV]

  <bb 37> :
  xReturn_27 = 0;

  <bb 38> :
  # xReturn_11 = PHI <xReturn_35(36), xReturn_27(37)>
  ulNewMaskValue_44 = uxSavedInterruptStatus_26;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_44 : "memory");

  <bb 39> :
  _36 = xReturn_11;

  <bb 40> :
<L36>:
  return _36;

}


xQueueGenericSend (struct QueueDefinition * xQueue, const void * const pvItemToQueue, TickType_t xTicksToWait, const BaseType_t xCopyPosition)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxQueue;
  struct TimeOut_t xTimeOut;
  BaseType_t xYieldRequired;
  BaseType_t xEntryTimeSet;
  BaseType_t D.6882;
  int iftmp.2;
  int iftmp.1;
  int iftmp.0;
  long unsigned int _1;
  long unsigned int _2;
  long int _3;
  long unsigned int xTicksToWait.3_4;
  long unsigned int _5;
  long unsigned int _6;
  long unsigned int _7;
  struct List_t * _8;
  long int _9;
  volatile uint32_t * _10;
  volatile uint32_t * _11;
  long unsigned int xTicksToWait.4_12;
  signed char _13;
  signed char _14;
  long int _15;
  long int _16;
  struct List_t * _17;
  long unsigned int xTicksToWait.5_18;
  long int _19;
  volatile uint32_t * _20;
  int iftmp.0_23;
  int iftmp.1_24;
  int iftmp.2_25;
  BaseType_t _26;
  int iftmp.0_39;
  int iftmp.0_40;
  int iftmp.1_42;
  int iftmp.1_43;
  int iftmp.2_45;
  int iftmp.2_46;
  BaseType_t _59;
  BaseType_t _70;
  BaseType_t _81;

  <bb 2> :
  xEntryTimeSet_34 = 0;
  pxQueue_36 = xQueue_35(D);
  if (pxQueue_36 == 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> :
  if (pvItemToQueue_37(D) != 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 7> :
  _1 = pxQueue_36->uxItemSize;
  if (_1 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  iftmp.0_40 = 1;
  goto <bb 10>; [INV]

  <bb 9> :
  iftmp.0_39 = 0;

  <bb 10> :
  # iftmp.0_23 = PHI <iftmp.0_40(8), iftmp.0_39(9)>
  if (iftmp.0_23 == 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 12> :

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

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

  <bb 15> :
  _2 = pxQueue_36->uxLength;
  if (_2 == 1)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  iftmp.1_43 = 1;
  goto <bb 18>; [INV]

  <bb 17> :
  iftmp.1_42 = 0;

  <bb 18> :
  # iftmp.1_24 = PHI <iftmp.1_43(16), iftmp.1_42(17)>
  if (iftmp.1_24 == 0)
    goto <bb 19>; [INV]
  else
    goto <bb 22>; [INV]

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

  <bb 20> :

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

  <bb 22> :
  _3 = xTaskGetSchedulerState ();
  if (_3 != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 23> :
  xTicksToWait.3_4 = xTicksToWait;
  if (xTicksToWait.3_4 == 0)
    goto <bb 24>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 24> :
  iftmp.2_46 = 1;
  goto <bb 26>; [INV]

  <bb 25> :
  iftmp.2_45 = 0;

  <bb 26> :
  # iftmp.2_25 = PHI <iftmp.2_46(24), iftmp.2_45(25)>
  if (iftmp.2_25 == 0)
    goto <bb 27>; [INV]
  else
    goto <bb 30>; [INV]

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

  <bb 28> :

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

  <bb 30> :
  # xEntryTimeSet_21 = PHI <xEntryTimeSet_34(26), xEntryTimeSet_22(52)>
  vPortEnterCritical ();
  _5 ={v} pxQueue_36->uxMessagesWaiting;
  _6 = pxQueue_36->uxLength;
  if (_5 < _6)
    goto <bb 32>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 31> :
  if (xCopyPosition_41(D) == 2)
    goto <bb 32>; [INV]
  else
    goto <bb 38>; [INV]

  <bb 32> :
  xYieldRequired_72 = prvCopyDataToQueue (pxQueue_36, pvItemToQueue_37(D), xCopyPosition_41(D));
  _7 ={v} pxQueue_36->xTasksWaitingToReceive.uxNumberOfItems;
  if (_7 != 0)
    goto <bb 33>; [INV]
  else
    goto <bb 35>; [INV]

  <bb 33> :
  _8 = &pxQueue_36->xTasksWaitingToReceive;
  _9 = xTaskRemoveFromEventList (_8);
  if (_9 != 0)
    goto <bb 34>; [INV]
  else
    goto <bb 37>; [INV]

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

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

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

  <bb 37> :
  vPortExitCritical ();
  _81 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 53>; [INV]

  <bb 38> :
  xTicksToWait.4_12 = xTicksToWait;
  if (xTicksToWait.4_12 == 0)
    goto <bb 39>; [INV]
  else
    goto <bb 40>; [INV]

  <bb 39> :
  vPortExitCritical ();
  _70 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 53>; [INV]

  <bb 40> :
  if (xEntryTimeSet_21 == 0)
    goto <bb 41>; [INV]
  else
    goto <bb 42>; [INV]

  <bb 41> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet_49 = 1;

  <bb 42> :
  # xEntryTimeSet_22 = PHI <xEntryTimeSet_21(40), xEntryTimeSet_49(41)>
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _13 ={v} pxQueue_36->cRxLock;
  if (_13 == -1)
    goto <bb 43>; [INV]
  else
    goto <bb 44>; [INV]

  <bb 43> :
  pxQueue_36->cRxLock ={v} 0;

  <bb 44> :
  _14 ={v} pxQueue_36->cTxLock;
  if (_14 == -1)
    goto <bb 45>; [INV]
  else
    goto <bb 46>; [INV]

  <bb 45> :
  pxQueue_36->cTxLock ={v} 0;

  <bb 46> :
  vPortExitCritical ();
  _15 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_15 == 0)
    goto <bb 47>; [INV]
  else
    goto <bb 51>; [INV]

  <bb 47> :
  _16 = prvIsQueueFull (pxQueue_36);
  if (_16 != 0)
    goto <bb 48>; [INV]
  else
    goto <bb 50>; [INV]

  <bb 48> :
  _17 = &pxQueue_36->xTasksWaitingToSend;
  xTicksToWait.5_18 = xTicksToWait;
  vTaskPlaceOnEventList (_17, xTicksToWait.5_18);
  prvUnlockQueue (pxQueue_36);
  _19 = xTaskResumeAll ();
  if (_19 == 0)
    goto <bb 49>; [INV]
  else
    goto <bb 52>; [INV]

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

  <bb 50> :
  prvUnlockQueue (pxQueue_36);
  xTaskResumeAll ();
  goto <bb 52>; [INV]

  <bb 51> :
  prvUnlockQueue (pxQueue_36);
  xTaskResumeAll ();
  _59 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 53>; [INV]

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

  <bb 53> :
  # _26 = PHI <_81(37), _70(39), _59(51)>
  xTimeOut ={v} {CLOBBER};

  <bb 54> :
<L55>:
  return _26;

}


xQueueCreateCountingSemaphore (const UBaseType_t uxMaxCount, const UBaseType_t uxInitialCount)
{
  uint32_t ulNewBASEPRI;
  struct QueueDefinition * xHandle;
  struct QueueDefinition * D.6845;
  struct QueueDefinition * _11;

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

  <bb 3> :
  if (uxInitialCount_6(D) <= uxMaxCount_5(D))
    goto <bb 4>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 4> :
  xHandle_9 = xQueueGenericCreate (uxMaxCount_5(D), 0, 2);
  if (xHandle_9 != 0B)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 5> :
  MEM[(struct Queue_t *)xHandle_9].uxMessagesWaiting ={v} uxInitialCount_6(D);

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

  <bb 7> :
  if (xHandle_4 == 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 11>; [INV]

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

  <bb 9> :

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

  <bb 11> :
  # xHandle_1 = PHI <xHandle_9(6), xHandle_4(7)>
  _11 = xHandle_1;

  <bb 12> :
<L10>:
  return _11;

}


xQueueTakeMutexRecursive (struct QueueDefinition * xMutex, TickType_t xTicksToWait)
{
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxMutex;
  BaseType_t xReturn;
  BaseType_t D.6834;
  struct tskTaskControlBlock * _1;
  struct tskTaskControlBlock * _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  long unsigned int _6;
  BaseType_t _19;

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

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

  <bb 4> :

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

  <bb 6> :
  _1 = pxMutex_10->u.xSemaphore.xMutexHolder;
  _2 = xTaskGetCurrentTaskHandle ();
  if (_1 == _2)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  _3 = pxMutex_10->u.xSemaphore.uxRecursiveCallCount;
  _4 = _3 + 1;
  pxMutex_10->u.xSemaphore.uxRecursiveCallCount = _4;
  xReturn_18 = 1;
  goto <bb 10>; [INV]

  <bb 8> :
  xReturn_15 = xQueueSemaphoreTake (pxMutex_10, xTicksToWait_13(D));
  if (xReturn_15 != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  _5 = pxMutex_10->u.xSemaphore.uxRecursiveCallCount;
  _6 = _5 + 1;
  pxMutex_10->u.xSemaphore.uxRecursiveCallCount = _6;

  <bb 10> :
  # xReturn_7 = PHI <xReturn_18(7), xReturn_15(8), xReturn_15(9)>
  _19 = xReturn_7;

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

}


xQueueGiveMutexRecursive (struct QueueDefinition * xMutex)
{
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxMutex;
  BaseType_t xReturn;
  BaseType_t D.6824;
  struct tskTaskControlBlock * _1;
  struct tskTaskControlBlock * _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  BaseType_t _17;

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

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

  <bb 4> :

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

  <bb 6> :
  _1 = pxMutex_10->u.xSemaphore.xMutexHolder;
  _2 = xTaskGetCurrentTaskHandle ();
  if (_1 == _2)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 7> :
  _3 = pxMutex_10->u.xSemaphore.uxRecursiveCallCount;
  _4 = _3 + 4294967295;
  pxMutex_10->u.xSemaphore.uxRecursiveCallCount = _4;
  _5 = pxMutex_10->u.xSemaphore.uxRecursiveCallCount;
  if (_5 == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  xQueueGenericSend (pxMutex_10, 0B, 0, 0);

  <bb 9> :
  xReturn_16 = 1;
  goto <bb 11>; [INV]

  <bb 10> :
  xReturn_13 = 0;

  <bb 11> :
  # xReturn_6 = PHI <xReturn_16(9), xReturn_13(10)>
  _17 = xReturn_6;

  <bb 12> :
<L9>:
  return _17;

}


xQueueGetMutexHolderFromISR (struct QueueDefinition * xSemaphore)
{
  uint32_t ulNewBASEPRI;
  struct tskTaskControlBlock * pxReturn;
  struct tskTaskControlBlock * D.6814;
  int8_t * _1;
  struct tskTaskControlBlock * _7;

  <bb 2> :
  if (xSemaphore_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> :
  _1 = MEM[(struct Queue_t *)xSemaphore_3(D)].pcHead;
  if (_1 == 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  pxReturn_6 = MEM[(struct Queue_t *)xSemaphore_3(D)].u.xSemaphore.xMutexHolder;
  goto <bb 9>; [INV]

  <bb 8> :
  pxReturn_5 = 0B;

  <bb 9> :
  # pxReturn_2 = PHI <pxReturn_6(7), pxReturn_5(8)>
  _7 = pxReturn_2;

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

}


xQueueGetMutexHolder (struct QueueDefinition * xSemaphore)
{
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxSemaphore;
  struct tskTaskControlBlock * pxReturn;
  struct tskTaskControlBlock * D.6807;
  int8_t * _1;
  struct tskTaskControlBlock * _10;

  <bb 2> :
  pxSemaphore_4 = xSemaphore_3(D);
  if (xSemaphore_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_11 : "i" 16 : "memory");

  <bb 4> :

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

  <bb 6> :
  vPortEnterCritical ();
  _1 = pxSemaphore_4->pcHead;
  if (_1 == 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  pxReturn_8 = pxSemaphore_4->u.xSemaphore.xMutexHolder;
  goto <bb 9>; [INV]

  <bb 8> :
  pxReturn_7 = 0B;

  <bb 9> :
  # pxReturn_2 = PHI <pxReturn_8(7), pxReturn_7(8)>
  vPortExitCritical ();
  _10 = pxReturn_2;

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

}


xQueueCreateMutex (const uint8_t ucQueueType)
{
  const UBaseType_t uxMutexSize;
  const UBaseType_t uxMutexLength;
  struct QueueDefinition * xNewQueue;
  struct QueueDefinition * D.6800;
  struct QueueDefinition * _8;

  <bb 2> :
  uxMutexLength_1 = 1;
  uxMutexSize_2 = 0;
  xNewQueue_6 = xQueueGenericCreate (uxMutexLength_1, uxMutexSize_2, ucQueueType_4(D));
  prvInitialiseMutex (xNewQueue_6);
  _8 = xNewQueue_6;

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

}


prvInitialiseMutex (struct Queue_t * pxNewQueue)
{
  <bb 2> :
  if (pxNewQueue_2(D) != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  pxNewQueue_2(D)->u.xSemaphore.xMutexHolder = 0B;
  pxNewQueue_2(D)->pcHead = 0B;
  pxNewQueue_2(D)->u.xSemaphore.uxRecursiveCallCount = 0;
  xQueueGenericSend (pxNewQueue_2(D), 0B, 0, 0);

  <bb 4> :
  return;

}


prvInitialiseNewQueue (const UBaseType_t uxQueueLength, const UBaseType_t uxItemSize, uint8_t * pucQueueStorage, const uint8_t ucQueueType, struct Queue_t * pxNewQueue)
{
  <bb 2> :
  if (uxItemSize_2(D) == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  pxNewQueue_4(D)->pcHead = pxNewQueue_4(D);
  goto <bb 5>; [INV]

  <bb 4> :
  pxNewQueue_4(D)->pcHead = pucQueueStorage_5(D);

  <bb 5> :
  pxNewQueue_4(D)->uxLength = uxQueueLength_8(D);
  pxNewQueue_4(D)->uxItemSize = uxItemSize_2(D);
  xQueueGenericReset (pxNewQueue_4(D), 1);
  pxNewQueue_4(D)->ucQueueType = ucQueueType_12(D);
  return;

}


xQueueGenericCreate (const UBaseType_t uxQueueLength, const UBaseType_t uxItemSize, const uint8_t ucQueueType)
{
  uint32_t ulNewBASEPRI;
  uint8_t * pucQueueStorage;
  size_t xQueueSizeInBytes;
  struct Queue_t * pxNewQueue;
  struct QueueDefinition * D.6792;
  __complex__ long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  unsigned int _4;
  struct QueueDefinition * _19;

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

  <bb 3> :
  _1 = .MUL_OVERFLOW (uxItemSize_10(D), uxQueueLength_9(D));
  _2 = IMAGPART_EXPR <_1>;
  if (_2 == 0)
    goto <bb 4>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 4> :
  _3 = uxQueueLength_9(D) * uxItemSize_10(D);
  if (_3 <= 4294967215)
    goto <bb 5>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 5> :
  xQueueSizeInBytes_11 = uxQueueLength_9(D) * uxItemSize_10(D);
  _4 = xQueueSizeInBytes_11 + 80;
  pxNewQueue_14 = pvPortMalloc (_4);
  if (pxNewQueue_14 != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  pucQueueStorage_15 = pxNewQueue_14;
  pucQueueStorage_16 = pucQueueStorage_15 + 80;
  prvInitialiseNewQueue (uxQueueLength_9(D), uxItemSize_10(D), pucQueueStorage_16, ucQueueType_17(D), pxNewQueue_14);

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

  <bb 8> :
  if (pxNewQueue_8 == 0B)
    goto <bb 9>; [INV]
  else
    goto <bb 12>; [INV]

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

  <bb 10> :

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

  <bb 12> :
  # pxNewQueue_5 = PHI <pxNewQueue_14(7), pxNewQueue_8(8)>
  _19 = pxNewQueue_5;

  <bb 13> :
<L11>:
  return _19;

}


xQueueGenericReset (struct QueueDefinition * xQueue, BaseType_t xNewQueue)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  BaseType_t D.6780;
  long unsigned int _1;
  __complex__ long unsigned int _2;
  long unsigned int _3;
  long unsigned int _4;
  long unsigned int _5;
  int8_t * _6;
  long unsigned int _7;
  long unsigned int _8;
  long unsigned int _9;
  int8_t * _10;
  int8_t * _11;
  int8_t * _12;
  long unsigned int _13;
  long unsigned int _14;
  long unsigned int _15;
  long unsigned int _16;
  int8_t * _17;
  long unsigned int _18;
  struct List_t * _19;
  long int _20;
  volatile uint32_t * _21;
  struct List_t * _22;
  struct List_t * _23;
  BaseType_t _47;

  <bb 2> :
  xReturn_27 = 1;
  pxQueue_29 = xQueue_28(D);
  if (pxQueue_29 == 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> :
  if (pxQueue_29 != 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 7> :
  _1 = pxQueue_29->uxLength;
  if (_1 != 0)
    goto <bb 8>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 8> :
  _3 = pxQueue_29->uxItemSize;
  _4 = pxQueue_29->uxLength;
  _2 = .MUL_OVERFLOW (_3, _4);
  _5 = IMAGPART_EXPR <_2>;
  if (_5 == 0)
    goto <bb 9>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 9> :
  vPortEnterCritical ();
  _6 = pxQueue_29->pcHead;
  _7 = pxQueue_29->uxLength;
  _8 = pxQueue_29->uxItemSize;
  _9 = _7 * _8;
  _10 = _6 + _9;
  pxQueue_29->u.xQueue.pcTail = _10;
  pxQueue_29->uxMessagesWaiting ={v} 0;
  _11 = pxQueue_29->pcHead;
  pxQueue_29->pcWriteTo = _11;
  _12 = pxQueue_29->pcHead;
  _13 = pxQueue_29->uxLength;
  _14 = _13 + 4294967295;
  _15 = pxQueue_29->uxItemSize;
  _16 = _14 * _15;
  _17 = _12 + _16;
  pxQueue_29->u.xQueue.pcReadFrom = _17;
  pxQueue_29->cRxLock ={v} -1;
  pxQueue_29->cTxLock ={v} -1;
  if (xNewQueue_38(D) == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 10> :
  _18 ={v} pxQueue_29->xTasksWaitingToSend.uxNumberOfItems;
  if (_18 != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 11> :
  _19 = &pxQueue_29->xTasksWaitingToSend;
  _20 = xTaskRemoveFromEventList (_19);
  if (_20 != 0)
    goto <bb 12>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 13> :
  _22 = &pxQueue_29->xTasksWaitingToSend;
  vListInitialise (_22);
  _23 = &pxQueue_29->xTasksWaitingToReceive;
  vListInitialise (_23);

  <bb 14> :
  vPortExitCritical ();
  goto <bb 16>; [INV]

  <bb 15> :
  xReturn_46 = 0;

  <bb 16> :
  # xReturn_24 = PHI <xReturn_27(14), xReturn_46(15)>
  if (xReturn_24 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 20>; [INV]

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

  <bb 18> :

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

  <bb 20> :
  _47 = xReturn_24;

  <bb 21> :
<L20>:
  return _47;

}