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> :
  # DEBUG BEGIN_STMT
  pxQueue_9 = xQueue_8(D);
  # DEBUG pxQueue => pxQueue_9
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _1 ={v} pxQueue_9->cRxLock;
  if (_1 == -1)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

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

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

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

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

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

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

}


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

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  ux_5 = 0;
  # DEBUG ux => ux_5
  goto <bb 9>; [INV]

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  xQueueRegistry[ux_2].pcQueueName = 0B;
  # DEBUG BEGIN_STMT
  xQueueRegistry[ux_2].xHandle = 0B;
  # DEBUG BEGIN_STMT
  goto <bb 10>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  ux_7 = ux_2 + 1;
  # DEBUG ux => ux_7

  <bb 9> :
  # ux_2 = PHI <ux_5(5), ux_7(8)>
  # DEBUG ux => ux_2
  # DEBUG BEGIN_STMT
  if (ux_2 <= 1)
    goto <bb 6>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 10> :
  return;

}


pcQueueGetName (struct QueueDefinition * xQueue)
{
  const char * pcReturn;
  UBaseType_t ux;
  struct QueueDefinition * _1;
  const char * _10;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  ux_6 = 0;
  # DEBUG ux => ux_6
  goto <bb 9>; [INV]

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  pcReturn_9 = xQueueRegistry[ux_2].pcQueueName;
  # DEBUG pcReturn => pcReturn_9
  # DEBUG BEGIN_STMT
  goto <bb 10>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  ux_8 = ux_2 + 1;
  # DEBUG ux => ux_8

  <bb 9> :
  # ux_2 = PHI <ux_6(5), ux_8(8)>
  # DEBUG ux => ux_2
  # DEBUG BEGIN_STMT
  if (ux_2 <= 1)
    goto <bb 6>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 10> :
  # pcReturn_3 = PHI <pcReturn_9(7), pcReturn_4(9)>
  # DEBUG pcReturn => pcReturn_3
  # DEBUG BEGIN_STMT
  _10 = pcReturn_3;
  return _10;

}


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

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxEntryToWrite_9 = 0B;
  # DEBUG pxEntryToWrite => pxEntryToWrite_9
  # DEBUG BEGIN_STMT
  if (pcQueueName_10(D) != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  ux_11 = 0;
  # DEBUG ux => ux_11
  goto <bb 13>; [INV]

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  pxEntryToWrite_15 = &xQueueRegistry[ux_3];
  # DEBUG pxEntryToWrite => pxEntryToWrite_15
  # DEBUG BEGIN_STMT
  goto <bb 14>; [INV]

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

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

  <bb 11> :
  # DEBUG BEGIN_STMT
  pxEntryToWrite_13 = &xQueueRegistry[ux_3];
  # DEBUG pxEntryToWrite => pxEntryToWrite_13

  <bb 12> :
  # pxEntryToWrite_4 = PHI <pxEntryToWrite_5(9), pxEntryToWrite_5(10), pxEntryToWrite_13(11)>
  # DEBUG pxEntryToWrite => pxEntryToWrite_4
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  ux_14 = ux_3 + 1;
  # DEBUG ux => ux_14

  <bb 13> :
  # ux_3 = PHI <ux_11(6), ux_14(12)>
  # pxEntryToWrite_5 = PHI <pxEntryToWrite_9(6), pxEntryToWrite_4(12)>
  # DEBUG pxEntryToWrite => pxEntryToWrite_5
  # DEBUG ux => ux_3
  # DEBUG BEGIN_STMT
  if (ux_3 <= 1)
    goto <bb 7>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 14> :
  # pxEntryToWrite_6 = PHI <pxEntryToWrite_9(5), pxEntryToWrite_15(8), pxEntryToWrite_5(13)>
  # DEBUG pxEntryToWrite => pxEntryToWrite_6
  # DEBUG BEGIN_STMT
  if (pxEntryToWrite_6 != 0B)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  # DEBUG BEGIN_STMT
  pxEntryToWrite_6->pcQueueName = pcQueueName_10(D);
  # DEBUG BEGIN_STMT
  pxEntryToWrite_6->xHandle = xQueue_8(D);

  <bb 16> :
  # DEBUG BEGIN_STMT
  return;

}


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

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

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

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

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

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  xReturn_7 = 0;
  # DEBUG xReturn => xReturn_7

  <bb 8> :
  # xReturn_3 = PHI <xReturn_8(6), xReturn_7(7)>
  # DEBUG xReturn => xReturn_3
  # DEBUG BEGIN_STMT
  _9 = xReturn_3;
  return _9;

}


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

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _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> :
  # DEBUG BEGIN_STMT
  xReturn_8 = 1;
  # DEBUG xReturn => xReturn_8
  goto <bb 5>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  xReturn_7 = 0;
  # DEBUG xReturn => xReturn_7

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

}


xQueueIsQueueEmptyFromISR (struct QueueDefinition * const xQueue)
{
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  long unsigned int _1;
  BaseType_t _8;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _1 ={v} pxQueue_4->uxMessagesWaiting;
  if (_1 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  xReturn_6 = 0;
  # DEBUG xReturn => xReturn_6

  <bb 8> :
  # xReturn_2 = PHI <xReturn_7(6), xReturn_6(7)>
  # DEBUG xReturn => xReturn_2
  # DEBUG BEGIN_STMT
  _8 = xReturn_2;
  return _8;

}


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

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

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

  <bb 4> :
  # DEBUG BEGIN_STMT
  xReturn_6 = 0;
  # DEBUG xReturn => xReturn_6

  <bb 5> :
  # xReturn_2 = PHI <xReturn_7(3), xReturn_6(4)>
  # DEBUG xReturn => xReturn_2
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _9 = xReturn_2;
  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.6_4;
  unsigned char _5;
  long unsigned int _6;
  struct List_t * _7;
  long int _8;
  unsigned char cRxLock.7_9;
  unsigned char _10;

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

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

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

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

  <bb 6> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  cTxLock.6_4 = (unsigned char) cTxLock_11;
  _5 = cTxLock.6_4 + 255;
  cTxLock_23 = (int8_t) _5;
  # DEBUG cTxLock => cTxLock_23

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  pxQueue_19(D)->cTxLock ={v} -1;
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  cRxLock_27 ={v} pxQueue_19(D)->cRxLock;
  # DEBUG cRxLock => cRxLock_27
  # DEBUG BEGIN_STMT
  goto <bb 13>; [INV]

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

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

  <bb 11> :
  # DEBUG BEGIN_STMT
  vTaskMissedYield ();

  <bb 12> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  cRxLock.7_9 = (unsigned char) cRxLock_12;
  _10 = cRxLock.7_9 + 255;
  cRxLock_30 = (int8_t) _10;
  # DEBUG cRxLock => cRxLock_30

  <bb 13> :
  # cRxLock_12 = PHI <cRxLock_27(8), cRxLock_30(12)>
  # DEBUG cRxLock => cRxLock_12
  # DEBUG BEGIN_STMT
  if (cRxLock_12 > 0)
    goto <bb 9>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  pxQueue_19(D)->cRxLock ={v} -1;
  # DEBUG BEGIN_STMT
  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> :
  # DEBUG BEGIN_STMT
  _1 = pxQueue_13(D)->uxItemSize;
  if (_1 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  _2 = pxQueue_13(D)->u.xQueue.pcReadFrom;
  _3 = pxQueue_13(D)->uxItemSize;
  _4 = _2 + _3;
  pxQueue_13(D)->u.xQueue.pcReadFrom = _4;
  # DEBUG BEGIN_STMT
  _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> :
  # DEBUG BEGIN_STMT
  _7 = pxQueue_13(D)->pcHead;
  pxQueue_13(D)->u.xQueue.pcReadFrom = _7;

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _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;
  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> :
  # DEBUG BEGIN_STMT
  xReturn_29 = 0;
  # DEBUG xReturn => xReturn_29
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxMessagesWaiting_32 ={v} pxQueue_31(D)->uxMessagesWaiting;
  # DEBUG uxMessagesWaiting => uxMessagesWaiting_32
  # DEBUG BEGIN_STMT
  _1 = pxQueue_31(D)->uxItemSize;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

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

  <bb 6> :
  # DEBUG BEGIN_STMT
  _4 = pxQueue_31(D)->pcWriteTo;
  _5 = pxQueue_31(D)->uxItemSize;
  memcpy (_4, pvItemToQueue_34(D), _5);
  # DEBUG BEGIN_STMT
  _6 = pxQueue_31(D)->pcWriteTo;
  _7 = pxQueue_31(D)->uxItemSize;
  _8 = _6 + _7;
  pxQueue_31(D)->pcWriteTo = _8;
  # DEBUG BEGIN_STMT
  _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> :
  # DEBUG BEGIN_STMT
  _11 = pxQueue_31(D)->pcHead;
  pxQueue_31(D)->pcWriteTo = _11;
  goto <bb 13>; [INV]

  <bb 8> :
  # DEBUG BEGIN_STMT
  _12 = pxQueue_31(D)->u.xQueue.pcReadFrom;
  _13 = pxQueue_31(D)->uxItemSize;
  memcpy (_12, pvItemToQueue_34(D), _13);
  # DEBUG BEGIN_STMT
  _14 = pxQueue_31(D)->u.xQueue.pcReadFrom;
  _15 = pxQueue_31(D)->uxItemSize;
  _16 = -_15;
  _17 = _14 + _16;
  pxQueue_31(D)->u.xQueue.pcReadFrom = _17;
  # DEBUG BEGIN_STMT
  _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> :
  # DEBUG BEGIN_STMT
  _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> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xPosition_33(D) == 2)
    goto <bb 11>; [INV]
  else
    goto <bb 13>; [INV]

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  uxMessagesWaiting_38 = uxMessagesWaiting_32 + 4294967295;
  # DEBUG uxMessagesWaiting => uxMessagesWaiting_38

  <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)>
  # DEBUG uxMessagesWaiting => uxMessagesWaiting_26
  # DEBUG xReturn => xReturn_25
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _24 = uxMessagesWaiting_26 + 1;
  pxQueue_31(D)->uxMessagesWaiting ={v} _24;
  # DEBUG BEGIN_STMT
  _46 = xReturn_25;
  return _46;

}


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

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

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

  <bb 4> :
  # DEBUG BEGIN_STMT
  uxHighestPriorityOfWaitingTasks_7 = 0;
  # DEBUG uxHighestPriorityOfWaitingTasks => uxHighestPriorityOfWaitingTasks_7

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

}


ucQueueGetQueueType (struct QueueDefinition * xQueue)
{
  uint8_t _3;

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

}


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

}


uxQueueGetQueueNumber (struct QueueDefinition * xQueue)
{
  UBaseType_t _3;

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

}


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

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vQueueUnregisterQueue (pxQueue_2);
  # DEBUG BEGIN_STMT
  vPortFree (pxQueue_2);
  return;

}


uxQueueMessagesWaitingFromISR (struct QueueDefinition * const xQueue)
{
  struct Queue_t * const pxQueue;
  UBaseType_t uxReturn;
  UBaseType_t _5;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxReturn_4 ={v} pxQueue_2->uxMessagesWaiting;
  # DEBUG uxReturn => uxReturn_4
  # DEBUG BEGIN_STMT
  _5 = uxReturn_4;
  return _5;

}


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

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _1 = pxQueue_4->uxLength;
  _2 ={v} pxQueue_4->uxMessagesWaiting;
  uxReturn_7 = _1 - _2;
  # DEBUG uxReturn => uxReturn_7
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _9 = uxReturn_7;
  return _9;

}


uxQueueMessagesWaiting (struct QueueDefinition * const xQueue)
{
  UBaseType_t uxReturn;
  UBaseType_t _6;

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

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

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

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  uxReturn_4 ={v} MEM[(struct Queue_t *)xQueue_1(D)].uxMessagesWaiting;
  # DEBUG uxReturn => uxReturn_4
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _6 = uxReturn_4;
  return _6;

}


xQueuePeekFromISR (struct QueueDefinition * xQueue, void * const pvBuffer)
{
  struct Queue_t * const pxQueue;
  int8_t * pcOriginalReadPosition;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  int iftmp.29_5;
  int iftmp.29_11;
  int iftmp.29_12;
  BaseType_t _22;

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

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

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

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

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

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

  <bb 8> :
  iftmp.29_11 = 0;

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

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

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

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

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

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

  <bb 15> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus_15 = ulPortRaiseBASEPRI ();
  # DEBUG uxSavedInterruptStatus => uxSavedInterruptStatus_15
  # DEBUG BEGIN_STMT
  _3 ={v} pxQueue_8->uxMessagesWaiting;
  if (_3 != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pcOriginalReadPosition_17 = pxQueue_8->u.xQueue.pcReadFrom;
  # DEBUG pcOriginalReadPosition => pcOriginalReadPosition_17
  # DEBUG BEGIN_STMT
  prvCopyDataFromQueue (pxQueue_8, pvBuffer_9(D));
  # DEBUG BEGIN_STMT
  pxQueue_8->u.xQueue.pcReadFrom = pcOriginalReadPosition_17;
  # DEBUG BEGIN_STMT
  xReturn_20 = 1;
  # DEBUG xReturn => xReturn_20
  goto <bb 18>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  xReturn_16 = 0;
  # DEBUG xReturn => xReturn_16

  <bb 18> :
  # xReturn_4 = PHI <xReturn_20(16), xReturn_16(17)>
  # DEBUG xReturn => xReturn_4
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptStatus_15);
  # DEBUG BEGIN_STMT
  _22 = xReturn_4;
  return _22;

}


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;
  long unsigned int _1;
  long unsigned int _2;
  long unsigned int _3;
  struct List_t * _4;
  long int _5;
  unsigned char cRxLock.28_6;
  unsigned char _7;
  signed char _8;
  int iftmp.27_10;
  int iftmp.27_17;
  int iftmp.27_18;
  BaseType_t _34;

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

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

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

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

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

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

  <bb 8> :
  iftmp.27_17 = 0;

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

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

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus_21 = ulPortRaiseBASEPRI ();
  # DEBUG uxSavedInterruptStatus => uxSavedInterruptStatus_21
  # DEBUG BEGIN_STMT
  uxMessagesWaiting_22 ={v} pxQueue_14->uxMessagesWaiting;
  # DEBUG uxMessagesWaiting => uxMessagesWaiting_22
  # DEBUG BEGIN_STMT
  if (uxMessagesWaiting_22 != 0)
    goto <bb 13>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 13> :
  # DEBUG BEGIN_STMT
  cRxLock_24 ={v} pxQueue_14->cRxLock;
  # DEBUG cRxLock => cRxLock_24
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  prvCopyDataFromQueue (pxQueue_14, pvBuffer_15(D));
  # DEBUG BEGIN_STMT
  _2 = uxMessagesWaiting_22 + 4294967295;
  pxQueue_14->uxMessagesWaiting ={v} _2;
  # DEBUG BEGIN_STMT
  if (cRxLock_24 == -1)
    goto <bb 14>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 14> :
  # DEBUG BEGIN_STMT
  _3 ={v} pxQueue_14->xTasksWaitingToSend.uxNumberOfItems;
  if (_3 != 0)
    goto <bb 15>; [INV]
  else
    goto <bb 22>; [INV]

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

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

  <bb 17> :
  # DEBUG BEGIN_STMT
  *pxHigherPriorityTaskWoken_30(D) = 1;
  goto <bb 22>; [INV]

  <bb 18> :
  # DEBUG BEGIN_STMT
  if (cRxLock_24 == 127)
    goto <bb 19>; [INV]
  else
    goto <bb 21>; [INV]

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

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

  <bb 21> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  cRxLock.28_6 = (unsigned char) cRxLock_24;
  _7 = cRxLock.28_6 + 1;
  _8 = (signed char) _7;
  pxQueue_14->cRxLock ={v} _8;

  <bb 22> :
  # DEBUG BEGIN_STMT
  xReturn_32 = 1;
  # DEBUG xReturn => xReturn_32
  goto <bb 24>; [INV]

  <bb 23> :
  # DEBUG BEGIN_STMT
  xReturn_23 = 0;
  # DEBUG xReturn => xReturn_23

  <bb 24> :
  # xReturn_9 = PHI <xReturn_32(22), xReturn_23(23)>
  # DEBUG xReturn => xReturn_9
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptStatus_21);
  # DEBUG BEGIN_STMT
  _34 = xReturn_9;
  return _34;

}


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;
  long unsigned int _1;
  long int _2;
  long unsigned int xTicksToWait.24_3;
  long unsigned int _4;
  struct List_t * _5;
  long int _6;
  volatile uint32_t * _7;
  long unsigned int xTicksToWait.25_8;
  signed char _9;
  signed char _10;
  long int _11;
  long int _12;
  struct List_t * _13;
  long unsigned int xTicksToWait.26_14;
  long int _15;
  volatile uint32_t * _16;
  long int _17;
  int iftmp.22_20;
  int iftmp.23_21;
  BaseType_t _22;
  int iftmp.22_34;
  int iftmp.22_35;
  int iftmp.23_37;
  int iftmp.23_38;
  BaseType_t _53;
  BaseType_t _64;
  BaseType_t _73;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xEntryTimeSet_29 = 0;
  # DEBUG xEntryTimeSet => xEntryTimeSet_29
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxQueue_31 = xQueue_30(D);
  # DEBUG pxQueue => pxQueue_31
  # DEBUG BEGIN_STMT
  if (pxQueue_31 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

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

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

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

  <bb 8> :
  iftmp.22_34 = 0;

  <bb 9> :
  # iftmp.22_20 = PHI <iftmp.22_35(7), iftmp.22_34(8)>
  if (iftmp.22_20 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

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

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

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

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

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

  <bb 15> :
  iftmp.23_37 = 0;

  <bb 16> :
  # iftmp.23_21 = PHI <iftmp.23_38(14), iftmp.23_37(15)>
  if (iftmp.23_21 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

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

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

  <bb 19> :
  # xEntryTimeSet_18 = PHI <xEntryTimeSet_29(16), xEntryTimeSet_19(37), xEntryTimeSet_19(36), xEntryTimeSet_19(34), xEntryTimeSet_19(35)>
  # DEBUG xEntryTimeSet => xEntryTimeSet_18
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  uxMessagesWaiting_40 ={v} pxQueue_31->uxMessagesWaiting;
  # DEBUG uxMessagesWaiting => uxMessagesWaiting_40
  # DEBUG BEGIN_STMT
  if (uxMessagesWaiting_40 != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 20> :
  # DEBUG BEGIN_STMT
  pcOriginalReadPosition_65 = pxQueue_31->u.xQueue.pcReadFrom;
  # DEBUG pcOriginalReadPosition => pcOriginalReadPosition_65
  # DEBUG BEGIN_STMT
  prvCopyDataFromQueue (pxQueue_31, pvBuffer_32(D));
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxQueue_31->u.xQueue.pcReadFrom = pcOriginalReadPosition_65;
  # DEBUG BEGIN_STMT
  _4 ={v} pxQueue_31->xTasksWaitingToReceive.uxNumberOfItems;
  if (_4 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 23>; [INV]

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

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

  <bb 23> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _73 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 39>; [INV]

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

  <bb 25> :
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _64 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 39>; [INV]

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

  <bb 27> :
  # DEBUG BEGIN_STMT
  vTaskInternalSetTimeOutState (&xTimeOut);
  # DEBUG BEGIN_STMT
  xEntryTimeSet_42 = 1;
  # DEBUG xEntryTimeSet => xEntryTimeSet_42

  <bb 28> :
  # xEntryTimeSet_19 = PHI <xEntryTimeSet_18(26), xEntryTimeSet_42(27)>
  # DEBUG xEntryTimeSet => xEntryTimeSet_19
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _9 ={v} pxQueue_31->cRxLock;
  if (_9 == -1)
    goto <bb 29>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 29> :
  # DEBUG BEGIN_STMT
  pxQueue_31->cRxLock ={v} 0;

  <bb 30> :
  # DEBUG BEGIN_STMT
  _10 ={v} pxQueue_31->cTxLock;
  if (_10 == -1)
    goto <bb 31>; [INV]
  else
    goto <bb 32>; [INV]

  <bb 31> :
  # DEBUG BEGIN_STMT
  pxQueue_31->cTxLock ={v} 0;

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

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

  <bb 34> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _13 = &pxQueue_31->xTasksWaitingToReceive;
  xTicksToWait.26_14 = xTicksToWait;
  vTaskPlaceOnEventList (_13, xTicksToWait.26_14);
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_31);
  # DEBUG BEGIN_STMT
  _15 = xTaskResumeAll ();
  if (_15 == 0)
    goto <bb 35>; [INV]
  else
    goto <bb 19>; [INV]

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

  <bb 36> :
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_31);
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  goto <bb 19>; [INV]

  <bb 37> :
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_31);
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  _17 = prvIsQueueEmpty (pxQueue_31);
  if (_17 != 0)
    goto <bb 38>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 38> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _53 = 0;
  // predicted unlikely by early return (on trees) predictor.

  <bb 39> :
  # _22 = PHI <_73(23), _64(25), _53(38)>
  xTimeOut ={v} {CLOBBER};
  return _22;

}


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;
  long unsigned int _1;
  long int _2;
  long unsigned int xTicksToWait.19_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.20_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.21_19;
  long int _20;
  volatile uint32_t * _21;
  long int _22;
  struct tskTaskControlBlock * _23;
  int iftmp.18_28;
  BaseType_t _29;
  int iftmp.18_45;
  int iftmp.18_46;
  BaseType_t _66;
  BaseType_t _81;
  BaseType_t _91;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xEntryTimeSet_39 = 0;
  # DEBUG xEntryTimeSet => xEntryTimeSet_39
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxQueue_41 = xQueue_40(D);
  # DEBUG pxQueue => pxQueue_41
  # DEBUG BEGIN_STMT
  xInheritanceOccurred_42 = 0;
  # DEBUG xInheritanceOccurred => xInheritanceOccurred_42
  # DEBUG BEGIN_STMT
  if (pxQueue_41 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

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

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

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

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

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

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

  <bb 11> :
  iftmp.18_45 = 0;

  <bb 12> :
  # iftmp.18_28 = PHI <iftmp.18_46(10), iftmp.18_45(11)>
  if (iftmp.18_28 == 0)
    goto <bb 13>; [INV]
  else
    goto <bb 15>; [INV]

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

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

  <bb 15> :
  # xEntryTimeSet_24 = PHI <xEntryTimeSet_39(12), xEntryTimeSet_25(40), xEntryTimeSet_25(39), xEntryTimeSet_25(37), xEntryTimeSet_25(38)>
  # xInheritanceOccurred_26 = PHI <xInheritanceOccurred_42(12), xInheritanceOccurred_26(40), xInheritanceOccurred_26(39), xInheritanceOccurred_27(37), xInheritanceOccurred_27(38)>
  # DEBUG xInheritanceOccurred => xInheritanceOccurred_26
  # DEBUG xEntryTimeSet => xEntryTimeSet_24
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  uxSemaphoreCount_48 ={v} pxQueue_41->uxMessagesWaiting;
  # DEBUG uxSemaphoreCount => uxSemaphoreCount_48
  # DEBUG BEGIN_STMT
  if (uxSemaphoreCount_48 != 0)
    goto <bb 16>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _4 = uxSemaphoreCount_48 + 4294967295;
  pxQueue_41->uxMessagesWaiting ={v} _4;
  # DEBUG BEGIN_STMT
  _5 = pxQueue_41->pcHead;
  if (_5 == 0B)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  _6 = pvTaskIncrementMutexHeldCount ();
  pxQueue_41->u.xSemaphore.xMutexHolder = _6;

  <bb 18> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _7 ={v} pxQueue_41->xTasksWaitingToSend.uxNumberOfItems;
  if (_7 != 0)
    goto <bb 19>; [INV]
  else
    goto <bb 21>; [INV]

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

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

  <bb 21> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _91 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 44>; [INV]

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

  <bb 23> :
  # DEBUG BEGIN_STMT
  if (xInheritanceOccurred_26 != 0)
    goto <bb 24>; [INV]
  else
    goto <bb 26>; [INV]

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

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

  <bb 26> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _81 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 44>; [INV]

  <bb 27> :
  # DEBUG BEGIN_STMT
  if (xEntryTimeSet_24 == 0)
    goto <bb 28>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 28> :
  # DEBUG BEGIN_STMT
  vTaskInternalSetTimeOutState (&xTimeOut);
  # DEBUG BEGIN_STMT
  xEntryTimeSet_50 = 1;
  # DEBUG xEntryTimeSet => xEntryTimeSet_50

  <bb 29> :
  # xEntryTimeSet_25 = PHI <xEntryTimeSet_24(27), xEntryTimeSet_50(28)>
  # DEBUG xEntryTimeSet => xEntryTimeSet_25
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _12 ={v} pxQueue_41->cRxLock;
  if (_12 == -1)
    goto <bb 30>; [INV]
  else
    goto <bb 31>; [INV]

  <bb 30> :
  # DEBUG BEGIN_STMT
  pxQueue_41->cRxLock ={v} 0;

  <bb 31> :
  # DEBUG BEGIN_STMT
  _13 ={v} pxQueue_41->cTxLock;
  if (_13 == -1)
    goto <bb 32>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 32> :
  # DEBUG BEGIN_STMT
  pxQueue_41->cTxLock ={v} 0;

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

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

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

  <bb 36> :
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _17 = pxQueue_41->u.xSemaphore.xMutexHolder;
  xInheritanceOccurred_72 = xTaskPriorityInherit (_17);
  # DEBUG xInheritanceOccurred => xInheritanceOccurred_72
  # DEBUG BEGIN_STMT
  vPortExitCritical ();

  <bb 37> :
  # xInheritanceOccurred_27 = PHI <xInheritanceOccurred_26(35), xInheritanceOccurred_72(36)>
  # DEBUG xInheritanceOccurred => xInheritanceOccurred_27
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _18 = &pxQueue_41->xTasksWaitingToReceive;
  xTicksToWait.21_19 = xTicksToWait;
  vTaskPlaceOnEventList (_18, xTicksToWait.21_19);
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_41);
  # DEBUG BEGIN_STMT
  _20 = xTaskResumeAll ();
  if (_20 == 0)
    goto <bb 38>; [INV]
  else
    goto <bb 15>; [INV]

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

  <bb 39> :
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_41);
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  goto <bb 15>; [INV]

  <bb 40> :
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_41);
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  _22 = prvIsQueueEmpty (pxQueue_41);
  if (_22 != 0)
    goto <bb 41>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 41> :
  # DEBUG BEGIN_STMT
  if (xInheritanceOccurred_26 != 0)
    goto <bb 42>; [INV]
  else
    goto <bb 43>; [INV]

  <bb 42> :
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxHighestWaitingPriority_63 = prvGetDisinheritPriorityAfterTimeout (pxQueue_41);
  # DEBUG uxHighestWaitingPriority => uxHighestWaitingPriority_63
  # DEBUG BEGIN_STMT
  _23 = pxQueue_41->u.xSemaphore.xMutexHolder;
  vTaskPriorityDisinheritAfterTimeout (_23, uxHighestWaitingPriority_63);
  # DEBUG BEGIN_STMT
  vPortExitCritical ();

  <bb 43> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _66 = 0;
  // predicted unlikely by early return (on trees) predictor.

  <bb 44> :
  # _29 = PHI <_91(21), _81(26), _66(43)>
  xTimeOut ={v} {CLOBBER};
  return _29;

}


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;
  long unsigned int _1;
  long int _2;
  long unsigned int xTicksToWait.15_3;
  long unsigned int _4;
  long unsigned int _5;
  struct List_t * _6;
  long int _7;
  volatile uint32_t * _8;
  long unsigned int xTicksToWait.16_9;
  signed char _10;
  signed char _11;
  long int _12;
  long int _13;
  struct List_t * _14;
  long unsigned int xTicksToWait.17_15;
  long int _16;
  volatile uint32_t * _17;
  long int _18;
  int iftmp.13_21;
  int iftmp.14_22;
  BaseType_t _23;
  int iftmp.13_35;
  int iftmp.13_36;
  int iftmp.14_38;
  int iftmp.14_39;
  BaseType_t _54;
  BaseType_t _65;
  BaseType_t _73;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xEntryTimeSet_30 = 0;
  # DEBUG xEntryTimeSet => xEntryTimeSet_30
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxQueue_32 = xQueue_31(D);
  # DEBUG pxQueue => pxQueue_32
  # DEBUG BEGIN_STMT
  if (pxQueue_32 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

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

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

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

  <bb 8> :
  iftmp.13_35 = 0;

  <bb 9> :
  # iftmp.13_21 = PHI <iftmp.13_36(7), iftmp.13_35(8)>
  if (iftmp.13_21 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

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

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

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

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

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

  <bb 15> :
  iftmp.14_38 = 0;

  <bb 16> :
  # iftmp.14_22 = PHI <iftmp.14_39(14), iftmp.14_38(15)>
  if (iftmp.14_22 == 0)
    goto <bb 17>; [INV]
  else
    goto <bb 19>; [INV]

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

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

  <bb 19> :
  # xEntryTimeSet_19 = PHI <xEntryTimeSet_30(16), xEntryTimeSet_20(37), xEntryTimeSet_20(36), xEntryTimeSet_20(34), xEntryTimeSet_20(35)>
  # DEBUG xEntryTimeSet => xEntryTimeSet_19
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  uxMessagesWaiting_41 ={v} pxQueue_32->uxMessagesWaiting;
  # DEBUG uxMessagesWaiting => uxMessagesWaiting_41
  # DEBUG BEGIN_STMT
  if (uxMessagesWaiting_41 != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 20> :
  # DEBUG BEGIN_STMT
  prvCopyDataFromQueue (pxQueue_32, pvBuffer_33(D));
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _4 = uxMessagesWaiting_41 + 4294967295;
  pxQueue_32->uxMessagesWaiting ={v} _4;
  # DEBUG BEGIN_STMT
  _5 ={v} pxQueue_32->xTasksWaitingToSend.uxNumberOfItems;
  if (_5 != 0)
    goto <bb 21>; [INV]
  else
    goto <bb 23>; [INV]

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

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

  <bb 23> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _73 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 39>; [INV]

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

  <bb 25> :
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _65 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 39>; [INV]

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

  <bb 27> :
  # DEBUG BEGIN_STMT
  vTaskInternalSetTimeOutState (&xTimeOut);
  # DEBUG BEGIN_STMT
  xEntryTimeSet_43 = 1;
  # DEBUG xEntryTimeSet => xEntryTimeSet_43

  <bb 28> :
  # xEntryTimeSet_20 = PHI <xEntryTimeSet_19(26), xEntryTimeSet_43(27)>
  # DEBUG xEntryTimeSet => xEntryTimeSet_20
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _10 ={v} pxQueue_32->cRxLock;
  if (_10 == -1)
    goto <bb 29>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 29> :
  # DEBUG BEGIN_STMT
  pxQueue_32->cRxLock ={v} 0;

  <bb 30> :
  # DEBUG BEGIN_STMT
  _11 ={v} pxQueue_32->cTxLock;
  if (_11 == -1)
    goto <bb 31>; [INV]
  else
    goto <bb 32>; [INV]

  <bb 31> :
  # DEBUG BEGIN_STMT
  pxQueue_32->cTxLock ={v} 0;

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

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

  <bb 34> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _14 = &pxQueue_32->xTasksWaitingToReceive;
  xTicksToWait.17_15 = xTicksToWait;
  vTaskPlaceOnEventList (_14, xTicksToWait.17_15);
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_32);
  # DEBUG BEGIN_STMT
  _16 = xTaskResumeAll ();
  if (_16 == 0)
    goto <bb 35>; [INV]
  else
    goto <bb 19>; [INV]

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

  <bb 36> :
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_32);
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  goto <bb 19>; [INV]

  <bb 37> :
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_32);
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  _18 = prvIsQueueEmpty (pxQueue_32);
  if (_18 != 0)
    goto <bb 38>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 38> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _54 = 0;
  // predicted unlikely by early return (on trees) predictor.

  <bb 39> :
  # _23 = PHI <_73(23), _65(25), _54(38)>
  xTimeOut ={v} {CLOBBER};
  return _23;

}


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;
  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.12_9;
  unsigned char _10;
  signed char _11;
  int iftmp.11_13;
  int iftmp.11_19;
  int iftmp.11_20;
  BaseType_t _35;

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

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

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

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

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

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

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

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

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

  <bb 11> :
  iftmp.11_19 = 0;

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

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

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

  <bb 15> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus_23 = ulPortRaiseBASEPRI ();
  # DEBUG uxSavedInterruptStatus => uxSavedInterruptStatus_23
  # DEBUG BEGIN_STMT
  uxMessagesWaiting_24 ={v} pxQueue_17->uxMessagesWaiting;
  # DEBUG uxMessagesWaiting => uxMessagesWaiting_24
  # DEBUG BEGIN_STMT
  _4 = pxQueue_17->uxLength;
  if (uxMessagesWaiting_24 < _4)
    goto <bb 16>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 16> :
  # DEBUG BEGIN_STMT
  cTxLock_26 ={v} pxQueue_17->cTxLock;
  # DEBUG cTxLock => cTxLock_26
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _5 = uxMessagesWaiting_24 + 1;
  pxQueue_17->uxMessagesWaiting ={v} _5;
  # DEBUG BEGIN_STMT
  if (cTxLock_26 == -1)
    goto <bb 17>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 17> :
  # DEBUG BEGIN_STMT
  _6 ={v} pxQueue_17->xTasksWaitingToReceive.uxNumberOfItems;
  if (_6 != 0)
    goto <bb 18>; [INV]
  else
    goto <bb 25>; [INV]

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

  <bb 19> :
  # DEBUG BEGIN_STMT
  if (pxHigherPriorityTaskWoken_31(D) != 0B)
    goto <bb 20>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 20> :
  # DEBUG BEGIN_STMT
  *pxHigherPriorityTaskWoken_31(D) = 1;
  goto <bb 25>; [INV]

  <bb 21> :
  # DEBUG BEGIN_STMT
  if (cTxLock_26 == 127)
    goto <bb 22>; [INV]
  else
    goto <bb 24>; [INV]

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

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

  <bb 24> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  cTxLock.12_9 = (unsigned char) cTxLock_26;
  _10 = cTxLock.12_9 + 1;
  _11 = (signed char) _10;
  pxQueue_17->cTxLock ={v} _11;

  <bb 25> :
  # DEBUG BEGIN_STMT
  xReturn_33 = 1;
  # DEBUG xReturn => xReturn_33
  goto <bb 27>; [INV]

  <bb 26> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xReturn_25 = 0;
  # DEBUG xReturn => xReturn_25

  <bb 27> :
  # xReturn_12 = PHI <xReturn_33(25), xReturn_25(26)>
  # DEBUG xReturn => xReturn_12
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptStatus_23);
  # DEBUG BEGIN_STMT
  _35 = xReturn_12;
  return _35;

}


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;
  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.10_8;
  unsigned char _9;
  signed char _10;
  int iftmp.8_12;
  int iftmp.9_13;
  int iftmp.8_20;
  int iftmp.8_21;
  int iftmp.9_23;
  int iftmp.9_24;
  BaseType_t _39;

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

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

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

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

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

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

  <bb 8> :
  iftmp.8_20 = 0;

  <bb 9> :
  # iftmp.8_12 = PHI <iftmp.8_21(7), iftmp.8_20(8)>
  if (iftmp.8_12 == 0)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

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

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xCopyPosition_22(D) != 2)
    goto <bb 14>; [INV]
  else
    goto <bb 13>; [INV]

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

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

  <bb 15> :
  iftmp.9_23 = 0;

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

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

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

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortValidateInterruptPriority ();
  # DEBUG BEGIN_STMT
  uxSavedInterruptStatus_27 = ulPortRaiseBASEPRI ();
  # DEBUG uxSavedInterruptStatus => uxSavedInterruptStatus_27
  # DEBUG BEGIN_STMT
  _3 ={v} pxQueue_17->uxMessagesWaiting;
  _4 = pxQueue_17->uxLength;
  if (_3 < _4)
    goto <bb 21>; [INV]
  else
    goto <bb 20>; [INV]

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

  <bb 21> :
  # DEBUG BEGIN_STMT
  cTxLock_29 ={v} pxQueue_17->cTxLock;
  # DEBUG cTxLock => cTxLock_29
  # DEBUG BEGIN_STMT
  uxPreviousMessagesWaiting_30 ={v} pxQueue_17->uxMessagesWaiting;
  # DEBUG uxPreviousMessagesWaiting => uxPreviousMessagesWaiting_30
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  prvCopyDataToQueue (pxQueue_17, pvItemToQueue_18(D), xCopyPosition_22(D));
  # DEBUG BEGIN_STMT
  if (cTxLock_29 == -1)
    goto <bb 22>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 22> :
  # DEBUG BEGIN_STMT
  _5 ={v} pxQueue_17->xTasksWaitingToReceive.uxNumberOfItems;
  if (_5 != 0)
    goto <bb 23>; [INV]
  else
    goto <bb 30>; [INV]

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

  <bb 24> :
  # DEBUG BEGIN_STMT
  if (pxHigherPriorityTaskWoken_35(D) != 0B)
    goto <bb 25>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 25> :
  # DEBUG BEGIN_STMT
  *pxHigherPriorityTaskWoken_35(D) = 1;
  goto <bb 30>; [INV]

  <bb 26> :
  # DEBUG BEGIN_STMT
  if (cTxLock_29 == 127)
    goto <bb 27>; [INV]
  else
    goto <bb 29>; [INV]

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

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

  <bb 29> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  cTxLock.10_8 = (unsigned char) cTxLock_29;
  _9 = cTxLock.10_8 + 1;
  _10 = (signed char) _9;
  pxQueue_17->cTxLock ={v} _10;

  <bb 30> :
  # DEBUG BEGIN_STMT
  xReturn_37 = 1;
  # DEBUG xReturn => xReturn_37
  goto <bb 32>; [INV]

  <bb 31> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xReturn_28 = 0;
  # DEBUG xReturn => xReturn_28

  <bb 32> :
  # xReturn_11 = PHI <xReturn_37(30), xReturn_28(31)>
  # DEBUG xReturn => xReturn_11
  # DEBUG BEGIN_STMT
  vPortSetBASEPRI (uxSavedInterruptStatus_27);
  # DEBUG BEGIN_STMT
  _39 = xReturn_11;
  return _39;

}


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;
  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_38;
  int iftmp.0_39;
  int iftmp.1_41;
  int iftmp.1_42;
  int iftmp.2_44;
  int iftmp.2_45;
  BaseType_t _58;
  BaseType_t _69;
  BaseType_t _80;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xEntryTimeSet_33 = 0;
  # DEBUG xEntryTimeSet => xEntryTimeSet_33
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxQueue_35 = xQueue_34(D);
  # DEBUG pxQueue => pxQueue_35
  # DEBUG BEGIN_STMT
  if (pxQueue_35 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

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

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

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

  <bb 8> :
  iftmp.0_38 = 0;

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

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

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xCopyPosition_40(D) != 2)
    goto <bb 14>; [INV]
  else
    goto <bb 13>; [INV]

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

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

  <bb 15> :
  iftmp.1_41 = 0;

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

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

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

  <bb 19> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _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_45 = 1;
  goto <bb 23>; [INV]

  <bb 22> :
  iftmp.2_44 = 0;

  <bb 23> :
  # iftmp.2_25 = PHI <iftmp.2_45(21), iftmp.2_44(22)>
  if (iftmp.2_25 == 0)
    goto <bb 24>; [INV]
  else
    goto <bb 26>; [INV]

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

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

  <bb 26> :
  # xEntryTimeSet_21 = PHI <xEntryTimeSet_33(23), xEntryTimeSet_22(45), xEntryTimeSet_22(46), xEntryTimeSet_22(44)>
  # DEBUG xEntryTimeSet => xEntryTimeSet_21
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _5 ={v} pxQueue_35->uxMessagesWaiting;
  _6 = pxQueue_35->uxLength;
  if (_5 < _6)
    goto <bb 28>; [INV]
  else
    goto <bb 27>; [INV]

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

  <bb 28> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xYieldRequired_71 = prvCopyDataToQueue (pxQueue_35, pvItemToQueue_36(D), xCopyPosition_40(D));
  # DEBUG xYieldRequired => xYieldRequired_71
  # DEBUG BEGIN_STMT
  _7 ={v} pxQueue_35->xTasksWaitingToReceive.uxNumberOfItems;
  if (_7 != 0)
    goto <bb 29>; [INV]
  else
    goto <bb 31>; [INV]

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

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

  <bb 31> :
  # DEBUG BEGIN_STMT
  if (xYieldRequired_71 != 0)
    goto <bb 32>; [INV]
  else
    goto <bb 33>; [INV]

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

  <bb 33> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _80 = 1;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 48>; [INV]

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

  <bb 35> :
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _69 = 0;
  // predicted unlikely by early return (on trees) predictor.
  goto <bb 48>; [INV]

  <bb 36> :
  # DEBUG BEGIN_STMT
  if (xEntryTimeSet_21 == 0)
    goto <bb 37>; [INV]
  else
    goto <bb 38>; [INV]

  <bb 37> :
  # DEBUG BEGIN_STMT
  vTaskInternalSetTimeOutState (&xTimeOut);
  # DEBUG BEGIN_STMT
  xEntryTimeSet_48 = 1;
  # DEBUG xEntryTimeSet => xEntryTimeSet_48

  <bb 38> :
  # xEntryTimeSet_22 = PHI <xEntryTimeSet_21(36), xEntryTimeSet_48(37)>
  # DEBUG xEntryTimeSet => xEntryTimeSet_22
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  vTaskSuspendAll ();
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _13 ={v} pxQueue_35->cRxLock;
  if (_13 == -1)
    goto <bb 39>; [INV]
  else
    goto <bb 40>; [INV]

  <bb 39> :
  # DEBUG BEGIN_STMT
  pxQueue_35->cRxLock ={v} 0;

  <bb 40> :
  # DEBUG BEGIN_STMT
  _14 ={v} pxQueue_35->cTxLock;
  if (_14 == -1)
    goto <bb 41>; [INV]
  else
    goto <bb 42>; [INV]

  <bb 41> :
  # DEBUG BEGIN_STMT
  pxQueue_35->cTxLock ={v} 0;

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

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

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

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

  <bb 46> :
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_35);
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  goto <bb 26>; [INV]

  <bb 47> :
  # DEBUG BEGIN_STMT
  prvUnlockQueue (pxQueue_35);
  # DEBUG BEGIN_STMT
  xTaskResumeAll ();
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _58 = 0;
  // predicted unlikely by early return (on trees) predictor.

  <bb 48> :
  # _26 = PHI <_80(33), _69(35), _58(47)>
  xTimeOut ={v} {CLOBBER};
  return _26;

}


xQueueCreateCountingSemaphore (const UBaseType_t uxMaxCount, const UBaseType_t uxInitialCount)
{
  struct QueueDefinition * xHandle;
  struct QueueDefinition * _11;

  <bb 2> :
  # DEBUG BEGIN_STMT
  xHandle_3 = 0B;
  # DEBUG xHandle => xHandle_3
  # DEBUG BEGIN_STMT
  if (uxMaxCount_4(D) != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :
  # DEBUG BEGIN_STMT
  xHandle_8 = xQueueGenericCreate (uxMaxCount_4(D), 0, 2);
  # DEBUG xHandle => xHandle_8
  # DEBUG BEGIN_STMT
  if (xHandle_8 != 0B)
    goto <bb 5>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  MEM[(struct Queue_t *)xHandle_8].uxMessagesWaiting ={v} uxInitialCount_5(D);
  # DEBUG BEGIN_STMT
  goto <bb 9>; [INV]

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

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

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

  <bb 9> :
  # xHandle_1 = PHI <xHandle_8(5), xHandle_3(6), xHandle_8(4)>
  # DEBUG xHandle => xHandle_1
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _11 = xHandle_1;
  return _11;

}


xQueueTakeMutexRecursive (struct QueueDefinition * xMutex, TickType_t xTicksToWait)
{
  struct Queue_t * const pxMutex;
  BaseType_t xReturn;
  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> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxMutex_10 = xMutex_9(D);
  # DEBUG pxMutex => pxMutex_10
  # DEBUG BEGIN_STMT
  if (pxMutex_10 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

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

  <bb 6> :
  # DEBUG BEGIN_STMT
  _3 = pxMutex_10->u.xSemaphore.uxRecursiveCallCount;
  _4 = _3 + 1;
  pxMutex_10->u.xSemaphore.uxRecursiveCallCount = _4;
  # DEBUG BEGIN_STMT
  xReturn_18 = 1;
  # DEBUG xReturn => xReturn_18
  goto <bb 9>; [INV]

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  _5 = pxMutex_10->u.xSemaphore.uxRecursiveCallCount;
  _6 = _5 + 1;
  pxMutex_10->u.xSemaphore.uxRecursiveCallCount = _6;

  <bb 9> :
  # xReturn_7 = PHI <xReturn_18(6), xReturn_15(7), xReturn_15(8)>
  # DEBUG xReturn => xReturn_7
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _19 = xReturn_7;
  return _19;

}


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

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

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

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

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

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

  <bb 7> :
  # DEBUG BEGIN_STMT
  xQueueGenericSend (pxMutex_10, 0B, 0, 0);

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

  <bb 9> :
  # DEBUG BEGIN_STMT
  xReturn_13 = 0;
  # DEBUG xReturn => xReturn_13

  <bb 10> :
  # xReturn_6 = PHI <xReturn_16(8), xReturn_13(9)>
  # DEBUG xReturn => xReturn_6
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _17 = xReturn_6;
  return _17;

}


xQueueGetMutexHolderFromISR (struct QueueDefinition * xSemaphore)
{
  struct tskTaskControlBlock * pxReturn;
  int8_t * _1;
  struct tskTaskControlBlock * _7;

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

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

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

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

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxReturn_6 = MEM[(struct Queue_t *)xSemaphore_3(D)].u.xSemaphore.xMutexHolder;
  # DEBUG pxReturn => pxReturn_6
  goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  pxReturn_5 = 0B;
  # DEBUG pxReturn => pxReturn_5

  <bb 8> :
  # pxReturn_2 = PHI <pxReturn_6(6), pxReturn_5(7)>
  # DEBUG pxReturn => pxReturn_2
  # DEBUG BEGIN_STMT
  _7 = pxReturn_2;
  return _7;

}


xQueueGetMutexHolder (struct QueueDefinition * xSemaphore)
{
  struct Queue_t * const pxSemaphore;
  struct tskTaskControlBlock * pxReturn;
  int8_t * _1;
  struct tskTaskControlBlock * _10;

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

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

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

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

  <bb 6> :
  # DEBUG BEGIN_STMT
  pxReturn_8 = pxSemaphore_4->u.xSemaphore.xMutexHolder;
  # DEBUG pxReturn => pxReturn_8
  goto <bb 8>; [INV]

  <bb 7> :
  # DEBUG BEGIN_STMT
  pxReturn_7 = 0B;
  # DEBUG pxReturn => pxReturn_7

  <bb 8> :
  # pxReturn_2 = PHI <pxReturn_8(6), pxReturn_7(7)>
  # DEBUG pxReturn => pxReturn_2
  # DEBUG BEGIN_STMT
  vPortExitCritical ();
  # DEBUG BEGIN_STMT
  _10 = pxReturn_2;
  return _10;

}


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

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  uxMutexLength_1 = 1;
  # DEBUG uxMutexLength => uxMutexLength_1
  uxMutexSize_2 = 0;
  # DEBUG uxMutexSize => uxMutexSize_2
  # DEBUG BEGIN_STMT
  xNewQueue_6 = xQueueGenericCreate (1, 0, ucQueueType_4(D));
  # DEBUG xNewQueue => xNewQueue_6
  # DEBUG BEGIN_STMT
  prvInitialiseMutex (xNewQueue_6);
  # DEBUG BEGIN_STMT
  _8 = xNewQueue_6;
  return _8;

}


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

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

  <bb 4> :
  # DEBUG BEGIN_STMT
  return;

}


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

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

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

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

}


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

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxNewQueue_7 = 0B;
  # DEBUG pxNewQueue => pxNewQueue_7
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (uxQueueLength_8(D) != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 7>; [INV]

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

  <bb 4> :
  _3 = uxQueueLength_8(D) * uxItemSize_9(D);
  if (_3 <= 4294967215)
    goto <bb 5>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  xQueueSizeInBytes_10 = uxQueueLength_8(D) * uxItemSize_9(D);
  # DEBUG xQueueSizeInBytes => xQueueSizeInBytes_10
  # DEBUG BEGIN_STMT
  _4 = xQueueSizeInBytes_10 + 80;
  pxNewQueue_13 = pvPortMalloc (_4);
  # DEBUG pxNewQueue => pxNewQueue_13
  # DEBUG BEGIN_STMT
  if (pxNewQueue_13 != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 6> :
  # DEBUG BEGIN_STMT
  pucQueueStorage_14 = pxNewQueue_13;
  # DEBUG pucQueueStorage => pucQueueStorage_14
  # DEBUG BEGIN_STMT
  pucQueueStorage_15 = pucQueueStorage_14 + 80;
  # DEBUG pucQueueStorage => pucQueueStorage_15
  # DEBUG BEGIN_STMT
  prvInitialiseNewQueue (uxQueueLength_8(D), uxItemSize_9(D), pucQueueStorage_15, ucQueueType_16(D), pxNewQueue_13);
  goto <bb 10>; [INV]

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

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

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

  <bb 10> :
  # pxNewQueue_5 = PHI <pxNewQueue_13(6), pxNewQueue_7(7), pxNewQueue_13(5)>
  # DEBUG pxNewQueue => pxNewQueue_5
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _19 = pxNewQueue_5;
  return _19;

}


xQueueGenericReset (struct QueueDefinition * xQueue, BaseType_t xNewQueue)
{
  struct Queue_t * const pxQueue;
  BaseType_t xReturn;
  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> :
  # DEBUG BEGIN_STMT
  xReturn_27 = 1;
  # DEBUG xReturn => xReturn_27
  # DEBUG BEGIN_STMT
  pxQueue_29 = xQueue_28(D);
  # DEBUG pxQueue => pxQueue_29
  # DEBUG BEGIN_STMT
  if (pxQueue_29 == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

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

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

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

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

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

  <bb 8> :
  # DEBUG BEGIN_STMT
  vPortEnterCritical ();
  # DEBUG BEGIN_STMT
  _6 = pxQueue_29->pcHead;
  _7 = pxQueue_29->uxLength;
  _8 = pxQueue_29->uxItemSize;
  _9 = _7 * _8;
  _10 = _6 + _9;
  pxQueue_29->u.xQueue.pcTail = _10;
  # DEBUG BEGIN_STMT
  pxQueue_29->uxMessagesWaiting ={v} 0;
  # DEBUG BEGIN_STMT
  _11 = pxQueue_29->pcHead;
  pxQueue_29->pcWriteTo = _11;
  # DEBUG BEGIN_STMT
  _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;
  # DEBUG BEGIN_STMT
  pxQueue_29->cRxLock ={v} -1;
  # DEBUG BEGIN_STMT
  pxQueue_29->cTxLock ={v} -1;
  # DEBUG BEGIN_STMT
  if (xNewQueue_38(D) == 0)
    goto <bb 9>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 9> :
  # DEBUG BEGIN_STMT
  _18 ={v} pxQueue_29->xTasksWaitingToSend.uxNumberOfItems;
  if (_18 != 0)
    goto <bb 10>; [INV]
  else
    goto <bb 13>; [INV]

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

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

  <bb 12> :
  # DEBUG BEGIN_STMT
  _22 = &pxQueue_29->xTasksWaitingToSend;
  vListInitialise (_22);
  # DEBUG BEGIN_STMT
  _23 = &pxQueue_29->xTasksWaitingToReceive;
  vListInitialise (_23);

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

  <bb 14> :
  # DEBUG BEGIN_STMT
  xReturn_46 = 0;
  # DEBUG xReturn => xReturn_46

  <bb 15> :
  # xReturn_24 = PHI <xReturn_27(13), xReturn_46(14)>
  # DEBUG xReturn => xReturn_24
  # DEBUG BEGIN_STMT
  if (xReturn_24 == 0)
    goto <bb 16>; [INV]
  else
    goto <bb 18>; [INV]

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

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

  <bb 18> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _47 = xReturn_24;
  return _47;

}


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

}


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

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

}


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

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

}