efi_fdt_alloc_size
size_t efi_fdt_alloc_size(void);
alloc_size = marks[MARK_END] - marks[MARK_START] + efi_fdt_alloc_size() + EFIBOOT_ALIGN;