Index: kernel/arch/ia32/include/smp/smp.h
===================================================================
--- kernel/arch/ia32/include/smp/smp.h	(revision 7d07bf31f74e2ee585ca017e2dccbd51c38cad08)
+++ kernel/arch/ia32/include/smp/smp.h	(revision 623b49f1b94781911cb219ad1a68b6afdb2b0bbf)
@@ -44,8 +44,8 @@
 	bool (*cpu_bootstrap)(index_t i);	/**< Check whether the processor of index i is BSP. */
 	uint8_t (*cpu_apic_id)(index_t i);		/**< Return APIC ID of the processor of index i. */
-	int (*irq_to_pin)(int irq);		/**< Return mapping between irq and APIC pin. */
+	int (*irq_to_pin)(unsigned int irq);		/**< Return mapping between irq and APIC pin. */
 };
 
-extern int smp_irq_to_pin(int irq);
+extern int smp_irq_to_pin(unsigned int irq);
 
 #endif
Index: kernel/arch/ia32/src/smp/apic.c
===================================================================
--- kernel/arch/ia32/src/smp/apic.c	(revision 7d07bf31f74e2ee585ca017e2dccbd51c38cad08)
+++ kernel/arch/ia32/src/smp/apic.c	(revision 623b49f1b94781911cb219ad1a68b6afdb2b0bbf)
@@ -147,5 +147,5 @@
 {
 	io_apic_id_t idreg;
-	int i;
+	unsigned int i;
 
 	exc_register(VECTOR_APIC_SPUR, "apic_spurious", (iroutine) apic_spurious);
@@ -173,5 +173,5 @@
 	
 		if ((pin = smp_irq_to_pin(i)) != -1)
-			io_apic_change_ioredtbl(pin, DEST_ALL, IVT_IRQBASE+i, LOPRI);
+			io_apic_change_ioredtbl(pin, DEST_ALL, IVT_IRQBASE + i, LOPRI);
 	}
 	
@@ -535,8 +535,9 @@
 {
 	io_redirection_reg_t reg;
-	int i, pin;
-	
-	for (i=0;i<16;i++) {
-		if (irqmask & (1<<i)) {
+	unsigned int i;
+	int pin;
+	
+	for (i = 0; i < 16; i++) {
+		if (irqmask & (1 << i)) {
 			/*
 			 * Mask the signal input in IO APIC if there is a
@@ -545,7 +546,7 @@
 			pin = smp_irq_to_pin(i);
 			if (pin != -1) {
-				reg.lo = io_apic_read(IOREDTBL + pin*2);
+				reg.lo = io_apic_read(IOREDTBL + pin * 2);
 				reg.masked = true;
-				io_apic_write(IOREDTBL + pin*2, reg.lo);
+				io_apic_write(IOREDTBL + pin * 2, reg.lo);
 			}
 			
@@ -560,9 +561,10 @@
 void io_apic_enable_irqs(uint16_t irqmask)
 {
-	int i, pin;
+	unsigned int i;
+	int pin;
 	io_redirection_reg_t reg;	
 	
-	for (i=0;i<16;i++) {
-		if (irqmask & (1<<i)) {
+	for (i = 0;i < 16; i++) {
+		if (irqmask & (1 << i)) {
 			/*
 			 * Unmask the signal input in IO APIC if there is a
@@ -571,7 +573,7 @@
 			pin = smp_irq_to_pin(i);
 			if (pin != -1) {
-				reg.lo = io_apic_read(IOREDTBL + pin*2);
+				reg.lo = io_apic_read(IOREDTBL + pin * 2);
 				reg.masked = false;
-				io_apic_write(IOREDTBL + pin*2, reg.lo);
+				io_apic_write(IOREDTBL + pin * 2, reg.lo);
 			}
 			
Index: kernel/arch/ia32/src/smp/mps.c
===================================================================
--- kernel/arch/ia32/src/smp/mps.c	(revision 7d07bf31f74e2ee585ca017e2dccbd51c38cad08)
+++ kernel/arch/ia32/src/smp/mps.c	(revision 623b49f1b94781911cb219ad1a68b6afdb2b0bbf)
@@ -91,5 +91,5 @@
 static bool is_bsp(index_t i);
 static uint8_t get_cpu_apic_id(index_t i);
-static int mps_irq_to_pin(int irq);
+static int mps_irq_to_pin(unsigned int irq);
 
 struct smp_config_operations mps_config_operations = {
@@ -414,9 +414,9 @@
 }
 
-int mps_irq_to_pin(int irq)
+int mps_irq_to_pin(unsigned int irq)
 {
 	unsigned int i;
 	
-	for(i = 0; i < io_intr_entry_cnt; i++) {
+	for (i = 0; i < io_intr_entry_cnt; i++) {
 		if (io_intr_entries[i].src_bus_irq == irq && io_intr_entries[i].intr_type == 0)
 			return io_intr_entries[i].dst_io_apic_pin;
Index: kernel/arch/ia32/src/smp/smp.c
===================================================================
--- kernel/arch/ia32/src/smp/smp.c	(revision 7d07bf31f74e2ee585ca017e2dccbd51c38cad08)
+++ kernel/arch/ia32/src/smp/smp.c	(revision 623b49f1b94781911cb219ad1a68b6afdb2b0bbf)
@@ -171,5 +171,5 @@
 }
 
-int smp_irq_to_pin(int irq)
+int smp_irq_to_pin(unsigned int irq)
 {
 	ASSERT(ops != NULL);
Index: kernel/arch/ia32xen/src/smp/apic.c
===================================================================
--- kernel/arch/ia32xen/src/smp/apic.c	(revision 7d07bf31f74e2ee585ca017e2dccbd51c38cad08)
+++ kernel/arch/ia32xen/src/smp/apic.c	(revision 623b49f1b94781911cb219ad1a68b6afdb2b0bbf)
@@ -125,5 +125,5 @@
 {
 	io_apic_id_t idreg;
-	int i;
+	unsigned int i;
 
 	exc_register(VECTOR_APIC_SPUR, "apic_spurious", (iroutine) apic_spurious);
@@ -529,8 +529,9 @@
 {
 	io_redirection_reg_t reg;
-	int i, pin;
-	
-	for (i=0;i<16;i++) {
-		if (irqmask & (1<<i)) {
+	unsigned int i;
+	int pin;
+	
+	for (i = 0; i < 16; i++) {
+		if (irqmask & (1 << i)) {
 			/*
 			 * Mask the signal input in IO APIC if there is a
@@ -554,9 +555,10 @@
 void io_apic_enable_irqs(uint16_t irqmask)
 {
-	int i, pin;
+	unsigned int i;
+	int pin;
 	io_redirection_reg_t reg;	
 	
-	for (i=0;i<16;i++) {
-		if (irqmask & (1<<i)) {
+	for (i = 0; i < 16; i++) {
+		if (irqmask & (1 << i)) {
 			/*
 			 * Unmask the signal input in IO APIC if there is a
Index: kernel/arch/ia32xen/src/smp/mps.c
===================================================================
--- kernel/arch/ia32xen/src/smp/mps.c	(revision 7d07bf31f74e2ee585ca017e2dccbd51c38cad08)
+++ kernel/arch/ia32xen/src/smp/mps.c	(revision 623b49f1b94781911cb219ad1a68b6afdb2b0bbf)
@@ -93,5 +93,5 @@
 static bool is_bsp(index_t i);
 static uint8_t get_cpu_apic_id(index_t i);
-static int mps_irq_to_pin(int irq);
+static int mps_irq_to_pin(unsigned int irq);
 
 struct smp_config_operations mps_config_operations = {
@@ -416,9 +416,9 @@
 }
 
-int mps_irq_to_pin(int irq)
+int mps_irq_to_pin(unsigned int irq)
 {
 	int i;
 	
-	for(i=0;i<io_intr_entry_cnt;i++) {
+	for (i = 0; i < io_intr_entry_cnt; i++) {
 		if (io_intr_entries[i].src_bus_irq == irq && io_intr_entries[i].intr_type == 0)
 			return io_intr_entries[i].dst_io_apic_pin;
Index: kernel/arch/ia32xen/src/smp/smp.c
===================================================================
--- kernel/arch/ia32xen/src/smp/smp.c	(revision 7d07bf31f74e2ee585ca017e2dccbd51c38cad08)
+++ kernel/arch/ia32xen/src/smp/smp.c	(revision 623b49f1b94781911cb219ad1a68b6afdb2b0bbf)
@@ -163,5 +163,5 @@
 }
 
-int smp_irq_to_pin(int irq)
+int smp_irq_to_pin(unsigned int irq)
 {
 	ASSERT(ops != NULL);
Index: kernel/genarch/src/acpi/madt.c
===================================================================
--- kernel/genarch/src/acpi/madt.c	(revision 7d07bf31f74e2ee585ca017e2dccbd51c38cad08)
+++ kernel/genarch/src/acpi/madt.c	(revision 623b49f1b94781911cb219ad1a68b6afdb2b0bbf)
@@ -70,5 +70,5 @@
 
 struct madt_apic_header * * madt_entries_index = NULL;
-int madt_entries_index_cnt = 0;
+unsigned int madt_entries_index_cnt = 0;
 
 char *entry[] = {
@@ -91,5 +91,5 @@
 static bool madt_cpu_bootstrap(index_t i);
 static uint8_t madt_cpu_apic_id(index_t i);
-static int madt_irq_to_pin(int irq);
+static int madt_irq_to_pin(unsigned int irq);
 
 struct smp_config_operations madt_config_operations = {
@@ -125,5 +125,5 @@
 }
 
-int madt_irq_to_pin(int irq)
+int madt_irq_to_pin(unsigned int irq)
 {
 	ASSERT(irq < sizeof(isa_irq_map)/sizeof(int));
@@ -144,5 +144,5 @@
 	struct madt_apic_header *h;
 	
-        l_apic = (uint32_t *) (unative_t) acpi_madt->l_apic_address;
+	l_apic = (uint32_t *) (unative_t) acpi_madt->l_apic_address;
 
 	/* calculate madt entries */
@@ -165,39 +165,38 @@
 	qsort(madt_entries_index, madt_entries_index_cnt, sizeof(uintptr_t), &madt_cmp);
 
-	/* Parse MADT entries */	
-	for (index = 0; index < madt_entries_index_cnt - 1; index++) {
-		h = madt_entries_index[index];
-		switch (h->type) {
-			case MADT_L_APIC:
-				madt_l_apic_entry((struct madt_l_apic *) h, index);
-				break;
-			case MADT_IO_APIC:
-				madt_io_apic_entry((struct madt_io_apic *) h, index);
-				break;
-			case MADT_INTR_SRC_OVRD:
-				madt_intr_src_ovrd_entry((struct madt_intr_src_ovrd *) h, index);
-				break;
-			case MADT_NMI_SRC:
-			case MADT_L_APIC_NMI:
-			case MADT_L_APIC_ADDR_OVRD:
-			case MADT_IO_SAPIC:
-			case MADT_L_SAPIC:
-			case MADT_PLATFORM_INTR_SRC:
-				printf("MADT: skipping %s entry (type=%zd)\n", entry[h->type], h->type);
-				break;
-
-			default:
-				if (h->type >= MADT_RESERVED_SKIP_BEGIN && h->type <= MADT_RESERVED_SKIP_END) {
-					printf("MADT: skipping reserved entry (type=%zd)\n", h->type);
-				}
-				if (h->type >= MADT_RESERVED_OEM_BEGIN) {
-					printf("MADT: skipping OEM entry (type=%zd)\n", h->type);
-				}
-				break;
+	/* Parse MADT entries */
+	if (madt_entries_index_cnt > 0) {	
+		for (index = 0; index < madt_entries_index_cnt - 1; index++) {
+			h = madt_entries_index[index];
+			switch (h->type) {
+				case MADT_L_APIC:
+					madt_l_apic_entry((struct madt_l_apic *) h, index);
+					break;
+				case MADT_IO_APIC:
+					madt_io_apic_entry((struct madt_io_apic *) h, index);
+					break;
+				case MADT_INTR_SRC_OVRD:
+					madt_intr_src_ovrd_entry((struct madt_intr_src_ovrd *) h, index);
+					break;
+				case MADT_NMI_SRC:
+				case MADT_L_APIC_NMI:
+				case MADT_L_APIC_ADDR_OVRD:
+				case MADT_IO_SAPIC:
+				case MADT_L_SAPIC:
+				case MADT_PLATFORM_INTR_SRC:
+					printf("MADT: skipping %s entry (type=%zd)\n", entry[h->type], h->type);
+					break;
+	
+				default:
+					if (h->type >= MADT_RESERVED_SKIP_BEGIN && h->type <= MADT_RESERVED_SKIP_END) {
+						printf("MADT: skipping reserved entry (type=%zd)\n", h->type);
+					}
+					if (h->type >= MADT_RESERVED_OEM_BEGIN) {
+						printf("MADT: skipping OEM entry (type=%zd)\n", h->type);
+					}
+					break;
+			}
 		}
-	
-	
-	}
-	
+	}
 
 	if (cpu_count)