Index: src/debug/print.c
===================================================================
--- src/debug/print.c	(revision 724b58aaabefadca6d3a85277fe070140ec29bc3)
+++ src/debug/print.c	(revision 93ca46f7db9fa7b986fd58472ab20b5b0321e051)
@@ -45,5 +45,5 @@
  *
  */
-void print_str(char *str)
+void print_str(const char *str)
 {
         int i = 0;
@@ -66,5 +66,5 @@
  *
  */
-void print_fixed_hex(__native num, int width)
+void print_fixed_hex(const __native num, const int width)
 {
 	int i;
@@ -85,12 +85,13 @@
  *
  */
-void print_number(__native num, int base)
-{ 
+void print_number(const __native num, const int base)
+{
+	int val = num;
 	char d[sizeof(__native)*8+1];		/* this is good enough even for base == 2 */
         int i = sizeof(__native)*8-1;
     
 	do {
-		d[i--] = digits[num % base];
-	} while (num /= base);
+		d[i--] = digits[val % base];
+	} while (val /= base);
 	
 	d[sizeof(__native)*8] = 0;	
@@ -133,5 +134,5 @@
  *
  */
-void printf(char *fmt, ...)
+void printf(const char *fmt, ...)
 {
 	int irqpri, i = 0;