// WriteS3BootScript - decompiled from Platform.efi
__int64 __fastcall WriteS3BootScript(const void *DestinationBuffer, __int64 a2, UINTN Length)
{
  __int64 result; // rax
  __int64 DxeServicesTable; // rax

  result = qword_FF08; /*0x7b0c*/
  if ( !qword_FF08 ) /*0x7b16*/
  {
    DxeServicesTable = GetDxeServicesTable(&DestinationBuffer_, &qword_FF08, Length); /*0x7b26*/
    if ( DxeServicesTable < 0 ) /*0x7b2e*/
    {
      DebugPrint(0x80000000, "\nASSERT_EFI_ERROR (Status = %r)\n", DxeServicesTable); /*0x7b3f*/
      Assert((__int64)"e:\\hs\\MdePkg\\Library\\DxeHobLib\\HobLib.c", 54, (__int64)"!EFI_ERROR (Status)"); /*0x7b57*/
    }
    result = qword_FF08; /*0x7b5c*/
    if ( !qword_FF08 ) /*0x7b66*/
    {
      Assert((__int64)"e:\\hs\\MdePkg\\Library\\DxeHobLib\\HobLib.c", 55, (__int64)"mHobList != ((void *) 0)"); /*0x7b79*/
      return qword_FF08; /*0x7b7e*/
    }
  }
  return result; /*0x7b85*/
}