// CreateDevicePath - decompiled from Platform.efi
void *__fastcall CreateDevicePath(UINTN AllocationSize, UINTN n26, __int64 SourceBuffer)
{
  void *DestinationBuffer; // rax

  if ( !SourceBuffer ) /*0x60db*/
    Assert( /*0x60f0*/
      (__int64)"e:\\hs\\MdePkg\\Library\\UefiMemoryAllocationLib\\MemoryAllocationLib.c",
      569,
      (__int64)"Buffer != ((void *) 0)");
  if ( n26 > -SourceBuffer ) /*0x60fe*/
    Assert( /*0x6113*/
      (__int64)"e:\\hs\\MdePkg\\Library\\UefiMemoryAllocationLib\\MemoryAllocationLib.c",
      570,
      (__int64)"AllocationSize <= (0xFFFFFFFFFFFFFFFFULL - (UINTN) Buffer + 1)");
  DestinationBuffer = AllocateCopyPool(AllocationSize, (const void *)n26); /*0x611b*/
  if ( DestinationBuffer ) /*0x6123*/
    return CopyMem(DestinationBuffer, (const void *)SourceBuffer, n26); /*0x612e*/
  return DestinationBuffer; /*0x6138*/
}