vQueueWaitForMessageRestricted (struct QueueDefinition * xQueue, TickType_t xTicksToWait, const BaseType_t xWaitIndefinitely)
{
  struct Queue_t * const pxQueue;

  <bb 2> :
  pxQueue = xQueue;
  vPortEnterCritical ();
  _1 = pxQueue->cRxLock;
  if (_1 == -1)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  pxQueue->cRxLock = 0;

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

  <bb 5> :
  pxQueue->cTxLock = 0;

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

  <bb 7> :
  _4 = &pxQueue->xTasksWaitingToReceive;
  vTaskPlaceOnEventListRestricted (_4, xTicksToWait, xWaitIndefinitely);

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

}


vQueueUnregisterQueue (struct QueueDefinition * xQueue)
{
  UBaseType_t ux;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  ux = 0;
  goto <bb 9>; [INV]

  <bb 6> :
  _1 = xQueueRegistry[ux].xHandle;
  if (xQueue == _1)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  xQueueRegistry[ux].pcQueueName = 0B;
  xQueueRegistry[ux].xHandle = 0B;
  goto <bb 10>; [INV]

  <bb 8> :
  ux = ux + 1;

  <bb 9> :
  if (ux <= 1)
    goto <bb 6>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 10> :
  return;

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  ux = 0;
  goto <bb 9>; [INV]

  <bb 6> :
  _1 = xQueueRegistry[ux].xHandle;
  if (xQueue == _1)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  pcReturn = xQueueRegistry[ux].pcQueueName;
  goto <bb 10>; [INV]

  <bb 8> :
  ux = ux + 1;

  <bb 9> :
  if (ux <= 1)
    goto <bb 6>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 10> :
  D.7264 = pcReturn;

  <bb 11> :
<L8>:
  return D.7264;

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  pxEntryToWrite = 0B;
  if (pcQueueName != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 6> :
  ux = 0;
  goto <bb 13>; [INV]

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

  <bb 8> :
  pxEntryToWrite = &xQueueRegistry[ux];
  goto <bb 14>; [INV]

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

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

  <bb 11> :
  pxEntryToWrite = &xQueueRegistry[ux];

  <bb 12> :
  ux = ux + 1;

  <bb 13> :
  if (ux <= 1)
    goto <bb 7>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 15> :
  pxEntryToWrite->pcQueueName = pcQueueName;
  pxEntryToWrite->xHandle = xQueue;

  <bb 16> :
  return;

}


xQueueIsQueueFullFromISR (struct QueueDefinition * const xQueue)
{
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  BaseType_t D.7245;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = pxQueue->uxMessagesWaiting;
  _2 = pxQueue->uxLength;
  if (_1 == _2)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  xReturn = 1;
  goto <bb 8>; [INV]

  <bb 7> :
  xReturn = 0;

  <bb 8> :
  D.7245 = xReturn;

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

}


prvIsQueueFull (const struct Queue_t * pxQueue)
{
  BaseType_t xReturn;
  BaseType_t D.7238;

  <bb 2> :
  vPortEnterCritical ();
  _1 = pxQueue->uxMessagesWaiting;
  _2 = pxQueue->uxLength;
  if (_1 == _2)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

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

  <bb 4> :
  xReturn = 0;

  <bb 5> :
  vPortExitCritical ();
  D.7238 = xReturn;

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

}


xQueueIsQueueEmptyFromISR (struct QueueDefinition * const xQueue)
{
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  BaseType_t D.7233;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = pxQueue->uxMessagesWaiting;
  if (_1 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  xReturn = 1;
  goto <bb 8>; [INV]

  <bb 7> :
  xReturn = 0;

  <bb 8> :
  D.7233 = xReturn;

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

}


prvIsQueueEmpty (const struct Queue_t * pxQueue)
{
  BaseType_t xReturn;
  BaseType_t D.7226;

  <bb 2> :
  vPortEnterCritical ();
  _1 = pxQueue->uxMessagesWaiting;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

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

  <bb 4> :
  xReturn = 0;

  <bb 5> :
  vPortExitCritical ();
  D.7226 = xReturn;

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

}


prvUnlockQueue (struct Queue_t * const pxQueue)
{
  int8_t cRxLock;
  int8_t cTxLock;

  <bb 2> :
  vPortEnterCritical ();
  cTxLock = pxQueue->cTxLock;
  goto <bb 8>; [INV]

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

  <bb 4> :
  _2 = &pxQueue->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;
  _5 = cTxLock.28_4 + 255;
  cTxLock = (int8_t) _5;

  <bb 8> :
  if (cTxLock > 0)
    goto <bb 3>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 9> :
  pxQueue->cTxLock = -1;
  vPortExitCritical ();
  vPortEnterCritical ();
  cRxLock = pxQueue->cRxLock;
  goto <bb 15>; [INV]

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

  <bb 11> :
  _7 = &pxQueue->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;
  _10 = cRxLock.29_9 + 255;
  cRxLock = (int8_t) _10;
  goto <bb 15>; [INV]

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

  <bb 15> :
  if (cRxLock > 0)
    goto <bb 10>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 16> :
  pxQueue->cRxLock = -1;
  vPortExitCritical ();
  return;

}


prvCopyDataFromQueue (struct Queue_t * const pxQueue, void * const pvBuffer)
{
  <bb 2> :
  _1 = pxQueue->uxItemSize;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :
  _7 = pxQueue->pcHead;
  pxQueue->u.xQueue.pcReadFrom = _7;

  <bb 5> :
  _8 = pxQueue->u.xQueue.pcReadFrom;
  _9 = pxQueue->uxItemSize;
  memcpy (pvBuffer, _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;

  <bb 2> :
  xReturn = 0;
  uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  _1 = pxQueue->uxItemSize;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

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

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

  <bb 7> :
  _11 = pxQueue->pcHead;
  pxQueue->pcWriteTo = _11;
  goto <bb 13>; [INV]

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

  <bb 9> :
  _20 = pxQueue->u.xQueue.pcTail;
  _21 = pxQueue->uxItemSize;
  _22 = -_21;
  _23 = _20 + _22;
  pxQueue->u.xQueue.pcReadFrom = _23;

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

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

  <bb 12> :
  uxMessagesWaiting = uxMessagesWaiting + 4294967295;

  <bb 13> :
  _24 = uxMessagesWaiting + 1;
  pxQueue->uxMessagesWaiting = _24;
  D.7204 = xReturn;

  <bb 14> :
<L21>:
  return D.7204;

}


prvGetDisinheritPriorityAfterTimeout (const struct Queue_t * const pxQueue)
{
  UBaseType_t uxHighestPriorityOfWaitingTasks;
  UBaseType_t D.7181;

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

  <bb 3> :
  _2 = pxQueue->xTasksWaitingToReceive.xListEnd.pxNext;
  _3 = _2->xItemValue;
  uxHighestPriorityOfWaitingTasks = 5 - _3;
  goto <bb 5>; [INV]

  <bb 4> :
  uxHighestPriorityOfWaitingTasks = 0;

  <bb 5> :
  D.7181 = uxHighestPriorityOfWaitingTasks;

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

}


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

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

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

}


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

}


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

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

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

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  vQueueUnregisterQueue (pxQueue);
  vPortFree (pxQueue);
  return;

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  uxReturn = pxQueue->uxMessagesWaiting;
  D.7170 = uxReturn;

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

}


uxQueueSpacesAvailable (struct QueueDefinition * const xQueue)
{
  struct Queue_t * const pxQueue;
  UBaseType_t uxReturn;
  UBaseType_t D.7166;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  vPortEnterCritical ();
  _1 = pxQueue->uxLength;
  _2 = pxQueue->uxMessagesWaiting;
  uxReturn = _1 - _2;
  vPortExitCritical ();
  D.7166 = uxReturn;

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

}


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

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  vPortEnterCritical ();
  uxReturn = MEM[(struct Queue_t *)xQueue].uxMessagesWaiting;
  vPortExitCritical ();
  D.7162 = uxReturn;

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

}


xQueuePeekFromISR (struct QueueDefinition * xQueue, void * const pvBuffer)
{
  struct Queue_t * const pxQueue;
  int8_t * pcOriginalReadPosition;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  BaseType_t D.7158;
  int iftmp.27;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

  <bb 7> :
  iftmp.27 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.27 = 0;

  <bb 9> :
  if (iftmp.27 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

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

  <bb 12> :
  _2 = pxQueue->uxItemSize;
  if (_2 == 0)
    goto <bb 13>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 13> :
  vPortRaiseBASEPRI ();

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

  <bb 15> :
  vPortValidateInterruptPriority ();
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  _3 = pxQueue->uxMessagesWaiting;
  if (_3 != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  pcOriginalReadPosition = pxQueue->u.xQueue.pcReadFrom;
  prvCopyDataFromQueue (pxQueue, pvBuffer);
  pxQueue->u.xQueue.pcReadFrom = pcOriginalReadPosition;
  xReturn = 1;
  goto <bb 18>; [INV]

  <bb 17> :
  xReturn = 0;

  <bb 18> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.7158 = xReturn;

  <bb 19> :
<L16>:
  return D.7158;

}


xQueueReceiveFromISR (struct QueueDefinition * xQueue, void * const pvBuffer, BaseType_t * const pxHigherPriorityTaskWoken)
{
  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;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

  <bb 7> :
  iftmp.25 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.25 = 0;

  <bb 9> :
  if (iftmp.25 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

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

  <bb 12> :
  vPortValidateInterruptPriority ();
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  if (uxMessagesWaiting != 0)
    goto <bb 13>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 13> :
  cRxLock = pxQueue->cRxLock;
  prvCopyDataFromQueue (pxQueue, pvBuffer);
  _2 = uxMessagesWaiting + 4294967295;
  pxQueue->uxMessagesWaiting = _2;
  if (cRxLock == -1)
    goto <bb 14>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 14> :
  _3 = pxQueue->xTasksWaitingToSend.uxNumberOfItems;
  if (_3 != 0)
    goto <bb 15>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 15> :
  _4 = &pxQueue->xTasksWaitingToSend;
  _5 = xTaskRemoveFromEventList (_4);
  if (_5 != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 22>; [INV]

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

  <bb 17> :
  *pxHigherPriorityTaskWoken = 1;
  goto <bb 22>; [INV]

  <bb 18> :
  if (cRxLock == 127)
    goto <bb 19>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 19> :
  vPortRaiseBASEPRI ();

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

  <bb 21> :
  cRxLock.26_6 = (unsigned char) cRxLock;
  _7 = cRxLock.26_6 + 1;
  _8 = (signed char) _7;
  pxQueue->cRxLock = _8;

  <bb 22> :
  xReturn = 1;
  goto <bb 24>; [INV]

  <bb 23> :
  xReturn = 0;

  <bb 24> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.7142 = xReturn;

  <bb 25> :
<L28>:
  return D.7142;

}


xQueuePeek (struct QueueDefinition * xQueue, void * const pvBuffer, TickType_t xTicksToWait)
{
  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;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

  <bb 7> :
  iftmp.20 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.20 = 0;

  <bb 9> :
  if (iftmp.20 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

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

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

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

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

  <bb 15> :
  iftmp.21 = 0;

  <bb 16> :
  if (iftmp.21 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 17> :
  vPortRaiseBASEPRI ();

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

  <bb 19> :
  vPortEnterCritical ();
  uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  if (uxMessagesWaiting != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 20> :
  pcOriginalReadPosition = pxQueue->u.xQueue.pcReadFrom;
  prvCopyDataFromQueue (pxQueue, pvBuffer);
  pxQueue->u.xQueue.pcReadFrom = pcOriginalReadPosition;
  _4 = pxQueue->xTasksWaitingToReceive.uxNumberOfItems;
  if (_4 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 21> :
  _5 = &pxQueue->xTasksWaitingToReceive;
  _6 = xTaskRemoveFromEventList (_5);
  if (_6 != 0)
    goto <bb 22>; [INV]
  else
    goto <bb 23>; [INV]

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

  <bb 23> :
  vPortExitCritical ();
  D.7093 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

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

  <bb 25> :
  vPortExitCritical ();
  D.7093 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

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

  <bb 27> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet = 1;

  <bb 28> :
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _9 = pxQueue->cRxLock;
  if (_9 == -1)
    goto <bb 29>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 29> :
  pxQueue->cRxLock = 0;

  <bb 30> :
  _10 = pxQueue->cTxLock;
  if (_10 == -1)
    goto <bb 31>; [INV]
  else
    goto <bb 32>; [INV]

  <bb 31> :
  pxQueue->cTxLock = 0;

  <bb 32> :
  vPortExitCritical ();
  _11 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_11 == 0)
    goto <bb 33>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 33> :
  _12 = prvIsQueueEmpty (pxQueue);
  if (_12 != 0)
    goto <bb 34>; [INV]
  else
    goto <bb 36>; [INV]

  <bb 34> :
  _13 = &pxQueue->xTasksWaitingToReceive;
  xTicksToWait.24_14 = xTicksToWait;
  vTaskPlaceOnEventList (_13, xTicksToWait.24_14);
  prvUnlockQueue (pxQueue);
  _15 = xTaskResumeAll ();
  if (_15 == 0)
    goto <bb 35>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 35> :
  _16 = 3758157060B;
  *_16 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 39>; [INV]

  <bb 36> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  goto <bb 39>; [INV]

  <bb 37> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  _17 = prvIsQueueEmpty (pxQueue);
  if (_17 != 0)
    goto <bb 38>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 38> :
  D.7093 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

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

  <bb 40> :
  xTimeOut = {CLOBBER};

  <bb 41> :
<L47>:
  return D.7093;

}


xQueueSemaphoreTake (struct QueueDefinition * xQueue, TickType_t xTicksToWait)
{
  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;

  <bb 2> :
  xEntryTimeSet = 0;
  pxQueue = xQueue;
  xInheritanceOccurred = 0;
  if (pxQueue == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = pxQueue->uxItemSize;
  if (_1 != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  vPortRaiseBASEPRI ();

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

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

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

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

  <bb 11> :
  iftmp.16 = 0;

  <bb 12> :
  if (iftmp.16 == 0)
    goto <bb 13>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 13> :
  vPortRaiseBASEPRI ();

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

  <bb 15> :
  vPortEnterCritical ();
  uxSemaphoreCount = pxQueue->uxMessagesWaiting;
  if (uxSemaphoreCount != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 16> :
  _4 = uxSemaphoreCount + 4294967295;
  pxQueue->uxMessagesWaiting = _4;
  _5 = pxQueue->pcHead;
  if (_5 == 0B)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  _6 = pvTaskIncrementMutexHeldCount ();
  pxQueue->u.xSemaphore.xMutexHolder = _6;

  <bb 18> :
  _7 = pxQueue->xTasksWaitingToSend.uxNumberOfItems;
  if (_7 != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 19> :
  _8 = &pxQueue->xTasksWaitingToSend;
  _9 = xTaskRemoveFromEventList (_8);
  if (_9 != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 21>; [INV]

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

  <bb 21> :
  vPortExitCritical ();
  D.7039 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 45>; [INV]

  <bb 22> :
  xTicksToWait.18_11 = xTicksToWait;
  if (xTicksToWait.18_11 == 0)
    goto <bb 23>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 23> :
  if (xInheritanceOccurred != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 24> :
  vPortRaiseBASEPRI ();

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

  <bb 26> :
  vPortExitCritical ();
  D.7039 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 45>; [INV]

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

  <bb 28> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet = 1;

  <bb 29> :
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _12 = pxQueue->cRxLock;
  if (_12 == -1)
    goto <bb 30>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 30> :
  pxQueue->cRxLock = 0;

  <bb 31> :
  _13 = pxQueue->cTxLock;
  if (_13 == -1)
    goto <bb 32>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 32> :
  pxQueue->cTxLock = 0;

  <bb 33> :
  vPortExitCritical ();
  _14 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_14 == 0)
    goto <bb 34>; [INV]
  else
    goto <bb 40>; [INV]

  <bb 34> :
  _15 = prvIsQueueEmpty (pxQueue);
  if (_15 != 0)
    goto <bb 35>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 35> :
  _16 = pxQueue->pcHead;
  if (_16 == 0B)
    goto <bb 36>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 36> :
  vPortEnterCritical ();
  _17 = pxQueue->u.xSemaphore.xMutexHolder;
  xInheritanceOccurred = xTaskPriorityInherit (_17);
  vPortExitCritical ();

  <bb 37> :
  _18 = &pxQueue->xTasksWaitingToReceive;
  xTicksToWait.19_19 = xTicksToWait;
  vTaskPlaceOnEventList (_18, xTicksToWait.19_19);
  prvUnlockQueue (pxQueue);
  _20 = xTaskResumeAll ();
  if (_20 == 0)
    goto <bb 38>; [INV]
  else
    goto <bb 44>; [INV]

  <bb 38> :
  _21 = 3758157060B;
  *_21 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 44>; [INV]

  <bb 39> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  goto <bb 44>; [INV]

  <bb 40> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  _22 = prvIsQueueEmpty (pxQueue);
  if (_22 != 0)
    goto <bb 41>; [INV]
  else
    goto <bb 44>; [INV]

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

  <bb 42> :
  vPortEnterCritical ();
  uxHighestWaitingPriority = prvGetDisinheritPriorityAfterTimeout (pxQueue);
  _23 = pxQueue->u.xSemaphore.xMutexHolder;
  vTaskPriorityDisinheritAfterTimeout (_23, uxHighestWaitingPriority);
  vPortExitCritical ();

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

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

  <bb 45> :
  xTimeOut = {CLOBBER};

  <bb 46> :
<L54>:
  return D.7039;

}


xQueueReceive (struct QueueDefinition * xQueue, void * const pvBuffer, TickType_t xTicksToWait)
{
  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;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

  <bb 7> :
  iftmp.11 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.11 = 0;

  <bb 9> :
  if (iftmp.11 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

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

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

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

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

  <bb 15> :
  iftmp.12 = 0;

  <bb 16> :
  if (iftmp.12 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 17> :
  vPortRaiseBASEPRI ();

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

  <bb 19> :
  vPortEnterCritical ();
  uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  if (uxMessagesWaiting != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 20> :
  prvCopyDataFromQueue (pxQueue, pvBuffer);
  _4 = uxMessagesWaiting + 4294967295;
  pxQueue->uxMessagesWaiting = _4;
  _5 = pxQueue->xTasksWaitingToSend.uxNumberOfItems;
  if (_5 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 21> :
  _6 = &pxQueue->xTasksWaitingToSend;
  _7 = xTaskRemoveFromEventList (_6);
  if (_7 != 0)
    goto <bb 22>; [INV]
  else
    goto <bb 23>; [INV]

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

  <bb 23> :
  vPortExitCritical ();
  D.6994 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

  <bb 24> :
  xTicksToWait.14_9 = xTicksToWait;
  if (xTicksToWait.14_9 == 0)
    goto <bb 25>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 25> :
  vPortExitCritical ();
  D.6994 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

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

  <bb 27> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet = 1;

  <bb 28> :
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _10 = pxQueue->cRxLock;
  if (_10 == -1)
    goto <bb 29>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 29> :
  pxQueue->cRxLock = 0;

  <bb 30> :
  _11 = pxQueue->cTxLock;
  if (_11 == -1)
    goto <bb 31>; [INV]
  else
    goto <bb 32>; [INV]

  <bb 31> :
  pxQueue->cTxLock = 0;

  <bb 32> :
  vPortExitCritical ();
  _12 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_12 == 0)
    goto <bb 33>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 33> :
  _13 = prvIsQueueEmpty (pxQueue);
  if (_13 != 0)
    goto <bb 34>; [INV]
  else
    goto <bb 36>; [INV]

  <bb 34> :
  _14 = &pxQueue->xTasksWaitingToReceive;
  xTicksToWait.15_15 = xTicksToWait;
  vTaskPlaceOnEventList (_14, xTicksToWait.15_15);
  prvUnlockQueue (pxQueue);
  _16 = xTaskResumeAll ();
  if (_16 == 0)
    goto <bb 35>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 35> :
  _17 = 3758157060B;
  *_17 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 39>; [INV]

  <bb 36> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  goto <bb 39>; [INV]

  <bb 37> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  _18 = prvIsQueueEmpty (pxQueue);
  if (_18 != 0)
    goto <bb 38>; [INV]
  else
    goto <bb 39>; [INV]

  <bb 38> :
  D.6994 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 40>; [INV]

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

  <bb 40> :
  xTimeOut = {CLOBBER};

  <bb 41> :
<L47>:
  return D.6994;

}


xQueueGiveFromISR (struct QueueDefinition * xQueue, BaseType_t * const pxHigherPriorityTaskWoken)
{
  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;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = pxQueue->uxItemSize;
  if (_1 != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  vPortRaiseBASEPRI ();

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

  <bb 8> :
  _2 = pxQueue->pcHead;
  if (_2 != 0B)
    goto <bb 10>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 9> :
  _3 = pxQueue->u.xSemaphore.xMutexHolder;
  if (_3 == 0B)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

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

  <bb 11> :
  iftmp.9 = 0;

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

  <bb 13> :
  vPortRaiseBASEPRI ();

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

  <bb 15> :
  vPortValidateInterruptPriority ();
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  uxMessagesWaiting = pxQueue->uxMessagesWaiting;
  _4 = pxQueue->uxLength;
  if (uxMessagesWaiting < _4)
    goto <bb 16>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 16> :
  cTxLock = pxQueue->cTxLock;
  _5 = uxMessagesWaiting + 1;
  pxQueue->uxMessagesWaiting = _5;
  if (cTxLock == -1)
    goto <bb 17>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 17> :
  _6 = pxQueue->xTasksWaitingToReceive.uxNumberOfItems;
  if (_6 != 0)
    goto <bb 18>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 18> :
  _7 = &pxQueue->xTasksWaitingToReceive;
  _8 = xTaskRemoveFromEventList (_7);
  if (_8 != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 25>; [INV]

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

  <bb 20> :
  *pxHigherPriorityTaskWoken = 1;
  goto <bb 25>; [INV]

  <bb 21> :
  if (cTxLock == 127)
    goto <bb 22>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 22> :
  vPortRaiseBASEPRI ();

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

  <bb 24> :
  cTxLock.10_9 = (unsigned char) cTxLock;
  _10 = cTxLock.10_9 + 1;
  _11 = (signed char) _10;
  pxQueue->cTxLock = _11;

  <bb 25> :
  xReturn = 1;
  goto <bb 27>; [INV]

  <bb 26> :
  xReturn = 0;

  <bb 27> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.6968 = xReturn;

  <bb 28> :
<L31>:
  return D.6968;

}


xQueueGenericSendFromISR (struct QueueDefinition * xQueue, const void * const pvItemToQueue, BaseType_t * const pxHigherPriorityTaskWoken, const BaseType_t xCopyPosition)
{
  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;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

  <bb 7> :
  iftmp.6 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.6 = 0;

  <bb 9> :
  if (iftmp.6 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

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

  <bb 12> :
  if (xCopyPosition != 2)
    goto <bb 14>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 13> :
  _2 = pxQueue->uxLength;
  if (_2 == 1)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

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

  <bb 15> :
  iftmp.7 = 0;

  <bb 16> :
  if (iftmp.7 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 17> :
  vPortRaiseBASEPRI ();

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

  <bb 19> :
  vPortValidateInterruptPriority ();
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  _3 = pxQueue->uxMessagesWaiting;
  _4 = pxQueue->uxLength;
  if (_3 < _4)
    goto <bb 21>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 20> :
  if (xCopyPosition == 2)
    goto <bb 21>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 21> :
  cTxLock = pxQueue->cTxLock;
  uxPreviousMessagesWaiting = pxQueue->uxMessagesWaiting;
  prvCopyDataToQueue (pxQueue, pvItemToQueue, xCopyPosition);
  if (cTxLock == -1)
    goto <bb 22>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 22> :
  _5 = pxQueue->xTasksWaitingToReceive.uxNumberOfItems;
  if (_5 != 0)
    goto <bb 23>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 23> :
  _6 = &pxQueue->xTasksWaitingToReceive;
  _7 = xTaskRemoveFromEventList (_6);
  if (_7 != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 24> :
  if (pxHigherPriorityTaskWoken != 0B)
    goto <bb 25>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 25> :
  *pxHigherPriorityTaskWoken = 1;
  goto <bb 30>; [INV]

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

  <bb 27> :
  vPortRaiseBASEPRI ();

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

  <bb 29> :
  cTxLock.8_8 = (unsigned char) cTxLock;
  _9 = cTxLock.8_8 + 1;
  _10 = (signed char) _9;
  pxQueue->cTxLock = _10;

  <bb 30> :
  xReturn = 1;
  goto <bb 32>; [INV]

  <bb 31> :
  xReturn = 0;

  <bb 32> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.6936 = xReturn;

  <bb 33> :
<L36>:
  return D.6936;

}


xQueueGenericSend (struct QueueDefinition * xQueue, const void * const pvItemToQueue, TickType_t xTicksToWait, const BaseType_t xCopyPosition)
{
  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;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

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

  <bb 7> :
  iftmp.0 = 1;
  goto <bb 9>; [INV]

  <bb 8> :
  iftmp.0 = 0;

  <bb 9> :
  if (iftmp.0 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

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

  <bb 12> :
  if (xCopyPosition != 2)
    goto <bb 14>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 13> :
  _2 = pxQueue->uxLength;
  if (_2 == 1)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

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

  <bb 15> :
  iftmp.1 = 0;

  <bb 16> :
  if (iftmp.1 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 17> :
  vPortRaiseBASEPRI ();

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

  <bb 19> :
  _3 = xTaskGetSchedulerState ();
  if (_3 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 20> :
  xTicksToWait.3_4 = xTicksToWait;
  if (xTicksToWait.3_4 == 0)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  iftmp.2 = 1;
  goto <bb 23>; [INV]

  <bb 22> :
  iftmp.2 = 0;

  <bb 23> :
  if (iftmp.2 == 0)
    goto <bb 24>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 24> :
  vPortRaiseBASEPRI ();

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

  <bb 26> :
  vPortEnterCritical ();
  _5 = pxQueue->uxMessagesWaiting;
  _6 = pxQueue->uxLength;
  if (_5 < _6)
    goto <bb 28>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 27> :
  if (xCopyPosition == 2)
    goto <bb 28>; [INV]
  else
    goto <bb 34>; [INV]

  <bb 28> :
  xYieldRequired = prvCopyDataToQueue (pxQueue, pvItemToQueue, xCopyPosition);
  _7 = pxQueue->xTasksWaitingToReceive.uxNumberOfItems;
  if (_7 != 0)
    goto <bb 29>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 29> :
  _8 = &pxQueue->xTasksWaitingToReceive;
  _9 = xTaskRemoveFromEventList (_8);
  if (_9 != 0)
    goto <bb 30>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 30> :
  _10 = 3758157060B;
  *_10 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 33>; [INV]

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

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

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

  <bb 34> :
  xTicksToWait.4_12 = xTicksToWait;
  if (xTicksToWait.4_12 == 0)
    goto <bb 35>; [INV]
  else
    goto <bb 36>; [INV]

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

  <bb 36> :
  if (xEntryTimeSet == 0)
    goto <bb 37>; [INV]
  else
    goto <bb 38>; [INV]

  <bb 37> :
  vTaskInternalSetTimeOutState (&xTimeOut);
  xEntryTimeSet = 1;

  <bb 38> :
  vPortExitCritical ();
  vTaskSuspendAll ();
  vPortEnterCritical ();
  _13 = pxQueue->cRxLock;
  if (_13 == -1)
    goto <bb 39>; [INV]
  else
    goto <bb 40>; [INV]

  <bb 39> :
  pxQueue->cRxLock = 0;

  <bb 40> :
  _14 = pxQueue->cTxLock;
  if (_14 == -1)
    goto <bb 41>; [INV]
  else
    goto <bb 42>; [INV]

  <bb 41> :
  pxQueue->cTxLock = 0;

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

  <bb 43> :
  _16 = prvIsQueueFull (pxQueue);
  if (_16 != 0)
    goto <bb 44>; [INV]
  else
    goto <bb 46>; [INV]

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

  <bb 45> :
  _20 = 3758157060B;
  *_20 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 48>; [INV]

  <bb 46> :
  prvUnlockQueue (pxQueue);
  xTaskResumeAll ();
  goto <bb 48>; [INV]

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

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

  <bb 49> :
  xTimeOut = {CLOBBER};

  <bb 50> :
<L55>:
  return D.6882;

}


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

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

  <bb 3> :
  if (uxInitialCount <= uxMaxCount)
    goto <bb 4>; [INV]
  else
    goto <bb 7>; [INV]

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

  <bb 5> :
  MEM[(struct Queue_t *)xHandle].uxMessagesWaiting = uxInitialCount;

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

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

  <bb 8> :
  vPortRaiseBASEPRI ();

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

  <bb 10> :
  D.6845 = xHandle;

  <bb 11> :
<L10>:
  return D.6845;

}


xQueueTakeMutexRecursive (struct QueueDefinition * xMutex, TickType_t xTicksToWait)
{
  struct Queue_t * const pxMutex;
  BaseType_t xReturn;
  BaseType_t D.6834;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  _3 = pxMutex->u.xSemaphore.uxRecursiveCallCount;
  _4 = _3 + 1;
  pxMutex->u.xSemaphore.uxRecursiveCallCount = _4;
  xReturn = 1;
  goto <bb 9>; [INV]

  <bb 7> :
  xReturn = xQueueSemaphoreTake (pxMutex, xTicksToWait);
  if (xReturn != 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  _5 = pxMutex->u.xSemaphore.uxRecursiveCallCount;
  _6 = _5 + 1;
  pxMutex->u.xSemaphore.uxRecursiveCallCount = _6;

  <bb 9> :
  D.6834 = xReturn;

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

}


xQueueGiveMutexRecursive (struct QueueDefinition * xMutex)
{
  struct Queue_t * const pxMutex;
  BaseType_t xReturn;
  BaseType_t D.6824;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = pxMutex->u.xSemaphore.xMutexHolder;
  _2 = xTaskGetCurrentTaskHandle ();
  if (_1 == _2)
    goto <bb 6>; [INV]
  else
    goto <bb 9>; [INV]

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

  <bb 7> :
  xQueueGenericSend (pxMutex, 0B, 0, 0);

  <bb 8> :
  xReturn = 1;
  goto <bb 10>; [INV]

  <bb 9> :
  xReturn = 0;

  <bb 10> :
  D.6824 = xReturn;

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

}


xQueueGetMutexHolderFromISR (struct QueueDefinition * xSemaphore)
{
  struct tskTaskControlBlock * pxReturn;
  struct tskTaskControlBlock * D.6814;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = MEM[(struct Queue_t *)xSemaphore].pcHead;
  if (_1 == 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  pxReturn = MEM[(struct Queue_t *)xSemaphore].u.xSemaphore.xMutexHolder;
  goto <bb 8>; [INV]

  <bb 7> :
  pxReturn = 0B;

  <bb 8> :
  D.6814 = pxReturn;

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

}


xQueueGetMutexHolder (struct QueueDefinition * xSemaphore)
{
  struct Queue_t * const pxSemaphore;
  struct tskTaskControlBlock * pxReturn;
  struct tskTaskControlBlock * D.6807;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  pxReturn = pxSemaphore->u.xSemaphore.xMutexHolder;
  goto <bb 8>; [INV]

  <bb 7> :
  pxReturn = 0B;

  <bb 8> :
  vPortExitCritical ();
  D.6807 = pxReturn;

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

}


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

  <bb 2> :
  uxMutexLength = 1;
  uxMutexSize = 0;
  xNewQueue = xQueueGenericCreate (uxMutexLength, uxMutexSize, ucQueueType);
  prvInitialiseMutex (xNewQueue);
  D.6800 = xNewQueue;

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

}


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

  <bb 3> :
  pxNewQueue->u.xSemaphore.xMutexHolder = 0B;
  pxNewQueue->pcHead = 0B;
  pxNewQueue->u.xSemaphore.uxRecursiveCallCount = 0;
  xQueueGenericSend (pxNewQueue, 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 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  pxNewQueue->pcHead = pxNewQueue;
  goto <bb 5>; [INV]

  <bb 4> :
  pxNewQueue->pcHead = pucQueueStorage;

  <bb 5> :
  pxNewQueue->uxLength = uxQueueLength;
  pxNewQueue->uxItemSize = uxItemSize;
  xQueueGenericReset (pxNewQueue, 1);
  pxNewQueue->ucQueueType = ucQueueType;
  return;

}


xQueueGenericCreate (const UBaseType_t uxQueueLength, const UBaseType_t uxItemSize, const uint8_t ucQueueType)
{
  uint8_t * pucQueueStorage;
  size_t xQueueSizeInBytes;
  struct Queue_t * pxNewQueue;
  struct QueueDefinition * D.6792;

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

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

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

  <bb 5> :
  xQueueSizeInBytes = uxQueueLength * uxItemSize;
  _4 = xQueueSizeInBytes + 80;
  pxNewQueue = pvPortMalloc (_4);
  if (pxNewQueue != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  pucQueueStorage = pxNewQueue;
  pucQueueStorage = pucQueueStorage + 80;
  prvInitialiseNewQueue (uxQueueLength, uxItemSize, pucQueueStorage, ucQueueType, pxNewQueue);

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

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

  <bb 9> :
  vPortRaiseBASEPRI ();

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

  <bb 11> :
  D.6792 = pxNewQueue;

  <bb 12> :
<L11>:
  return D.6792;

}


xQueueGenericReset (struct QueueDefinition * xQueue, BaseType_t xNewQueue)
{
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  BaseType_t D.6780;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  if (pxQueue != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 6> :
  _1 = pxQueue->uxLength;
  if (_1 != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 8> :
  vPortEnterCritical ();
  _6 = pxQueue->pcHead;
  _7 = pxQueue->uxLength;
  _8 = pxQueue->uxItemSize;
  _9 = _7 * _8;
  _10 = _6 + _9;
  pxQueue->u.xQueue.pcTail = _10;
  pxQueue->uxMessagesWaiting = 0;
  _11 = pxQueue->pcHead;
  pxQueue->pcWriteTo = _11;
  _12 = pxQueue->pcHead;
  _13 = pxQueue->uxLength;
  _14 = _13 + 4294967295;
  _15 = pxQueue->uxItemSize;
  _16 = _14 * _15;
  _17 = _12 + _16;
  pxQueue->u.xQueue.pcReadFrom = _17;
  pxQueue->cRxLock = -1;
  pxQueue->cTxLock = -1;
  if (xNewQueue == 0)
    goto <bb 9>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 9> :
  _18 = pxQueue->xTasksWaitingToSend.uxNumberOfItems;
  if (_18 != 0)
    goto <bb 10>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 10> :
  _19 = &pxQueue->xTasksWaitingToSend;
  _20 = xTaskRemoveFromEventList (_19);
  if (_20 != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 11> :
  _21 = 3758157060B;
  *_21 = 268435456;
  __asm__ __volatile__("dsb" :  :  : "memory");
  __asm__ __volatile__("isb");
  goto <bb 13>; [INV]

  <bb 12> :
  _22 = &pxQueue->xTasksWaitingToSend;
  vListInitialise (_22);
  _23 = &pxQueue->xTasksWaitingToReceive;
  vListInitialise (_23);

  <bb 13> :
  vPortExitCritical ();
  goto <bb 15>; [INV]

  <bb 14> :
  xReturn = 0;

  <bb 15> :
  if (xReturn == 0)
    goto <bb 16>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 16> :
  vPortRaiseBASEPRI ();

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

  <bb 18> :
  D.6780 = xReturn;

  <bb 19> :
<L20>:
  return D.6780;

}


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

}


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

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

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

}


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

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

}