ucStreamBufferGetStreamBufferType (struct StreamBufferDef_t * xStreamBuffer)
{
  uint8_t D.6586;

  <bb 2> :
  _1 = xStreamBuffer->ucFlags;
  D.6586 = _1 & 1;

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

}


vStreamBufferSetStreamBufferNumber (struct StreamBufferDef_t * xStreamBuffer, UBaseType_t uxStreamBufferNumber)
{
  <bb 2> :
  xStreamBuffer->uxStreamBufferNumber = uxStreamBufferNumber;
  return;

}


uxStreamBufferGetStreamBufferNumber (struct StreamBufferDef_t * xStreamBuffer)
{
  UBaseType_t D.6584;

  <bb 2> :
  D.6584 = xStreamBuffer->uxStreamBufferNumber;

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

}


prvInitialiseNewStreamBuffer (struct StreamBuffer_t * const pxStreamBuffer, uint8_t * const pucBuffer, size_t xBufferSizeBytes, size_t xTriggerLevelBytes, uint8_t ucFlags)
{
  const BaseType_t xWriteValue;

  <bb 2> :
  xWriteValue = 85;
  _1 = memset (pucBuffer, xWriteValue, xBufferSizeBytes);
  if (pucBuffer != _1)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  memset (pxStreamBuffer, 0, 36);
  pxStreamBuffer->pucBuffer = pucBuffer;
  pxStreamBuffer->xLength = xBufferSizeBytes;
  pxStreamBuffer->xTriggerLevelBytes = xTriggerLevelBytes;
  pxStreamBuffer->ucFlags = ucFlags;
  return;

}


prvBytesInBuffer (const struct StreamBuffer_t * const pxStreamBuffer)
{
  size_t xCount;
  size_t D.6580;
  unsigned int D.6576;

  <bb 2> :
  _1 = pxStreamBuffer->xLength;
  _2 = pxStreamBuffer->xHead;
  xCount = _1 + _2;
  D.6576 = pxStreamBuffer->xTail;
  xCount = xCount - D.6576;
  _3 = pxStreamBuffer->xLength;
  if (xCount >= _3)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  _4 = pxStreamBuffer->xLength;
  xCount = xCount - _4;

  <bb 4> :
  D.6580 = xCount;

  <bb 5> :
<L3>:
  return D.6580;

}


prvReadBytesFromBuffer (struct StreamBuffer_t * pxStreamBuffer, uint8_t * pucData, size_t xCount, size_t xTail)
{
  size_t xFirstLength;
  size_t D.6574;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = pxStreamBuffer->xLength;
  _2 = _1 - xTail;
  xFirstLength = MIN_EXPR <xCount, _2>;
  if (xFirstLength > xCount)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  vPortRaiseBASEPRI ();

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

  <bb 8> :
  _3 = xTail + xFirstLength;
  _4 = pxStreamBuffer->xLength;
  if (_3 > _4)
    goto <bb 9>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 9> :
  vPortRaiseBASEPRI ();

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

  <bb 11> :
  _5 = pxStreamBuffer->pucBuffer;
  _6 = _5 + xTail;
  memcpy (pucData, _6, xFirstLength);
  if (xCount > xFirstLength)
    goto <bb 12>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 12> :
  _7 = pucData + xFirstLength;
  _8 = pxStreamBuffer->pucBuffer;
  _9 = xCount - xFirstLength;
  memcpy (_7, _8, _9);

  <bb 13> :
  xTail = xTail + xCount;
  _10 = pxStreamBuffer->xLength;
  if (xTail >= _10)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  _11 = pxStreamBuffer->xLength;
  xTail = xTail - _11;

  <bb 15> :
  D.6574 = xTail;

  <bb 16> :
<L14>:
  return D.6574;

}


prvWriteBytesToBuffer (struct StreamBuffer_t * const pxStreamBuffer, const uint8_t * pucData, size_t xCount, size_t xHead)
{
  size_t xFirstLength;
  size_t D.6561;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = pxStreamBuffer->xLength;
  _2 = _1 - xHead;
  xFirstLength = MIN_EXPR <xCount, _2>;
  _3 = xHead + xFirstLength;
  _4 = pxStreamBuffer->xLength;
  if (_3 > _4)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  vPortRaiseBASEPRI ();

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

  <bb 8> :
  _5 = pxStreamBuffer->pucBuffer;
  _6 = _5 + xHead;
  memcpy (_6, pucData, xFirstLength);
  if (xCount > xFirstLength)
    goto <bb 9>; [INV]
  else
    goto <bb 13>; [INV]

  <bb 9> :
  _7 = xCount - xFirstLength;
  _8 = pxStreamBuffer->xLength;
  if (_7 > _8)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

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

  <bb 12> :
  _9 = pxStreamBuffer->pucBuffer;
  _10 = pucData + xFirstLength;
  _11 = xCount - xFirstLength;
  memcpy (_9, _10, _11);

  <bb 13> :
  xHead = xHead + xCount;
  _12 = pxStreamBuffer->xLength;
  if (xHead >= _12)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  _13 = pxStreamBuffer->xLength;
  xHead = xHead - _13;

  <bb 15> :
  D.6561 = xHead;

  <bb 16> :
<L15>:
  return D.6561;

}


xStreamBufferReceiveCompletedFromISR (struct StreamBufferDef_t * xStreamBuffer, BaseType_t * pxHigherPriorityTaskWoken)
{
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  BaseType_t D.6547;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  _1 = pxStreamBuffer->xTaskWaitingToSend;
  if (_1 != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  _2 = pxStreamBuffer->xTaskWaitingToSend;
  xTaskGenericNotifyFromISR (_2, 0, 0, 0, 0B, pxHigherPriorityTaskWoken);
  pxStreamBuffer->xTaskWaitingToSend = 0B;
  xReturn = 1;
  goto <bb 8>; [INV]

  <bb 7> :
  xReturn = 0;

  <bb 8> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.6547 = xReturn;

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

}


xStreamBufferSendCompletedFromISR (struct StreamBufferDef_t * xStreamBuffer, BaseType_t * pxHigherPriorityTaskWoken)
{
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  BaseType_t D.6540;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  _1 = pxStreamBuffer->xTaskWaitingToReceive;
  if (_1 != 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  _2 = pxStreamBuffer->xTaskWaitingToReceive;
  xTaskGenericNotifyFromISR (_2, 0, 0, 0, 0B, pxHigherPriorityTaskWoken);
  pxStreamBuffer->xTaskWaitingToReceive = 0B;
  xReturn = 1;
  goto <bb 8>; [INV]

  <bb 7> :
  xReturn = 0;

  <bb 8> :
  vPortSetBASEPRI (uxSavedInterruptStatus);
  D.6540 = xReturn;

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

}


xStreamBufferIsFull (struct StreamBufferDef_t * xStreamBuffer)
{
  const struct StreamBuffer_t * const pxStreamBuffer;
  size_t xBytesToStoreMessageLength;
  BaseType_t xReturn;
  BaseType_t D.6533;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = pxStreamBuffer->ucFlags;
  _2 = (int) _1;
  _3 = _2 & 1;
  if (_3 != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  xBytesToStoreMessageLength = 4;
  goto <bb 8>; [INV]

  <bb 7> :
  xBytesToStoreMessageLength = 0;

  <bb 8> :
  _4 = xStreamBufferSpacesAvailable (xStreamBuffer);
  if (xBytesToStoreMessageLength >= _4)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 10> :
  xReturn = 0;

  <bb 11> :
  D.6533 = xReturn;

  <bb 12> :
<L9>:
  return D.6533;

}


xStreamBufferIsEmpty (struct StreamBufferDef_t * xStreamBuffer)
{
  size_t xTail;
  BaseType_t xReturn;
  const struct StreamBuffer_t * const pxStreamBuffer;
  BaseType_t D.6523;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  xTail = pxStreamBuffer->xTail;
  _1 = pxStreamBuffer->xHead;
  if (xTail == _1)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

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

  <bb 7> :
  xReturn = 0;

  <bb 8> :
  D.6523 = xReturn;

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

}


prvReadMessageFromBuffer (struct StreamBuffer_t * pxStreamBuffer, void * pvRxData, size_t xBufferLengthBytes, size_t xBytesAvailable)
{
  size_t xNextTail;
  size_t xTempNextMessageLength;
  size_t xNextMessageLength;
  size_t xCount;
  size_t D.6515;

  <bb 2> :
  xNextTail = pxStreamBuffer->xTail;
  _1 = pxStreamBuffer->ucFlags;
  _2 = (int) _1;
  _3 = _2 & 1;
  if (_3 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  xNextTail = prvReadBytesFromBuffer (pxStreamBuffer, &xTempNextMessageLength, 4, xNextTail);
  xNextMessageLength = xTempNextMessageLength;
  xBytesAvailable = xBytesAvailable + 4294967292;
  if (xNextMessageLength > xBufferLengthBytes)
    goto <bb 4>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 4> :
  xNextMessageLength = 0;
  goto <bb 6>; [INV]

  <bb 5> :
  xNextMessageLength = xBufferLengthBytes;

  <bb 6> :
  xCount = MIN_EXPR <xBytesAvailable, xNextMessageLength>;
  if (xCount != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  _4 = prvReadBytesFromBuffer (pxStreamBuffer, pvRxData, xCount, xNextTail);
  pxStreamBuffer->xTail = _4;

  <bb 8> :
  D.6515 = xCount;
  xTempNextMessageLength = {CLOBBER};

  <bb 9> :
<L9>:
  return D.6515;

}


xStreamBufferReceiveFromISR (struct StreamBufferDef_t * xStreamBuffer, void * pvRxData, size_t xBufferLengthBytes, BaseType_t * const pxHigherPriorityTaskWoken)
{
  UBaseType_t uxSavedInterruptStatus;
  size_t xBytesToStoreMessageLength;
  size_t xBytesAvailable;
  size_t xReceivedLength;
  struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6505;

  <bb 2> :
  pxStreamBuffer = xStreamBuffer;
  xReceivedLength = 0;
  if (pvRxData == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

  <bb 8> :
  _1 = pxStreamBuffer->ucFlags;
  _2 = (int) _1;
  _3 = _2 & 1;
  if (_3 != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  xBytesToStoreMessageLength = 4;
  goto <bb 11>; [INV]

  <bb 10> :
  xBytesToStoreMessageLength = 0;

  <bb 11> :
  xBytesAvailable = prvBytesInBuffer (pxStreamBuffer);
  if (xBytesAvailable > xBytesToStoreMessageLength)
    goto <bb 12>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 12> :
  xReceivedLength = prvReadMessageFromBuffer (pxStreamBuffer, pvRxData, xBufferLengthBytes, xBytesAvailable);
  if (xReceivedLength != 0)
    goto <bb 13>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 13> :
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  _4 = pxStreamBuffer->xTaskWaitingToSend;
  if (_4 != 0B)
    goto <bb 14>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 14> :
  _5 = pxStreamBuffer->xTaskWaitingToSend;
  xTaskGenericNotifyFromISR (_5, 0, 0, 0, 0B, pxHigherPriorityTaskWoken);
  pxStreamBuffer->xTaskWaitingToSend = 0B;

  <bb 15> :
  vPortSetBASEPRI (uxSavedInterruptStatus);

  <bb 16> :
  D.6505 = xReceivedLength;

  <bb 17> :
<L17>:
  return D.6505;

}


xStreamBufferNextMessageLengthBytes (struct StreamBufferDef_t * xStreamBuffer)
{
  size_t xTempReturn;
  size_t xBytesAvailable;
  size_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6487;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = pxStreamBuffer->ucFlags;
  _2 = (int) _1;
  _3 = _2 & 1;
  if (_3 != 0)
    goto <bb 6>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 6> :
  xBytesAvailable = prvBytesInBuffer (pxStreamBuffer);
  if (xBytesAvailable > 4)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  _4 = pxStreamBuffer->xTail;
  prvReadBytesFromBuffer (pxStreamBuffer, &xTempReturn, 4, _4);
  xReturn = xTempReturn;
  goto <bb 13>; [INV]

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

  <bb 9> :
  vPortRaiseBASEPRI ();

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

  <bb 11> :
  xReturn = 0;
  goto <bb 13>; [INV]

  <bb 12> :
  xReturn = 0;

  <bb 13> :
  D.6487 = xReturn;
  xTempReturn = {CLOBBER};

  <bb 14> :
<L13>:
  return D.6487;

}


xStreamBufferReceive (struct StreamBufferDef_t * xStreamBuffer, void * pvRxData, size_t xBufferLengthBytes, TickType_t xTicksToWait)
{
  size_t xBytesToStoreMessageLength;
  size_t xBytesAvailable;
  size_t xReceivedLength;
  struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6475;

  <bb 2> :
  pxStreamBuffer = xStreamBuffer;
  xReceivedLength = 0;
  if (pvRxData == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

  <bb 8> :
  _1 = pxStreamBuffer->ucFlags;
  _2 = (int) _1;
  _3 = _2 & 1;
  if (_3 != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  xBytesToStoreMessageLength = 4;
  goto <bb 11>; [INV]

  <bb 10> :
  xBytesToStoreMessageLength = 0;

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

  <bb 12> :
  vPortEnterCritical ();
  xBytesAvailable = prvBytesInBuffer (pxStreamBuffer);
  if (xBytesAvailable <= xBytesToStoreMessageLength)
    goto <bb 13>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 13> :
  xTaskGenericNotifyStateClear (0B, 0);
  _4 = pxStreamBuffer->xTaskWaitingToReceive;
  if (_4 != 0B)
    goto <bb 14>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 14> :
  vPortRaiseBASEPRI ();

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

  <bb 16> :
  _5 = xTaskGetCurrentTaskHandle ();
  pxStreamBuffer->xTaskWaitingToReceive = _5;

  <bb 17> :
  vPortExitCritical ();
  if (xBytesAvailable <= xBytesToStoreMessageLength)
    goto <bb 18>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 18> :
  xTaskGenericNotifyWait (0, 0, 0, 0B, xTicksToWait);
  pxStreamBuffer->xTaskWaitingToReceive = 0B;
  xBytesAvailable = prvBytesInBuffer (pxStreamBuffer);
  goto <bb 20>; [INV]

  <bb 19> :
  xBytesAvailable = prvBytesInBuffer (pxStreamBuffer);

  <bb 20> :
  if (xBytesAvailable > xBytesToStoreMessageLength)
    goto <bb 21>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 21> :
  xReceivedLength = prvReadMessageFromBuffer (pxStreamBuffer, pvRxData, xBufferLengthBytes, xBytesAvailable);
  if (xReceivedLength != 0)
    goto <bb 22>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 22> :
  vTaskSuspendAll ();
  _6 = pxStreamBuffer->xTaskWaitingToSend;
  if (_6 != 0B)
    goto <bb 23>; [INV]
  else
    goto <bb 24>; [INV]

  <bb 23> :
  _7 = pxStreamBuffer->xTaskWaitingToSend;
  xTaskGenericNotify (_7, 0, 0, 0, 0B);
  pxStreamBuffer->xTaskWaitingToSend = 0B;

  <bb 24> :
  xTaskResumeAll ();

  <bb 25> :
  D.6475 = xReceivedLength;

  <bb 26> :
<L29>:
  return D.6475;

}


prvWriteMessageToBuffer (struct StreamBuffer_t * const pxStreamBuffer, const void * pvTxData, size_t xDataLengthBytes, size_t xSpace, size_t xRequiredSpace)
{
  size_t xNextHead;
  size_t D.6447;

  <bb 2> :
  xNextHead = pxStreamBuffer->xHead;
  _1 = pxStreamBuffer->ucFlags;
  _2 = (int) _1;
  _3 = _2 & 1;
  if (_3 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 3> :
  if (xSpace >= xRequiredSpace)
    goto <bb 4>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 4> :
  xNextHead = prvWriteBytesToBuffer (pxStreamBuffer, &xDataLengthBytes, 4, xNextHead);
  goto <bb 7>; [INV]

  <bb 5> :
  xDataLengthBytes = 0;
  goto <bb 7>; [INV]

  <bb 6> :
  xDataLengthBytes.2_4 = xDataLengthBytes;
  _5 = MIN_EXPR <xSpace, xDataLengthBytes.2_4>;
  xDataLengthBytes = _5;

  <bb 7> :
  xDataLengthBytes.3_6 = xDataLengthBytes;
  if (xDataLengthBytes.3_6 != 0)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  xDataLengthBytes.4_7 = xDataLengthBytes;
  _8 = prvWriteBytesToBuffer (pxStreamBuffer, pvTxData, xDataLengthBytes.4_7, xNextHead);
  pxStreamBuffer->xHead = _8;

  <bb 9> :
  D.6447 = xDataLengthBytes;

  <bb 10> :
<L8>:
  return D.6447;

}


xStreamBufferSendFromISR (struct StreamBufferDef_t * xStreamBuffer, const void * pvTxData, size_t xDataLengthBytes, BaseType_t * const pxHigherPriorityTaskWoken)
{
  UBaseType_t uxSavedInterruptStatus;
  size_t xRequiredSpace;
  size_t xSpace;
  size_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6435;

  <bb 2> :
  pxStreamBuffer = xStreamBuffer;
  xRequiredSpace = xDataLengthBytes;
  if (pvTxData == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

  <bb 8> :
  _1 = pxStreamBuffer->ucFlags;
  _2 = (int) _1;
  _3 = _2 & 1;
  if (_3 != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  xRequiredSpace = xRequiredSpace + 4;

  <bb 10> :
  xSpace = xStreamBufferSpacesAvailable (pxStreamBuffer);
  xReturn = prvWriteMessageToBuffer (pxStreamBuffer, pvTxData, xDataLengthBytes, xSpace, xRequiredSpace);
  if (xReturn != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 11> :
  _4 = prvBytesInBuffer (pxStreamBuffer);
  _5 = pxStreamBuffer->xTriggerLevelBytes;
  if (_4 >= _5)
    goto <bb 12>; [INV]
  else
    goto <bb 15>; [INV]

  <bb 12> :
  uxSavedInterruptStatus = ulPortRaiseBASEPRI ();
  _6 = pxStreamBuffer->xTaskWaitingToReceive;
  if (_6 != 0B)
    goto <bb 13>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 13> :
  _7 = pxStreamBuffer->xTaskWaitingToReceive;
  xTaskGenericNotifyFromISR (_7, 0, 0, 0, 0B, pxHigherPriorityTaskWoken);
  pxStreamBuffer->xTaskWaitingToReceive = 0B;

  <bb 14> :
  vPortSetBASEPRI (uxSavedInterruptStatus);

  <bb 15> :
  D.6435 = xReturn;

  <bb 16> :
<L17>:
  return D.6435;

}


xStreamBufferSend (struct StreamBufferDef_t * xStreamBuffer, const void * pvTxData, size_t xDataLengthBytes, TickType_t xTicksToWait)
{
  size_t xMaxReportedSpace;
  struct TimeOut_t xTimeOut;
  size_t xRequiredSpace;
  size_t xSpace;
  size_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6417;

  <bb 2> :
  pxStreamBuffer = xStreamBuffer;
  xSpace = 0;
  xRequiredSpace = xDataLengthBytes;
  xMaxReportedSpace = 0;
  if (pvTxData == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  vPortRaiseBASEPRI ();

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

  <bb 8> :
  _1 = pxStreamBuffer->xLength;
  xMaxReportedSpace = _1 + 4294967295;
  _2 = pxStreamBuffer->ucFlags;
  _3 = (int) _2;
  _4 = _3 & 1;
  if (_4 != 0)
    goto <bb 9>; [INV]
  else
    goto <bb 14>; [INV]

  <bb 9> :
  xRequiredSpace = xRequiredSpace + 4;
  if (xRequiredSpace <= xDataLengthBytes)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

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

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

  <bb 13> :
  xTicksToWait = 0;
  goto <bb 16>; [INV]

  <bb 14> :
  if (xRequiredSpace > xMaxReportedSpace)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  xRequiredSpace = xMaxReportedSpace;

  <bb 16> :
  xTicksToWait.0_5 = xTicksToWait;
  if (xTicksToWait.0_5 != 0)
    goto <bb 17>; [INV]
  else
    goto <bb 26>; [INV]

  <bb 17> :
  vTaskSetTimeOutState (&xTimeOut);

  <bb 18> :
  vPortEnterCritical ();
  xSpace = xStreamBufferSpacesAvailable (pxStreamBuffer);
  if (xSpace < xRequiredSpace)
    goto <bb 19>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 19> :
  xTaskGenericNotifyStateClear (0B, 0);
  _6 = pxStreamBuffer->xTaskWaitingToSend;
  if (_6 != 0B)
    goto <bb 20>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 20> :
  vPortRaiseBASEPRI ();

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

  <bb 22> :
  _7 = xTaskGetCurrentTaskHandle ();
  pxStreamBuffer->xTaskWaitingToSend = _7;
  goto <bb 24>; [INV]

  <bb 23> :
  vPortExitCritical ();
  goto <bb 25>; [INV]

  <bb 24> :
  vPortExitCritical ();
  xTicksToWait.1_8 = xTicksToWait;
  xTaskGenericNotifyWait (0, 0, 0, 0B, xTicksToWait.1_8);
  pxStreamBuffer->xTaskWaitingToSend = 0B;
  _9 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_9 == 0)
    goto <bb 18>; [INV]
  else
    goto <bb 25>; [INV]

  <bb 25> :

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

  <bb 27> :
  xSpace = xStreamBufferSpacesAvailable (pxStreamBuffer);

  <bb 28> :
  xReturn = prvWriteMessageToBuffer (pxStreamBuffer, pvTxData, xDataLengthBytes, xSpace, xRequiredSpace);
  if (xReturn != 0)
    goto <bb 29>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 29> :
  _10 = prvBytesInBuffer (pxStreamBuffer);
  _11 = pxStreamBuffer->xTriggerLevelBytes;
  if (_10 >= _11)
    goto <bb 30>; [INV]
  else
    goto <bb 33>; [INV]

  <bb 30> :
  vTaskSuspendAll ();
  _12 = pxStreamBuffer->xTaskWaitingToReceive;
  if (_12 != 0B)
    goto <bb 31>; [INV]
  else
    goto <bb 32>; [INV]

  <bb 31> :
  _13 = pxStreamBuffer->xTaskWaitingToReceive;
  xTaskGenericNotify (_13, 0, 0, 0, 0B);
  pxStreamBuffer->xTaskWaitingToReceive = 0B;

  <bb 32> :
  xTaskResumeAll ();

  <bb 33> :
  D.6417 = xReturn;
  xTimeOut = {CLOBBER};

  <bb 34> :
<L41>:
  return D.6417;

}


xStreamBufferBytesAvailable (struct StreamBufferDef_t * xStreamBuffer)
{
  size_t xReturn;
  const struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6381;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  xReturn = prvBytesInBuffer (pxStreamBuffer);
  D.6381 = xReturn;

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

}


xStreamBufferSpacesAvailable (struct StreamBufferDef_t * xStreamBuffer)
{
  size_t xOriginalTail;
  size_t xSpace;
  const struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6377;
  unsigned int D.6373;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  xOriginalTail = pxStreamBuffer->xTail;
  _1 = pxStreamBuffer->xLength;
  _2 = pxStreamBuffer->xTail;
  xSpace = _1 + _2;
  D.6373 = pxStreamBuffer->xHead;
  xSpace = xSpace - D.6373;
  _3 = pxStreamBuffer->xTail;
  if (xOriginalTail != _3)
    goto <bb 5>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 6> :
  xSpace = xSpace + 4294967295;
  _4 = pxStreamBuffer->xLength;
  if (xSpace >= _4)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  _5 = pxStreamBuffer->xLength;
  xSpace = xSpace - _5;

  <bb 8> :
  D.6377 = xSpace;

  <bb 9> :
<L8>:
  return D.6377;

}


xStreamBufferSetTriggerLevel (struct StreamBufferDef_t * xStreamBuffer, size_t xTriggerLevel)
{
  BaseType_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  BaseType_t D.6369;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

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

  <bb 6> :
  xTriggerLevel = 1;

  <bb 7> :
  _1 = pxStreamBuffer->xLength;
  if (xTriggerLevel < _1)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  pxStreamBuffer->xTriggerLevelBytes = xTriggerLevel;
  xReturn = 1;
  goto <bb 10>; [INV]

  <bb 9> :
  xReturn = 0;

  <bb 10> :
  D.6369 = xReturn;

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

}


xStreamBufferReset (struct StreamBufferDef_t * xStreamBuffer)
{
  UBaseType_t uxStreamBufferNumber;
  BaseType_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  BaseType_t D.6360;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  uxStreamBufferNumber = pxStreamBuffer->uxStreamBufferNumber;
  vPortEnterCritical ();
  _1 = pxStreamBuffer->xTaskWaitingToReceive;
  if (_1 == 0B)
    goto <bb 6>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 6> :
  _2 = pxStreamBuffer->xTaskWaitingToSend;
  if (_2 == 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  _3 = pxStreamBuffer->pucBuffer;
  _4 = pxStreamBuffer->xLength;
  _5 = pxStreamBuffer->xTriggerLevelBytes;
  _6 = pxStreamBuffer->ucFlags;
  prvInitialiseNewStreamBuffer (pxStreamBuffer, _3, _4, _5, _6);
  xReturn = 1;
  pxStreamBuffer->uxStreamBufferNumber = uxStreamBufferNumber;

  <bb 8> :
  vPortExitCritical ();
  D.6360 = xReturn;

  <bb 9> :
<L7>:
  return D.6360;

}


vStreamBufferDelete (struct StreamBufferDef_t * xStreamBuffer)
{
  struct StreamBuffer_t * pxStreamBuffer;

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

  <bb 3> :
  vPortRaiseBASEPRI ();

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

  <bb 5> :
  _1 = pxStreamBuffer->ucFlags;
  _2 = (int) _1;
  _3 = _2 & 2;
  if (_3 == 0)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 6> :
  vPortFree (pxStreamBuffer);
  goto <bb 8>; [INV]

  <bb 7> :
  memset (pxStreamBuffer, 0, 36);

  <bb 8> :
  return;

}


xStreamBufferGenericCreate (size_t xBufferSizeBytes, size_t xTriggerLevelBytes, BaseType_t xIsMessageBuffer)
{
  uint8_t ucFlags;
  uint8_t * pucAllocatedMemory;
  struct StreamBufferDef_t * D.6347;

  <bb 2> :
  if (xIsMessageBuffer == 1)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 3> :
  ucFlags = 1;
  if (xBufferSizeBytes <= 4)
    goto <bb 4>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 4> :
  vPortRaiseBASEPRI ();

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

  <bb 6> :
  ucFlags = 0;
  if (xBufferSizeBytes == 0)
    goto <bb 7>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 7> :
  vPortRaiseBASEPRI ();

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

  <bb 9> :
  if (xTriggerLevelBytes > xBufferSizeBytes)
    goto <bb 10>; [INV]
  else
    goto <bb 12>; [INV]

  <bb 10> :
  vPortRaiseBASEPRI ();

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

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

  <bb 13> :
  xTriggerLevelBytes = 1;

  <bb 14> :
  if (xBufferSizeBytes <= 4294967258)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  xBufferSizeBytes = xBufferSizeBytes + 1;
  _1 = xBufferSizeBytes + 36;
  pucAllocatedMemory = pvPortMalloc (_1);
  goto <bb 17>; [INV]

  <bb 16> :
  pucAllocatedMemory = 0B;

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

  <bb 18> :
  _2 = pucAllocatedMemory + 36;
  prvInitialiseNewStreamBuffer (pucAllocatedMemory, _2, xBufferSizeBytes, xTriggerLevelBytes, ucFlags);

  <bb 19> :
  D.6347 = pucAllocatedMemory;

  <bb 20> :
<L20>:
  return D.6347;

}


__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.6437;

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

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

}


__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;

}