OsIf_MicrosToTicks (uint32 Micros, OsIf_CounterType SelectedCounter)
{
  uint32 Value;
  uint32 D.4153;

  <bb 2> :
  # DEBUG BEGIN_STMT
  Value = 0;
  # DEBUG BEGIN_STMT
  _1 = (int) SelectedCounter;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
<L0>:
  # DEBUG BEGIN_STMT
  Value = OsIf_Timer_Dummy_MicrosToTicks (Micros);
  # DEBUG BEGIN_STMT

  <bb 4> :
  # DEBUG BEGIN_STMT
  D.4153 = Value;
  return D.4153;

}


OsIf_SetTimerFrequency (uint32 Freq, OsIf_CounterType SelectedCounter)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  _1 = (int) SelectedCounter;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
<L0>:
  # DEBUG BEGIN_STMT
  OsIf_Timer_Dummy_SetTimerFrequency (Freq);
  # DEBUG BEGIN_STMT

  <bb 4> :
  return;

}


OsIf_GetElapsed (uint32 * const CurrentRef, OsIf_CounterType SelectedCounter)
{
  uint32 Value;
  uint32 D.4149;

  <bb 2> :
  # DEBUG BEGIN_STMT
  Value = 0;
  # DEBUG BEGIN_STMT
  _1 = (int) SelectedCounter;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
<L0>:
  # DEBUG BEGIN_STMT
  Value = OsIf_Timer_Dummy_GetElapsed (CurrentRef);
  # DEBUG BEGIN_STMT

  <bb 4> :
  # DEBUG BEGIN_STMT
  D.4149 = Value;
  return D.4149;

}


OsIf_GetCounter (OsIf_CounterType SelectedCounter)
{
  uint32 Value;
  uint32 D.4145;

  <bb 2> :
  # DEBUG BEGIN_STMT
  Value = 0;
  # DEBUG BEGIN_STMT
  _1 = (int) SelectedCounter;
  if (_1 == 0)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
<L0>:
  # DEBUG BEGIN_STMT
  Value = OsIf_Timer_Dummy_GetCounter ();
  # DEBUG BEGIN_STMT

  <bb 4> :
  # DEBUG BEGIN_STMT
  D.4145 = Value;
  return D.4145;

}


OsIf_Init (const void * Config)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  if (Config != 0B)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
  # DEBUG BEGIN_STMT
  DevAssert (0);

  <bb 4> :
  # DEBUG BEGIN_STMT
  OsIf_Timer_Dummy_Init ();
  return;

}


OsIf_Timer_Dummy_MicrosToTicks (uint32 Micros)
{
  uint32 D.4155;

  <bb 2> :
  # DEBUG BEGIN_STMT
  D.4155 = Micros;
  return D.4155;

}


OsIf_Timer_Dummy_SetTimerFrequency (uint32 Freq)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  return;

}


OsIf_Timer_Dummy_GetElapsed (const uint32 * const CurrentRef)
{
  uint32 D.4151;

  <bb 2> :
  # DEBUG BEGIN_STMT
  # DEBUG BEGIN_STMT
  D.4151 = 1;
  return D.4151;

}


OsIf_Timer_Dummy_GetCounter ()
{
  uint32 D.4147;

  <bb 2> :
  # DEBUG BEGIN_STMT
  D.4147 = 0;
  return D.4147;

}


OsIf_Timer_Dummy_Init ()
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  return;

}


DevAssert (volatile boolean x)
{
  <bb 2> :
  # DEBUG BEGIN_STMT
  x.0_1 = x;
  if (x.0_1 != 0)
    goto <bb 4>; [INV]
  else
    goto <bb 3>; [INV]

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

  <bb 4> :
  # DEBUG BEGIN_STMT
  return;

}