@@ -32,6 +32,7 @@
#include "hw/sysbus.h"
static int apic_irq_delivered;
+static bool apic_irq_delivered_valid;
bool apic_report_tpr_access;
void cpu_set_apic_base(DeviceState *dev, uint64_t val)
@@ -136,13 +137,18 @@ void apic_reset_irq_delivered(void)
volatile int a_i_d = apic_irq_delivered;
trace_apic_reset_irq_delivered(a_i_d);
+ assert(!apic_irq_delivered_valid);
apic_irq_delivered = 0;
+ apic_irq_delivered_valid = true;
}
int apic_get_irq_delivered(void)
{
trace_apic_get_irq_delivered(apic_irq_delivered);
+ assert(apic_irq_delivered_valid);
+ apic_irq_delivered_valid = false;
+
return apic_irq_delivered;
}