ucStreamBufferGetStreamBufferType (struct StreamBufferDef_t * xStreamBuffer)
{
  uint8_t D.6587;
  unsigned char _1;
  uint8_t _4;

  <bb 2> :
  _1 = xStreamBuffer_3(D)->ucFlags;
  _4 = _1 & 1;

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

}


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

}


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

  <bb 2> :
  _3 = xStreamBuffer_2(D)->uxStreamBufferNumber;

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

}


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

  <bb 2> :
  xWriteValue_2 = 85;
  _1 = memset (pucBuffer_4(D), xWriteValue_2, xBufferSizeBytes_5(D));
  if (pucBuffer_4(D) != _1)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

  <bb 6> :
  memset (pxStreamBuffer_7(D), 0, 36);
  pxStreamBuffer_7(D)->pucBuffer = pucBuffer_4(D);
  pxStreamBuffer_7(D)->xLength = xBufferSizeBytes_5(D);
  pxStreamBuffer_7(D)->xTriggerLevelBytes = xTriggerLevelBytes_11(D);
  pxStreamBuffer_7(D)->ucFlags = ucFlags_13(D);
  return;

}


prvBytesInBuffer (const struct StreamBuffer_t * const pxStreamBuffer)
{
  size_t xCount;
  size_t D.6581;
  unsigned int D.6577;
  unsigned int _1;
  unsigned int _2;
  unsigned int _3;
  unsigned int _4;
  unsigned int _9;
  size_t _12;

  <bb 2> :
  _1 = pxStreamBuffer_7(D)->xLength;
  _2 ={v} pxStreamBuffer_7(D)->xHead;
  xCount_8 = _1 + _2;
  _9 ={v} pxStreamBuffer_7(D)->xTail;
  xCount_10 = xCount_8 - _9;
  _3 = pxStreamBuffer_7(D)->xLength;
  if (xCount_10 >= _3)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  _4 = pxStreamBuffer_7(D)->xLength;
  xCount_11 = xCount_10 - _4;

  <bb 4> :
  # xCount_5 = PHI <xCount_10(2), xCount_11(3)>
  _12 = xCount_5;

  <bb 5> :
<L3>:
  return _12;

}


prvReadBytesFromBuffer (struct StreamBuffer_t * pxStreamBuffer, uint8_t * pucData, size_t xCount, size_t xTail)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  size_t xFirstLength;
  size_t D.6575;
  unsigned int _1;
  unsigned int _2;
  unsigned int _3;
  unsigned int _4;
  uint8_t * _5;
  uint8_t * _6;
  uint8_t * _7;
  uint8_t * _8;
  unsigned int _9;
  unsigned int _10;
  unsigned int _11;
  size_t _24;

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

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

  <bb 4> :

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

  <bb 6> :
  _1 = pxStreamBuffer_16(D)->xLength;
  _2 = _1 - xTail_17(D);
  xFirstLength_18 = MIN_EXPR <xCount_14(D), _2>;
  if (xFirstLength_18 > xCount_14(D))
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 8> :

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

  <bb 10> :
  _3 = xTail_17(D) + xFirstLength_18;
  _4 = pxStreamBuffer_16(D)->xLength;
  if (_3 > _4)
    goto <bb 11>; [INV]
  else
    goto <bb 14>; [INV]

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

  <bb 12> :

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

  <bb 14> :
  _5 = pxStreamBuffer_16(D)->pucBuffer;
  _6 = _5 + xTail_17(D);
  memcpy (pucData_19(D), _6, xFirstLength_18);
  if (xCount_14(D) > xFirstLength_18)
    goto <bb 15>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 15> :
  _7 = pucData_19(D) + xFirstLength_18;
  _8 = pxStreamBuffer_16(D)->pucBuffer;
  _9 = xCount_14(D) - xFirstLength_18;
  memcpy (_7, _8, _9);

  <bb 16> :
  xTail_22 = xTail_17(D) + xCount_14(D);
  _10 = pxStreamBuffer_16(D)->xLength;
  if (xTail_22 >= _10)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  _11 = pxStreamBuffer_16(D)->xLength;
  xTail_23 = xTail_22 - _11;

  <bb 18> :
  # xTail_12 = PHI <xTail_22(16), xTail_23(17)>
  _24 = xTail_12;

  <bb 19> :
<L14>:
  return _24;

}


prvWriteBytesToBuffer (struct StreamBuffer_t * const pxStreamBuffer, const uint8_t * pucData, size_t xCount, size_t xHead)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  size_t xFirstLength;
  size_t D.6562;
  unsigned int _1;
  unsigned int _2;
  unsigned int _3;
  unsigned int _4;
  uint8_t * _5;
  uint8_t * _6;
  unsigned int _7;
  unsigned int _8;
  uint8_t * _9;
  const uint8_t * _10;
  unsigned int _11;
  unsigned int _12;
  unsigned int _13;
  size_t _26;

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

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

  <bb 4> :

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

  <bb 6> :
  _1 = pxStreamBuffer_18(D)->xLength;
  _2 = _1 - xHead_19(D);
  xFirstLength_20 = MIN_EXPR <xCount_16(D), _2>;
  _3 = xHead_19(D) + xFirstLength_20;
  _4 = pxStreamBuffer_18(D)->xLength;
  if (_3 > _4)
    goto <bb 7>; [INV]
  else
    goto <bb 10>; [INV]

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

  <bb 8> :

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

  <bb 10> :
  _5 = pxStreamBuffer_18(D)->pucBuffer;
  _6 = _5 + xHead_19(D);
  memcpy (_6, pucData_21(D), xFirstLength_20);
  if (xCount_16(D) > xFirstLength_20)
    goto <bb 11>; [INV]
  else
    goto <bb 16>; [INV]

  <bb 11> :
  _7 = xCount_16(D) - xFirstLength_20;
  _8 = pxStreamBuffer_18(D)->xLength;
  if (_7 > _8)
    goto <bb 12>; [INV]
  else
    goto <bb 15>; [INV]

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

  <bb 13> :

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

  <bb 15> :
  _9 = pxStreamBuffer_18(D)->pucBuffer;
  _10 = pucData_21(D) + xFirstLength_20;
  _11 = xCount_16(D) - xFirstLength_20;
  memcpy (_9, _10, _11);

  <bb 16> :
  xHead_24 = xHead_19(D) + xCount_16(D);
  _12 = pxStreamBuffer_18(D)->xLength;
  if (xHead_24 >= _12)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  _13 = pxStreamBuffer_18(D)->xLength;
  xHead_25 = xHead_24 - _13;

  <bb 18> :
  # xHead_14 = PHI <xHead_24(16), xHead_25(17)>
  _26 = xHead_14;

  <bb 19> :
<L15>:
  return _26;

}


xStreamBufferReceiveCompletedFromISR (struct StreamBufferDef_t * xStreamBuffer, BaseType_t * pxHigherPriorityTaskWoken)
{
  uint32_t ulNewMaskValue;
  uint32_t D.6632;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.6631;
  uint32_t ulNewBASEPRI;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  BaseType_t D.6548;
  struct tskTaskControlBlock * _1;
  struct tskTaskControlBlock * _2;
  BaseType_t _14;
  long unsigned int _18;

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

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

  <bb 4> :

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

  <bb 6> :
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_16, "=r" ulNewBASEPRI_17 : "i" 16 : "memory");
  _18 = ulOriginalBASEPRI_16;

  <bb 7> :
<L7>:
  _21 = _18;

  <bb 8> :
  uxSavedInterruptStatus_8 = _21;
  _1 ={v} pxStreamBuffer_6->xTaskWaitingToSend;
  if (_1 != 0B)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  _2 ={v} pxStreamBuffer_6->xTaskWaitingToSend;
  xTaskGenericNotifyFromISR (_2, 0, 0, 0, 0B, pxHigherPriorityTaskWoken_10(D));
  pxStreamBuffer_6->xTaskWaitingToSend ={v} 0B;
  xReturn_13 = 1;
  goto <bb 11>; [INV]

  <bb 10> :
  xReturn_9 = 0;

  <bb 11> :
  # xReturn_3 = PHI <xReturn_13(9), xReturn_9(10)>
  ulNewMaskValue_19 = uxSavedInterruptStatus_8;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_19 : "memory");

  <bb 12> :
  _14 = xReturn_3;

  <bb 13> :
<L6>:
  return _14;

}


xStreamBufferSendCompletedFromISR (struct StreamBufferDef_t * xStreamBuffer, BaseType_t * pxHigherPriorityTaskWoken)
{
  uint32_t ulNewMaskValue;
  uint32_t D.6625;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.6624;
  uint32_t ulNewBASEPRI;
  UBaseType_t uxSavedInterruptStatus;
  BaseType_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  BaseType_t D.6541;
  struct tskTaskControlBlock * _1;
  struct tskTaskControlBlock * _2;
  BaseType_t _14;
  long unsigned int _18;

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

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

  <bb 4> :

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

  <bb 6> :
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_16, "=r" ulNewBASEPRI_17 : "i" 16 : "memory");
  _18 = ulOriginalBASEPRI_16;

  <bb 7> :
<L7>:
  _21 = _18;

  <bb 8> :
  uxSavedInterruptStatus_8 = _21;
  _1 ={v} pxStreamBuffer_6->xTaskWaitingToReceive;
  if (_1 != 0B)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  _2 ={v} pxStreamBuffer_6->xTaskWaitingToReceive;
  xTaskGenericNotifyFromISR (_2, 0, 0, 0, 0B, pxHigherPriorityTaskWoken_10(D));
  pxStreamBuffer_6->xTaskWaitingToReceive ={v} 0B;
  xReturn_13 = 1;
  goto <bb 11>; [INV]

  <bb 10> :
  xReturn_9 = 0;

  <bb 11> :
  # xReturn_3 = PHI <xReturn_13(9), xReturn_9(10)>
  ulNewMaskValue_19 = uxSavedInterruptStatus_8;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_19 : "memory");

  <bb 12> :
  _14 = xReturn_3;

  <bb 13> :
<L6>:
  return _14;

}


xStreamBufferIsFull (struct StreamBufferDef_t * xStreamBuffer)
{
  uint32_t ulNewBASEPRI;
  const struct StreamBuffer_t * const pxStreamBuffer;
  size_t xBytesToStoreMessageLength;
  BaseType_t xReturn;
  BaseType_t D.6534;
  unsigned char _1;
  int _2;
  int _3;
  unsigned int _4;
  BaseType_t _15;

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

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

  <bb 4> :

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

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

  <bb 7> :
  xBytesToStoreMessageLength_11 = 4;
  goto <bb 9>; [INV]

  <bb 8> :
  xBytesToStoreMessageLength_10 = 0;

  <bb 9> :
  # xBytesToStoreMessageLength_6 = PHI <xBytesToStoreMessageLength_11(7), xBytesToStoreMessageLength_10(8)>
  _4 = xStreamBufferSpacesAvailable (xStreamBuffer_7(D));
  if (xBytesToStoreMessageLength_6 >= _4)
    goto <bb 10>; [INV]
  else
    goto <bb 11>; [INV]

  <bb 10> :
  xReturn_14 = 1;
  goto <bb 12>; [INV]

  <bb 11> :
  xReturn_13 = 0;

  <bb 12> :
  # xReturn_5 = PHI <xReturn_14(10), xReturn_13(11)>
  _15 = xReturn_5;

  <bb 13> :
<L9>:
  return _15;

}


xStreamBufferIsEmpty (struct StreamBufferDef_t * xStreamBuffer)
{
  uint32_t ulNewBASEPRI;
  size_t xTail;
  BaseType_t xReturn;
  const struct StreamBuffer_t * const pxStreamBuffer;
  BaseType_t D.6524;
  unsigned int _1;
  BaseType_t _9;

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

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

  <bb 4> :

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

  <bb 6> :
  xTail_6 ={v} pxStreamBuffer_4->xTail;
  _1 ={v} pxStreamBuffer_4->xHead;
  if (xTail_6 == _1)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

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

  <bb 8> :
  xReturn_7 = 0;

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

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

}


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.6516;
  unsigned char _1;
  int _2;
  int _3;
  unsigned int _4;
  size_t _25;

  <bb 2> :
  xNextTail_12 ={v} pxStreamBuffer_11(D)->xTail;
  _1 = pxStreamBuffer_11(D)->ucFlags;
  _2 = (int) _1;
  _3 = _2 & 1;
  if (_3 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 3> :
  xNextTail_17 = prvReadBytesFromBuffer (pxStreamBuffer_11(D), &xTempNextMessageLength, 4, xNextTail_12);
  xNextMessageLength_18 = xTempNextMessageLength;
  xBytesAvailable_19 = xBytesAvailable_15(D) + 4294967292;
  if (xNextMessageLength_18 > xBufferLengthBytes_13(D))
    goto <bb 4>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 5> :
  xNextMessageLength_14 = xBufferLengthBytes_13(D);

  <bb 6> :
  # xBytesAvailable_5 = PHI <xBytesAvailable_19(4), xBytesAvailable_15(D)(5), xBytesAvailable_19(3)>
  # xNextMessageLength_6 = PHI <xNextMessageLength_20(4), xNextMessageLength_14(5), xNextMessageLength_18(3)>
  # xNextTail_7 = PHI <xNextTail_17(4), xNextTail_12(5), xNextTail_17(3)>
  xCount_21 = MIN_EXPR <xBytesAvailable_5, xNextMessageLength_6>;
  if (xCount_21 != 0)
    goto <bb 7>; [INV]
  else
    goto <bb 8>; [INV]

  <bb 7> :
  _4 = prvReadBytesFromBuffer (pxStreamBuffer_11(D), pvRxData_22(D), xCount_21, xNextTail_7);
  pxStreamBuffer_11(D)->xTail ={v} _4;

  <bb 8> :
  _25 = xCount_21;
  xTempNextMessageLength ={v} {CLOBBER};

  <bb 9> :
<L9>:
  return _25;

}


xStreamBufferReceiveFromISR (struct StreamBufferDef_t * xStreamBuffer, void * pvRxData, size_t xBufferLengthBytes, BaseType_t * const pxHigherPriorityTaskWoken)
{
  uint32_t ulNewMaskValue;
  uint32_t D.6664;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.6663;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  UBaseType_t uxSavedInterruptStatus;
  size_t xBytesToStoreMessageLength;
  size_t xBytesAvailable;
  size_t xReceivedLength;
  struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6506;
  unsigned char _1;
  int _2;
  int _3;
  struct tskTaskControlBlock * _4;
  struct tskTaskControlBlock * _5;
  size_t _26;
  long unsigned int _31;

  <bb 2> :
  pxStreamBuffer_11 = xStreamBuffer_10(D);
  xReceivedLength_12 = 0;
  if (pvRxData_13(D) == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

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

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

  <bb 8> :

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

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

  <bb 11> :
  xBytesToStoreMessageLength_16 = 4;
  goto <bb 13>; [INV]

  <bb 12> :
  xBytesToStoreMessageLength_15 = 0;

  <bb 13> :
  # xBytesToStoreMessageLength_7 = PHI <xBytesToStoreMessageLength_16(11), xBytesToStoreMessageLength_15(12)>
  xBytesAvailable_18 = prvBytesInBuffer (pxStreamBuffer_11);
  if (xBytesAvailable_18 > xBytesToStoreMessageLength_7)
    goto <bb 14>; [INV]
  else
    goto <bb 21>; [INV]

  <bb 14> :
  xReceivedLength_21 = prvReadMessageFromBuffer (pxStreamBuffer_11, pvRxData_13(D), xBufferLengthBytes_19(D), xBytesAvailable_18);
  if (xReceivedLength_21 != 0)
    goto <bb 15>; [INV]
  else
    goto <bb 21>; [INV]

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

  <bb 16> :
<L18>:
  _34 = _31;

  <bb 17> :
  uxSavedInterruptStatus_22 = _34;
  _4 ={v} pxStreamBuffer_11->xTaskWaitingToSend;
  if (_4 != 0B)
    goto <bb 18>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 18> :
  _5 ={v} pxStreamBuffer_11->xTaskWaitingToSend;
  xTaskGenericNotifyFromISR (_5, 0, 0, 0, 0B, pxHigherPriorityTaskWoken_23(D));
  pxStreamBuffer_11->xTaskWaitingToSend ={v} 0B;

  <bb 19> :
  ulNewMaskValue_32 = uxSavedInterruptStatus_22;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_32 : "memory");

  <bb 20> :

  <bb 21> :
  # xReceivedLength_6 = PHI <xReceivedLength_12(13), xReceivedLength_21(20), xReceivedLength_21(14)>
  _26 = xReceivedLength_6;

  <bb 22> :
<L17>:
  return _26;

}


xStreamBufferNextMessageLengthBytes (struct StreamBufferDef_t * xStreamBuffer)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  size_t xTempReturn;
  size_t xBytesAvailable;
  size_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6488;
  unsigned char _1;
  int _2;
  int _3;
  unsigned int _4;
  size_t _16;

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

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

  <bb 4> :

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

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

  <bb 7> :
  xBytesAvailable_12 = prvBytesInBuffer (pxStreamBuffer_8);
  if (xBytesAvailable_12 > 4)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  _4 ={v} pxStreamBuffer_8->xTail;
  prvReadBytesFromBuffer (pxStreamBuffer_8, &xTempReturn, 4, _4);
  xReturn_15 = xTempReturn;
  goto <bb 15>; [INV]

  <bb 9> :
  if (xBytesAvailable_12 != 0)
    goto <bb 10>; [INV]
  else
    goto <bb 13>; [INV]

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

  <bb 11> :

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

  <bb 13> :
  xReturn_13 = 0;
  goto <bb 15>; [INV]

  <bb 14> :
  xReturn_10 = 0;

  <bb 15> :
  # xReturn_5 = PHI <xReturn_13(13), xReturn_10(14), xReturn_15(8)>
  _16 = xReturn_5;
  xTempReturn ={v} {CLOBBER};

  <bb 16> :
<L13>:
  return _16;

}


xStreamBufferReceive (struct StreamBufferDef_t * xStreamBuffer, void * pvRxData, size_t xBufferLengthBytes, TickType_t xTicksToWait)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  size_t xBytesToStoreMessageLength;
  size_t xBytesAvailable;
  size_t xReceivedLength;
  struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6476;
  unsigned char _1;
  int _2;
  int _3;
  struct tskTaskControlBlock * _4;
  struct tskTaskControlBlock * _5;
  struct tskTaskControlBlock * _6;
  struct tskTaskControlBlock * _7;
  size_t _43;

  <bb 2> :
  pxStreamBuffer_16 = xStreamBuffer_15(D);
  xReceivedLength_17 = 0;
  if (pvRxData_18(D) == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

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

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

  <bb 8> :

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

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

  <bb 11> :
  xBytesToStoreMessageLength_21 = 4;
  goto <bb 13>; [INV]

  <bb 12> :
  xBytesToStoreMessageLength_20 = 0;

  <bb 13> :
  # xBytesToStoreMessageLength_10 = PHI <xBytesToStoreMessageLength_21(11), xBytesToStoreMessageLength_20(12)>
  if (xTicksToWait_22(D) != 0)
    goto <bb 14>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 14> :
  vPortEnterCritical ();
  xBytesAvailable_27 = prvBytesInBuffer (pxStreamBuffer_16);
  if (xBytesAvailable_27 <= xBytesToStoreMessageLength_10)
    goto <bb 15>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 15> :
  xTaskGenericNotifyStateClear (0B, 0);
  _4 ={v} pxStreamBuffer_16->xTaskWaitingToReceive;
  if (_4 != 0B)
    goto <bb 16>; [INV]
  else
    goto <bb 19>; [INV]

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

  <bb 17> :

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

  <bb 19> :
  _5 = xTaskGetCurrentTaskHandle ();
  pxStreamBuffer_16->xTaskWaitingToReceive ={v} _5;

  <bb 20> :
  vPortExitCritical ();
  if (xBytesAvailable_27 <= xBytesToStoreMessageLength_10)
    goto <bb 21>; [INV]
  else
    goto <bb 23>; [INV]

  <bb 21> :
  xTaskGenericNotifyWait (0, 0, 0, 0B, xTicksToWait_22(D));
  pxStreamBuffer_16->xTaskWaitingToReceive ={v} 0B;
  xBytesAvailable_35 = prvBytesInBuffer (pxStreamBuffer_16);
  goto <bb 23>; [INV]

  <bb 22> :
  xBytesAvailable_24 = prvBytesInBuffer (pxStreamBuffer_16);

  <bb 23> :
  # xBytesAvailable_9 = PHI <xBytesAvailable_35(21), xBytesAvailable_24(22), xBytesAvailable_27(20)>
  if (xBytesAvailable_9 > xBytesToStoreMessageLength_10)
    goto <bb 24>; [INV]
  else
    goto <bb 28>; [INV]

  <bb 24> :
  xReceivedLength_38 = prvReadMessageFromBuffer (pxStreamBuffer_16, pvRxData_18(D), xBufferLengthBytes_36(D), xBytesAvailable_9);
  if (xReceivedLength_38 != 0)
    goto <bb 25>; [INV]
  else
    goto <bb 28>; [INV]

  <bb 25> :
  vTaskSuspendAll ();
  _6 ={v} pxStreamBuffer_16->xTaskWaitingToSend;
  if (_6 != 0B)
    goto <bb 26>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 26> :
  _7 ={v} pxStreamBuffer_16->xTaskWaitingToSend;
  xTaskGenericNotify (_7, 0, 0, 0, 0B);
  pxStreamBuffer_16->xTaskWaitingToSend ={v} 0B;

  <bb 27> :
  xTaskResumeAll ();

  <bb 28> :
  # xReceivedLength_8 = PHI <xReceivedLength_17(23), xReceivedLength_38(27), xReceivedLength_38(24)>
  _43 = xReceivedLength_8;

  <bb 29> :
<L29>:
  return _43;

}


prvWriteMessageToBuffer (struct StreamBuffer_t * const pxStreamBuffer, const void * pvTxData, size_t xDataLengthBytes, size_t xSpace, size_t xRequiredSpace)
{
  size_t xNextHead;
  size_t D.6448;
  unsigned char _1;
  int _2;
  int _3;
  unsigned int xDataLengthBytes.2_4;
  unsigned int _5;
  unsigned int xDataLengthBytes.3_6;
  unsigned int xDataLengthBytes.4_7;
  unsigned int _8;
  size_t _24;

  <bb 2> :
  xNextHead_14 ={v} pxStreamBuffer_13(D)->xHead;
  _1 = pxStreamBuffer_13(D)->ucFlags;
  _2 = (int) _1;
  _3 = _2 & 1;
  if (_3 != 0)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

  <bb 3> :
  if (xSpace_15(D) >= xRequiredSpace_17(D))
    goto <bb 4>; [INV]
  else
    goto <bb 5>; [INV]

  <bb 4> :
  xNextHead_20 = prvWriteBytesToBuffer (pxStreamBuffer_13(D), &xDataLengthBytes, 4, xNextHead_14);
  goto <bb 7>; [INV]

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

  <bb 6> :
  xDataLengthBytes.2_4 = xDataLengthBytes;
  _5 = MIN_EXPR <xSpace_15(D), xDataLengthBytes.2_4>;
  xDataLengthBytes = _5;

  <bb 7> :
  # xNextHead_9 = PHI <xNextHead_14(5), xNextHead_14(6), xNextHead_20(4)>
  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_13(D), pvTxData_21(D), xDataLengthBytes.4_7, xNextHead_9);
  pxStreamBuffer_13(D)->xHead ={v} _8;

  <bb 9> :
  _24 = xDataLengthBytes;

  <bb 10> :
<L8>:
  return _24;

}


xStreamBufferSendFromISR (struct StreamBufferDef_t * xStreamBuffer, const void * pvTxData, size_t xDataLengthBytes, BaseType_t * const pxHigherPriorityTaskWoken)
{
  uint32_t ulNewMaskValue;
  uint32_t D.6651;
  uint32_t ulOriginalBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t D.6650;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  UBaseType_t uxSavedInterruptStatus;
  size_t xRequiredSpace;
  size_t xSpace;
  size_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6436;
  unsigned char _1;
  int _2;
  int _3;
  unsigned int _4;
  unsigned int _5;
  struct tskTaskControlBlock * _6;
  struct tskTaskControlBlock * _7;
  size_t _27;
  long unsigned int _32;

  <bb 2> :
  pxStreamBuffer_12 = xStreamBuffer_11(D);
  xRequiredSpace_14 = xDataLengthBytes_13(D);
  if (pvTxData_15(D) == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

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

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

  <bb 8> :

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

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

  <bb 11> :
  xRequiredSpace_17 = xRequiredSpace_14 + 4;

  <bb 12> :
  # xRequiredSpace_8 = PHI <xRequiredSpace_14(10), xRequiredSpace_17(11)>
  xSpace_19 = xStreamBufferSpacesAvailable (pxStreamBuffer_12);
  xReturn_21 = prvWriteMessageToBuffer (pxStreamBuffer_12, pvTxData_15(D), xDataLengthBytes_13(D), xSpace_19, xRequiredSpace_8);
  if (xReturn_21 != 0)
    goto <bb 13>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 13> :
  _4 = prvBytesInBuffer (pxStreamBuffer_12);
  _5 = pxStreamBuffer_12->xTriggerLevelBytes;
  if (_4 >= _5)
    goto <bb 14>; [INV]
  else
    goto <bb 20>; [INV]

  <bb 14> :
  __asm__ __volatile__("	mrs %0, basepri											
	mov %1, %2												
	msr basepri, %1											
	isb														
	dsb														
" : "=r" ulOriginalBASEPRI_30, "=r" ulNewBASEPRI_31 : "i" 16 : "memory");
  _32 = ulOriginalBASEPRI_30;

  <bb 15> :
<L18>:
  _35 = _32;

  <bb 16> :
  uxSavedInterruptStatus_23 = _35;
  _6 ={v} pxStreamBuffer_12->xTaskWaitingToReceive;
  if (_6 != 0B)
    goto <bb 17>; [INV]
  else
    goto <bb 18>; [INV]

  <bb 17> :
  _7 ={v} pxStreamBuffer_12->xTaskWaitingToReceive;
  xTaskGenericNotifyFromISR (_7, 0, 0, 0, 0B, pxHigherPriorityTaskWoken_24(D));
  pxStreamBuffer_12->xTaskWaitingToReceive ={v} 0B;

  <bb 18> :
  ulNewMaskValue_33 = uxSavedInterruptStatus_23;
  __asm__ __volatile__("	msr basepri, %0	" :  : "r" ulNewMaskValue_33 : "memory");

  <bb 19> :

  <bb 20> :
  _27 = xReturn_21;

  <bb 21> :
<L17>:
  return _27;

}


xStreamBufferSend (struct StreamBufferDef_t * xStreamBuffer, const void * pvTxData, size_t xDataLengthBytes, TickType_t xTicksToWait)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  size_t xMaxReportedSpace;
  struct TimeOut_t xTimeOut;
  size_t xRequiredSpace;
  size_t xSpace;
  size_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6418;
  unsigned int _1;
  unsigned char _2;
  int _3;
  int _4;
  long unsigned int xTicksToWait.0_5;
  struct tskTaskControlBlock * _6;
  struct tskTaskControlBlock * _7;
  long unsigned int xTicksToWait.1_8;
  long int _9;
  unsigned int _10;
  unsigned int _11;
  struct tskTaskControlBlock * _12;
  struct tskTaskControlBlock * _13;
  size_t _57;

  <bb 2> :
  pxStreamBuffer_25 = xStreamBuffer_24(D);
  xSpace_26 = 0;
  xRequiredSpace_28 = xDataLengthBytes_27(D);
  xMaxReportedSpace_29 = 0;
  if (pvTxData_30(D) == 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 6>; [INV]

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

  <bb 4> :

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

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

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

  <bb 8> :

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

  <bb 10> :
  _1 = pxStreamBuffer_25->xLength;
  xMaxReportedSpace_32 = _1 + 4294967295;
  _2 = pxStreamBuffer_25->ucFlags;
  _3 = (int) _2;
  _4 = _3 & 1;
  if (_4 != 0)
    goto <bb 11>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 11> :
  xRequiredSpace_34 = xRequiredSpace_28 + 4;
  if (xRequiredSpace_34 <= xDataLengthBytes_27(D))
    goto <bb 12>; [INV]
  else
    goto <bb 15>; [INV]

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

  <bb 13> :

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

  <bb 15> :
  if (xRequiredSpace_34 > xMaxReportedSpace_32)
    goto <bb 16>; [INV]
  else
    goto <bb 19>; [INV]

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

  <bb 17> :
  if (xRequiredSpace_28 > xMaxReportedSpace_32)
    goto <bb 18>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 18> :
  xRequiredSpace_33 = xMaxReportedSpace_32;

  <bb 19> :
  # xRequiredSpace_16 = PHI <xRequiredSpace_34(16), xRequiredSpace_28(17), xRequiredSpace_33(18), xRequiredSpace_34(15)>
  xTicksToWait.0_5 = xTicksToWait;
  if (xTicksToWait.0_5 != 0)
    goto <bb 20>; [INV]
  else
    goto <bb 30>; [INV]

  <bb 20> :
  vTaskSetTimeOutState (&xTimeOut);

  <bb 21> :
  vPortEnterCritical ();
  xSpace_39 = xStreamBufferSpacesAvailable (pxStreamBuffer_25);
  if (xSpace_39 < xRequiredSpace_16)
    goto <bb 22>; [INV]
  else
    goto <bb 27>; [INV]

  <bb 22> :
  xTaskGenericNotifyStateClear (0B, 0);
  _6 ={v} pxStreamBuffer_25->xTaskWaitingToSend;
  if (_6 != 0B)
    goto <bb 23>; [INV]
  else
    goto <bb 26>; [INV]

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

  <bb 24> :

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

  <bb 26> :
  _7 = xTaskGetCurrentTaskHandle ();
  pxStreamBuffer_25->xTaskWaitingToSend ={v} _7;
  goto <bb 28>; [INV]

  <bb 27> :
  vPortExitCritical ();
  goto <bb 29>; [INV]

  <bb 28> :
  vPortExitCritical ();
  xTicksToWait.1_8 = xTicksToWait;
  xTaskGenericNotifyWait (0, 0, 0, 0B, xTicksToWait.1_8);
  pxStreamBuffer_25->xTaskWaitingToSend ={v} 0B;
  _9 = xTaskCheckForTimeOut (&xTimeOut, &xTicksToWait);
  if (_9 == 0)
    goto <bb 21>; [INV]
  else
    goto <bb 29>; [INV]

  <bb 29> :

  <bb 30> :
  # xSpace_14 = PHI <xSpace_26(19), xSpace_39(29)>
  if (xSpace_14 == 0)
    goto <bb 31>; [INV]
  else
    goto <bb 32>; [INV]

  <bb 31> :
  xSpace_49 = xStreamBufferSpacesAvailable (pxStreamBuffer_25);

  <bb 32> :
  # xSpace_15 = PHI <xSpace_14(30), xSpace_49(31)>
  xReturn_51 = prvWriteMessageToBuffer (pxStreamBuffer_25, pvTxData_30(D), xDataLengthBytes_27(D), xSpace_15, xRequiredSpace_16);
  if (xReturn_51 != 0)
    goto <bb 33>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 33> :
  _10 = prvBytesInBuffer (pxStreamBuffer_25);
  _11 = pxStreamBuffer_25->xTriggerLevelBytes;
  if (_10 >= _11)
    goto <bb 34>; [INV]
  else
    goto <bb 37>; [INV]

  <bb 34> :
  vTaskSuspendAll ();
  _12 ={v} pxStreamBuffer_25->xTaskWaitingToReceive;
  if (_12 != 0B)
    goto <bb 35>; [INV]
  else
    goto <bb 36>; [INV]

  <bb 35> :
  _13 ={v} pxStreamBuffer_25->xTaskWaitingToReceive;
  xTaskGenericNotify (_13, 0, 0, 0, 0B);
  pxStreamBuffer_25->xTaskWaitingToReceive ={v} 0B;

  <bb 36> :
  xTaskResumeAll ();

  <bb 37> :
  _57 = xReturn_51;
  xTimeOut ={v} {CLOBBER};

  <bb 38> :
<L41>:
  return _57;

}


xStreamBufferBytesAvailable (struct StreamBufferDef_t * xStreamBuffer)
{
  uint32_t ulNewBASEPRI;
  size_t xReturn;
  const struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6382;
  size_t _6;

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

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

  <bb 4> :

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

  <bb 6> :
  xReturn_5 = prvBytesInBuffer (pxStreamBuffer_2);
  _6 = xReturn_5;

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

}


xStreamBufferSpacesAvailable (struct StreamBufferDef_t * xStreamBuffer)
{
  uint32_t ulNewBASEPRI;
  size_t xOriginalTail;
  size_t xSpace;
  const struct StreamBuffer_t * const pxStreamBuffer;
  size_t D.6378;
  unsigned int D.6374;
  unsigned int _1;
  unsigned int _2;
  unsigned int _3;
  unsigned int _4;
  unsigned int _5;
  unsigned int _12;
  size_t _16;

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

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

  <bb 4> :

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

  <bb 6> :
  xOriginalTail_10 ={v} pxStreamBuffer_8->xTail;
  _1 = pxStreamBuffer_8->xLength;
  _2 ={v} pxStreamBuffer_8->xTail;
  xSpace_11 = _1 + _2;
  _12 ={v} pxStreamBuffer_8->xHead;
  xSpace_13 = xSpace_11 - _12;
  _3 ={v} pxStreamBuffer_8->xTail;
  if (xOriginalTail_10 != _3)
    goto <bb 6>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 7> :
  xSpace_14 = xSpace_13 + 4294967295;
  _4 = pxStreamBuffer_8->xLength;
  if (xSpace_14 >= _4)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  _5 = pxStreamBuffer_8->xLength;
  xSpace_15 = xSpace_14 - _5;

  <bb 9> :
  # xSpace_6 = PHI <xSpace_14(7), xSpace_15(8)>
  _16 = xSpace_6;

  <bb 10> :
<L8>:
  return _16;

}


xStreamBufferSetTriggerLevel (struct StreamBufferDef_t * xStreamBuffer, size_t xTriggerLevel)
{
  uint32_t ulNewBASEPRI;
  BaseType_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  BaseType_t D.6370;
  unsigned int _1;
  BaseType_t _13;

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

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

  <bb 4> :

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

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

  <bb 7> :
  xTriggerLevel_8 = 1;

  <bb 8> :
  # xTriggerLevel_2 = PHI <xTriggerLevel_7(D)(6), xTriggerLevel_8(7)>
  _1 = pxStreamBuffer_6->xLength;
  if (xTriggerLevel_2 < _1)
    goto <bb 9>; [INV]
  else
    goto <bb 10>; [INV]

  <bb 9> :
  pxStreamBuffer_6->xTriggerLevelBytes = xTriggerLevel_2;
  xReturn_12 = 1;
  goto <bb 11>; [INV]

  <bb 10> :
  xReturn_10 = 0;

  <bb 11> :
  # xReturn_3 = PHI <xReturn_12(9), xReturn_10(10)>
  _13 = xReturn_3;

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

}


xStreamBufferReset (struct StreamBufferDef_t * xStreamBuffer)
{
  uint32_t ulNewBASEPRI;
  UBaseType_t uxStreamBufferNumber;
  BaseType_t xReturn;
  struct StreamBuffer_t * const pxStreamBuffer;
  BaseType_t D.6361;
  struct tskTaskControlBlock * _1;
  struct tskTaskControlBlock * _2;
  uint8_t * _3;
  unsigned int _4;
  unsigned int _5;
  unsigned char _6;
  BaseType_t _19;

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

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

  <bb 4> :

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

  <bb 6> :
  uxStreamBufferNumber_13 = pxStreamBuffer_10->uxStreamBufferNumber;
  vPortEnterCritical ();
  _1 ={v} pxStreamBuffer_10->xTaskWaitingToReceive;
  if (_1 == 0B)
    goto <bb 7>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 7> :
  _2 ={v} pxStreamBuffer_10->xTaskWaitingToSend;
  if (_2 == 0B)
    goto <bb 8>; [INV]
  else
    goto <bb 9>; [INV]

  <bb 8> :
  _3 = pxStreamBuffer_10->pucBuffer;
  _4 = pxStreamBuffer_10->xLength;
  _5 = pxStreamBuffer_10->xTriggerLevelBytes;
  _6 = pxStreamBuffer_10->ucFlags;
  prvInitialiseNewStreamBuffer (pxStreamBuffer_10, _3, _4, _5, _6);
  xReturn_16 = 1;
  pxStreamBuffer_10->uxStreamBufferNumber = uxStreamBufferNumber_13;

  <bb 9> :
  # xReturn_7 = PHI <xReturn_11(6), xReturn_11(7), xReturn_16(8)>
  vPortExitCritical ();
  _19 = xReturn_7;

  <bb 10> :
<L7>:
  return _19;

}


vStreamBufferDelete (struct StreamBufferDef_t * xStreamBuffer)
{
  uint32_t ulNewBASEPRI;
  struct StreamBuffer_t * pxStreamBuffer;
  unsigned char _1;
  int _2;
  int _3;

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

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

  <bb 4> :

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

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

  <bb 7> :
  vPortFree (pxStreamBuffer_6);
  goto <bb 9>; [INV]

  <bb 8> :
  memset (pxStreamBuffer_6, 0, 36);

  <bb 9> :
  return;

}


xStreamBufferGenericCreate (size_t xBufferSizeBytes, size_t xTriggerLevelBytes, BaseType_t xIsMessageBuffer)
{
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint32_t ulNewBASEPRI;
  uint8_t ucFlags;
  uint8_t * pucAllocatedMemory;
  struct StreamBufferDef_t * D.6348;
  unsigned int _1;
  uint8_t * _2;
  struct StreamBufferDef_t * _21;

  <bb 2> :
  if (xIsMessageBuffer_9(D) == 1)
    goto <bb 3>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 3> :
  ucFlags_13 = 1;
  if (xBufferSizeBytes_11(D) <= 4)
    goto <bb 4>; [INV]
  else
    goto <bb 11>; [INV]

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

  <bb 5> :

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

  <bb 7> :
  ucFlags_10 = 0;
  if (xBufferSizeBytes_11(D) == 0)
    goto <bb 8>; [INV]
  else
    goto <bb 11>; [INV]

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

  <bb 9> :

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

  <bb 11> :
  # ucFlags_6 = PHI <ucFlags_13(3), ucFlags_10(7)>
  if (xTriggerLevelBytes_14(D) > xBufferSizeBytes_11(D))
    goto <bb 12>; [INV]
  else
    goto <bb 15>; [INV]

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

  <bb 13> :

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

  <bb 15> :
  if (xTriggerLevelBytes_14(D) == 0)
    goto <bb 16>; [INV]
  else
    goto <bb 17>; [INV]

  <bb 16> :
  xTriggerLevelBytes_15 = 1;

  <bb 17> :
  # xTriggerLevelBytes_4 = PHI <xTriggerLevelBytes_14(D)(15), xTriggerLevelBytes_15(16)>
  if (xBufferSizeBytes_11(D) <= 4294967258)
    goto <bb 18>; [INV]
  else
    goto <bb 19>; [INV]

  <bb 18> :
  xBufferSizeBytes_17 = xBufferSizeBytes_11(D) + 1;
  _1 = xBufferSizeBytes_17 + 36;
  pucAllocatedMemory_19 = pvPortMalloc (_1);
  goto <bb 20>; [INV]

  <bb 19> :
  pucAllocatedMemory_16 = 0B;

  <bb 20> :
  # xBufferSizeBytes_3 = PHI <xBufferSizeBytes_17(18), xBufferSizeBytes_11(D)(19)>
  # pucAllocatedMemory_5 = PHI <pucAllocatedMemory_19(18), pucAllocatedMemory_16(19)>
  if (pucAllocatedMemory_5 != 0B)
    goto <bb 21>; [INV]
  else
    goto <bb 22>; [INV]

  <bb 21> :
  _2 = pucAllocatedMemory_5 + 36;
  prvInitialiseNewStreamBuffer (pucAllocatedMemory_5, _2, xBufferSizeBytes_3, xTriggerLevelBytes_4, ucFlags_6);

  <bb 22> :
  _21 = pucAllocatedMemory_5;

  <bb 23> :
<L20>:
  return _21;

}