Index: boot/arch/ia64/src/main.c
===================================================================
--- boot/arch/ia64/src/main.c	(revision 8ca4b602c9e88731eb7b89e339794815b53a2c11)
+++ boot/arch/ia64/src/main.c	(revision eec201dc0da41d601ba79f79b51c8f95f25d461e)
@@ -44,4 +44,5 @@
 #include <errno.h>
 #include <payload.h>
+#include <kernel.h>
 
 #define DEFAULT_MEMORY_BASE		0x4000000ULL
@@ -182,5 +183,11 @@
 	    (uintptr_t) kernel_start, NULL);
 
-	printf("Booting the kernel ...\n");
-	jump_to_kernel(&bootinfo, kernel_start);
+	uintptr_t entry = check_kernel(kernel_start);
+
+	// FIXME: kernel's entry point is linked at a different address than
+	//        where it is run from.
+	entry = entry - KERNEL_VADDRESS + KERNEL_ADDRESS;
+
+	printf("Booting the kernel at %p...\n", (void *) entry);
+	jump_to_kernel(&bootinfo, (void *) entry);
 }