- printf("pci_bios_present: %d\n", RELOC_16(0xf000, num_pci_bios_present));
- printf("pci_bios_find_device: %d\n", RELOC_16(0xf000, num_pci_bios_find_device));
- printf("pci_bios_find_class: %d\n", RELOC_16(0xf000, num_pci_bios_find_class));
- printf("pci_bios_generate_special_cycle: %d\n", RELOC_16(0xf000, num_pci_bios_generate_special_cycle));
- printf("pci_bios_read_cfg_byte: %d\n", RELOC_16(0xf000, num_pci_bios_read_cfg_byte));
- printf("pci_bios_read_cfg_word: %d\n", RELOC_16(0xf000, num_pci_bios_read_cfg_word));
- printf("pci_bios_read_cfg_dword: %d\n", RELOC_16(0xf000, num_pci_bios_read_cfg_dword));
- printf("pci_bios_write_cfg_byte: %d\n", RELOC_16(0xf000, num_pci_bios_write_cfg_byte));
- printf("pci_bios_write_cfg_word: %d\n", RELOC_16(0xf000, num_pci_bios_write_cfg_word));
- printf("pci_bios_write_cfg_dword: %d\n", RELOC_16(0xf000, num_pci_bios_write_cfg_dword));
- printf("pci_bios_get_irq_routing: %d\n", RELOC_16(0xf000, num_pci_bios_get_irq_routing));
- printf("pci_bios_set_irq: %d\n", RELOC_16(0xf000, num_pci_bios_set_irq));
- printf("pci_bios_unknown_function: %d\n", RELOC_16(0xf000, num_pci_bios_unknown_function));
+ printf("pci_bios_present: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_present));
+ printf("pci_bios_find_device: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_find_device));
+ printf("pci_bios_find_class: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_find_class));
+ printf("pci_bios_generate_special_cycle: %d\n",
+ RELOC_16_LONG(0xf000,
+ num_pci_bios_generate_special_cycle));
+ printf("pci_bios_read_cfg_byte: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_read_cfg_byte));
+ printf("pci_bios_read_cfg_word: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_read_cfg_word));
+ printf("pci_bios_read_cfg_dword: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_read_cfg_dword));
+ printf("pci_bios_write_cfg_byte: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_write_cfg_byte));
+ printf("pci_bios_write_cfg_word: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_write_cfg_word));
+ printf("pci_bios_write_cfg_dword: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_write_cfg_dword));
+ printf("pci_bios_get_irq_routing: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_get_irq_routing));
+ printf("pci_bios_set_irq: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_set_irq));
+ printf("pci_bios_unknown_function: %d\n",
+ RELOC_16_LONG(0xf000, num_pci_bios_unknown_function));