+ /*
+ * Buggy BIOS check
+ * ACPI id of processors can be reported wrongly by the BIOS.
+ * Don't trust it blindly
+ */
+ if (processor_device_array[pr->id] != NULL &&
+ processor_device_array[pr->id] != (void *)device) {
+ ACPI_DEBUG_PRINT((ACPI_DB_ERROR, "BIOS reporting wrong ACPI id"
+ "for the processor\n"));
+ return_VALUE(-ENODEV);
+ }
+ processor_device_array[pr->id] = (void *)device;
+