On 13/07/2015 18:10, Peter Maydell wrote: > (4) a few other things which are suspicious at best: > hw/intc/apic_common.c: volatile int a_i_d = apic_irq_delivered;
This one has a comment above: /* Copy this into a local variable to encourage gcc to emit a plain * register for a sys/sdt.h marker. For details on this workaround, see: * https://sourceware.org/bugzilla/show_bug.cgi?id=13296 */ > hw/xen/xen_pt_msi.c: const volatile uint32_t *vec_ctrl; Seems to be MMIO (yes, really), so okay. Paolo