/* Convert to 64 bit value from two 32 bit words. */
STATIC UINT64 ConvertTo64Bit(IN UINT32 Low, IN UINT32 High)
/* Convert to 64 bit value from two 32 bit words. */
STATIC UINT64 ConvertTo64Bit(IN UINT32 Low, IN UINT32 High)
{
  return (Low | ((UINT64)High << 32));
}