uxListRemove (struct ListItem_t * const pxItemToRemove)
{
  struct List_t * const pxList;
  struct xLIST_ITEM * _1;
  struct xLIST_ITEM * _2;
  struct xLIST_ITEM * _3;
  struct xLIST_ITEM * _4;
  struct ListItem_t * _5;
  struct xLIST_ITEM * _6;
  long unsigned int _7;
  long unsigned int _8;
  UBaseType_t _18;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxList_12 = pxItemToRemove_11(D)->pvContainer;
  # DEBUG pxList => pxList_12
  # DEBUG BEGIN_STMT
  _1 = pxItemToRemove_11(D)->pxNext;
  _2 = pxItemToRemove_11(D)->pxPrevious;
  _1->pxPrevious = _2;
  # DEBUG BEGIN_STMT
  _3 = pxItemToRemove_11(D)->pxPrevious;
  _4 = pxItemToRemove_11(D)->pxNext;
  _3->pxNext = _4;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _5 = pxList_12->pxIndex;
  if (pxItemToRemove_11(D) == _5)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  _6 = pxItemToRemove_11(D)->pxPrevious;
  pxList_12->pxIndex = _6;

  <bb 4> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxItemToRemove_11(D)->pvContainer = 0B;
  # DEBUG BEGIN_STMT
  _7 ={v} pxList_12->uxNumberOfItems;
  _8 = _7 + 4294967295;
  pxList_12->uxNumberOfItems ={v} _8;
  # DEBUG BEGIN_STMT
  _18 ={v} pxList_12->uxNumberOfItems;
  return _18;

}


vListInsert (struct List_t * const pxList, struct ListItem_t * const pxNewListItem)
{
  const TickType_t xValueOfInsertion;
  struct ListItem_t * pxIterator;
  struct xLIST_ITEM * _1;
  long unsigned int _2;
  struct xLIST_ITEM * _3;
  struct xLIST_ITEM * _4;
  long unsigned int _5;
  long unsigned int _6;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  xValueOfInsertion_11 = pxNewListItem_10(D)->xItemValue;
  # DEBUG xValueOfInsertion => xValueOfInsertion_11
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  if (xValueOfInsertion_11 == 4294967295)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  pxIterator_15 = pxList_12(D)->xListEnd.pxPrevious;
  # DEBUG pxIterator => pxIterator_15
  goto <bb 7>; [INV]

  <bb 4> :
  # DEBUG BEGIN_STMT
  pxIterator_13 = &pxList_12(D)->xListEnd;
  # DEBUG pxIterator => pxIterator_13
  goto <bb 6>; [INV]

  <bb 5> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxIterator_14 = pxIterator_7->pxNext;
  # DEBUG pxIterator => pxIterator_14

  <bb 6> :
  # pxIterator_7 = PHI <pxIterator_13(4), pxIterator_14(5)>
  # DEBUG pxIterator => pxIterator_7
  # DEBUG BEGIN_STMT
  _1 = pxIterator_7->pxNext;
  _2 = _1->xItemValue;
  if (xValueOfInsertion_11 >= _2)
    goto <bb 5>; [INV]
  else
    goto <bb 7>; [INV]

  <bb 7> :
  # pxIterator_8 = PHI <pxIterator_15(3), pxIterator_7(6)>
  # DEBUG pxIterator => pxIterator_8
  # DEBUG BEGIN_STMT
  _3 = pxIterator_8->pxNext;
  pxNewListItem_10(D)->pxNext = _3;
  # DEBUG BEGIN_STMT
  _4 = pxNewListItem_10(D)->pxNext;
  _4->pxPrevious = pxNewListItem_10(D);
  # DEBUG BEGIN_STMT
  pxNewListItem_10(D)->pxPrevious = pxIterator_8;
  # DEBUG BEGIN_STMT
  pxIterator_8->pxNext = pxNewListItem_10(D);
  # DEBUG BEGIN_STMT
  pxNewListItem_10(D)->pvContainer = pxList_12(D);
  # DEBUG BEGIN_STMT
  _5 ={v} pxList_12(D)->uxNumberOfItems;
  _6 = _5 + 1;
  pxList_12(D)->uxNumberOfItems ={v} _6;
  return;

}


vListInsertEnd (struct List_t * const pxList, struct ListItem_t * const pxNewListItem)
{
  struct ListItem_t * const pxIndex;
  struct xLIST_ITEM * _1;
  struct xLIST_ITEM * _2;
  long unsigned int _3;
  long unsigned int _4;

  <bb 2> :
  # DEBUG BEGIN_STMT
  pxIndex_7 = pxList_6(D)->pxIndex;
  # DEBUG pxIndex => pxIndex_7
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  pxNewListItem_8(D)->pxNext = pxIndex_7;
  # DEBUG BEGIN_STMT
  _1 = pxIndex_7->pxPrevious;
  pxNewListItem_8(D)->pxPrevious = _1;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  _2 = pxIndex_7->pxPrevious;
  _2->pxNext = pxNewListItem_8(D);
  # DEBUG BEGIN_STMT
  pxIndex_7->pxPrevious = pxNewListItem_8(D);
  # DEBUG BEGIN_STMT
  pxNewListItem_8(D)->pvContainer = pxList_6(D);
  # DEBUG BEGIN_STMT
  _3 ={v} pxList_6(D)->uxNumberOfItems;
  _4 = _3 + 1;
  pxList_6(D)->uxNumberOfItems ={v} _4;
  return;

}


vListInitialiseItem (struct ListItem_t * const pxItem)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  pxItem_2(D)->pvContainer = 0B;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  return;

}


vListInitialise (struct List_t * const pxList)
{
  struct MiniListItem_t * _1;
  struct MiniListItem_t * _2;
  struct MiniListItem_t * _3;

  <bb 2> :
  # DEBUG BEGIN_STMT
  _1 = &pxList_4(D)->xListEnd;
  pxList_4(D)->pxIndex = _1;
  # DEBUG BEGIN_STMT
  pxList_4(D)->xListEnd.xItemValue = 4294967295;
  # DEBUG BEGIN_STMT
  _2 = &pxList_4(D)->xListEnd;
  pxList_4(D)->xListEnd.pxNext = _2;
  # DEBUG BEGIN_STMT
  _3 = &pxList_4(D)->xListEnd;
  pxList_4(D)->xListEnd.pxPrevious = _3;
  # DEBUG BEGIN_STMT
  pxList_4(D)->uxNumberOfItems ={v} 0;
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  return;

}