#define ACPI_SET64(ptr, val) (*ACPI_CAST64 (ptr) = (u64) (val))
/*
- * printf() format helpers
+ * printf() format helpers. These macros are workarounds for the difficulties
+ * with emitting 64-bit integers and 64-bit pointers with the same code
+ * for both 32-bit and 64-bit hosts.
*/
-
-/* Split 64-bit integer into two 32-bit values. Use with %8.8X%8.8X */
-
#define ACPI_FORMAT_UINT64(i) ACPI_HIDWORD(i), ACPI_LODWORD(i)
#if ACPI_MACHINE_WIDTH == 64
#define ACPI_FORMAT_NATIVE_UINT(i) ACPI_FORMAT_UINT64(i)
+#define ACPI_FORMAT_TO_UINT(i) ACPI_FORMAT_UINT64(i)
+#define ACPI_PRINTF_UINT "0x%8.8X%8.8X"
+
#else
-#define ACPI_FORMAT_NATIVE_UINT(i) 0, (i)
+#define ACPI_FORMAT_NATIVE_UINT(i) 0, (u32) (i)
+#define ACPI_FORMAT_TO_UINT(i) (u32) (i)
+#define ACPI_PRINTF_UINT "0x%8.8X"
#endif
/*