Index: kernel/generic/include/config.h
===================================================================
--- kernel/generic/include/config.h	(revision 019a348d874db2fcb7b702e64eab4d19d87a5973)
+++ kernel/generic/include/config.h	(revision 04357767a90c7f3afb5035aee20bc56c354efbb8)
@@ -66,5 +66,5 @@
 
 typedef struct {
-	size_t cpu_count;            /**< Number of processors detected. */
+	unsigned int cpu_count;      /**< Number of processors detected. */
 	volatile size_t cpu_active;  /**< Number of processors that are up and running. */
 	
Index: kernel/generic/include/cpu.h
===================================================================
--- kernel/generic/include/cpu.h	(revision 019a348d874db2fcb7b702e64eab4d19d87a5973)
+++ kernel/generic/include/cpu.h	(revision 04357767a90c7f3afb5035aee20bc56c354efbb8)
@@ -83,5 +83,5 @@
 	 * Processor ID assigned by kernel.
 	 */
-	size_t id;
+	unsigned int id;
 	
 	bool active;
Index: kernel/generic/include/sysinfo/abi.h
===================================================================
--- kernel/generic/include/sysinfo/abi.h	(revision 019a348d874db2fcb7b702e64eab4d19d87a5973)
+++ kernel/generic/include/sysinfo/abi.h	(revision 04357767a90c7f3afb5035aee20bc56c354efbb8)
@@ -66,5 +66,5 @@
  */
 typedef struct {
-	size_t id;               /**< CPU ID as stored by kernel */
+	unsigned int id;         /**< CPU ID as stored by kernel */
 	bool active;             /**< CPU is activate */
 	uint16_t frequency_mhz;  /**< Frequency in MHz */