Skip to content
Snippets Groups Projects
Commit fd1c946c authored by Thomas Sewell's avatar Thomas Sewell
Browse files

Adjust -1 syntax for new Isabelle.

parent 0b162d7d
No related branches found
No related tags found
No related merge requests found
......@@ -761,7 +761,7 @@ cteDeleteOne(cte_t* slot)
bool_t final;
finaliseCap_ret_t fc_ret UNUSED;
/** GHOSTUPD: "(gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = -1
/** GHOSTUPD: "(gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = (-1)
\<or> gs_get_assn cteDeleteOne_'proc \<acute>ghost'state = \<acute>cap_type, id)" */
final = isFinalCapability(slot);
......
......@@ -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 -1)" */
/** 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 -1)" */
/** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc (-1))" */
cteDeleteOne(irqSlot);
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment