From 0b162d7d3f100bb510d1dcfc92dc6f65dac95d65 Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Date: Fri, 15 May 2015 11:41:13 +1000
Subject: [PATCH] Weaken cap_async_cap cteDeleteOne assertions.
It's true that the interrupt node must contain async endpoint
caps, but we never proved the relevant invariant, and it doesn't
change much.
---
src/object/interrupt.c | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/object/interrupt.c b/src/object/interrupt.c
index c9236f88f..424fa3fea 100644
--- a/src/object/interrupt.c
+++ b/src/object/interrupt.c
@@ -171,7 +171,7 @@ invokeIRQHandler_SetIRQHandler(irq_t irq, cap_t cap, cte_t *slot)
cte_t *irqSlot;
irqSlot = intStateIRQNode + irq;
- /** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc (ucast cap_async_endpoint_cap))" */
+ /** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc -1)" */
cteDeleteOne(irqSlot);
cteInsert(cap, slot, irqSlot);
}
@@ -182,7 +182,7 @@ invokeIRQHandler_ClearIRQHandler(irq_t irq)
cte_t *irqSlot;
irqSlot = intStateIRQNode + irq;
- /** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc (ucast cap_async_endpoint_cap))" */
+ /** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc -1)" */
cteDeleteOne(irqSlot);
}
--
GitLab