This is expected. When the kernel is started by the bootloader, the processor is in
protected mode and can only use 32-bit instructions. One of the first things the x86_64?
kernel then does is to switch the processor to long mode and enable 64-bit instructions.
Because of this, the initial entry point assembly is 32bit, but the rest of the kernel is
64bit. You can verify this by checking the intermediate kernel build file:
$ file kernel/kernel.elf
kernel/kernel.elf: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), statically linked,
with debug_info, not stripped
This command is where the 64bit kernel is reformatted into a 32-bit elf:
From: Devel <devel-bounces(a)sel4.systems> on behalf of Chris Rothrock
Sent: Thursday, August 30, 2018 10:40 PM
Subject: [seL4] 32 bit vs 64 bit
When building the x86 demo for both 32 and 64 bit builds, it looks like the kernel is
still a 32 bit elf file regardless of the build and only the sel4test-driver file is what
is either 32 bit or 64 bit depending on which is selected. Is this normal or should the
kernel also be 64 bit on the 64 bit build?
Senior System Administrator