Index: kernel/arch/ia32/src/bios/bios.c
===================================================================
--- kernel/arch/ia32/src/bios/bios.c	(revision be3f94cc9353d7054d4a674904c7150a2206f504)
+++ kernel/arch/ia32/src/bios/bios.c	(revision f2b3d3ea3dc1fbb7a2312b326613bcc88a3bfaf5)
@@ -36,5 +36,5 @@
 #include <typedefs.h>
 
-#define BIOS_EBDA_PTR  0x40e
+#define BIOS_EBDA_PTR  0x40eU
 
 uintptr_t ebda = 0;
@@ -43,5 +43,5 @@
 {
 	/* Copy the EBDA address out from BIOS Data Area */
-	ebda = *((uint16_t *) BIOS_EBDA_PTR) * 0x10;
+	ebda = *((uint16_t *) BIOS_EBDA_PTR) * 0x10U;
 }