Index: kernel/generic/src/printf/printf.c
===================================================================
--- kernel/generic/src/printf/printf.c	(revision d99c1d2ba8c7b2c687d430f2e9fd237046606545)
+++ kernel/generic/src/printf/printf.c	(revision 170332d3d135e4a1d5f7b7ffcec5cc352b6faa1b)
@@ -34,4 +34,5 @@
 
 #include <print.h>
+#include <stdarg.h>
 
 int printf(const char *fmt, ...)
Index: kernel/generic/src/printf/printf_core.c
===================================================================
--- kernel/generic/src/printf/printf_core.c	(revision d99c1d2ba8c7b2c687d430f2e9fd237046606545)
+++ kernel/generic/src/printf/printf_core.c	(revision 170332d3d135e4a1d5f7b7ffcec5cc352b6faa1b)
@@ -46,16 +46,23 @@
 /** show prefixes 0x or 0 */
 #define __PRINTF_FLAG_PREFIX       0x00000001
+
 /** signed / unsigned number */
 #define __PRINTF_FLAG_SIGNED       0x00000002
+
 /** print leading zeroes */
 #define __PRINTF_FLAG_ZEROPADDED   0x00000004
+
 /** align to left */
 #define __PRINTF_FLAG_LEFTALIGNED  0x00000010
+
 /** always show + sign */
 #define __PRINTF_FLAG_SHOWPLUS     0x00000020
+
 /** print space instead of plus */
 #define __PRINTF_FLAG_SPACESIGN    0x00000040
+
 /** show big characters */
 #define __PRINTF_FLAG_BIGCHARS     0x00000080
+
 /** number has - sign */
 #define __PRINTF_FLAG_NEGATIVE     0x00000100
@@ -79,8 +86,8 @@
 } qualifier_t;
 
-static char nullstr[] = "(NULL)";
-static char digits_small[] = "0123456789abcdef";
-static char digits_big[] = "0123456789ABCDEF";
-static char invalch = U_SPECIAL;
+static const char *nullstr = "(NULL)";
+static const char *digits_small = "0123456789abcdef";
+static const char *digits_big = "0123456789ABCDEF";
+static const char invalch = U_SPECIAL;
 
 /** Print one or more characters without adding newline.
@@ -351,5 +358,5 @@
     uint32_t flags, printf_spec_t *ps)
 {
-	char *digits;
+	const char *digits;
 	if (flags & __PRINTF_FLAG_BIGCHARS)
 		digits = digits_big;