diff --git a/src/system/kernel/arch/x86/arch_real_time_clock.cpp b/src/system/kernel/arch/x86/arch_real_time_clock.cpp
index 5e5fee5e9f..24a02f5f39 100644
--- a/src/system/kernel/arch/x86/arch_real_time_clock.cpp
+++ b/src/system/kernel/arch/x86/arch_real_time_clock.cpp
@@ -8,6 +8,7 @@
 
 #include <arch/real_time_clock.h>
 #include <arch/cpu.h>
+#include <boot/kernel_args.h>
 
 #include <real_time_clock.h>
 #include <real_time_data.h>
@@ -214,7 +215,7 @@ arch_rtc_set_hw_time(uint32 seconds)
 
 	secs_to_cmos(seconds, &cmos);
 	write_cmos_clock(&cmos);
-}	
+}
 
 
 void
diff --git a/src/system/kernel/debug/debug_builtin_commands.cpp b/src/system/kernel/debug/debug_builtin_commands.cpp
index fb9e4b14d2..bb0fe2857a 100644
--- a/src/system/kernel/debug/debug_builtin_commands.cpp
+++ b/src/system/kernel/debug/debug_builtin_commands.cpp
@@ -10,6 +10,8 @@
 #include "debug_builtin_commands.h"
 
 #include <ctype.h>
+#include <string.h>
+
 #include <debug.h>
 #include <kernel.h>
 
diff --git a/src/system/kernel/device_manager/FileDevice.cpp b/src/system/kernel/device_manager/FileDevice.cpp
index 55e6fca21a..0f76dae5f4 100644
--- a/src/system/kernel/device_manager/FileDevice.cpp
+++ b/src/system/kernel/device_manager/FileDevice.cpp
@@ -7,6 +7,7 @@
 #include "FileDevice.h"
 
 #include <errno.h>
+#include <string.h>
 #include <unistd.h>
 
 #include <new>