Ghost assertions for cteDeleteOne.

src/kernel/thread.c

@@ -133,12 +133,14 @@ doReplyTransfer(tcb_t *sender, tcb_t *receiver, cte_t *slot)
 
     if (likely(fault_get_faultType(receiver->tcbFault) == fault_null_fault)) {
         doIPCTransfer(sender, NULL, 0, true, receiver, false);
+        /** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc -1)" */
         cteDeleteOne(slot);
         setThreadState(receiver, ThreadState_Running);
         attemptSwitchTo(receiver);
     } else {
         bool_t restart;
 
+        /** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc -1)" */
         cteDeleteOne(slot);
         restart = handleFaultReply(receiver, sender);
         fault_null_fault_ptr_new(&receiver->tcbFault);

src/object/cnode.c

@@ -756,10 +756,14 @@ reduceZombie(cte_t* slot, bool_t immediate)
 void
 cteDeleteOne(cte_t* slot)
 {
-    if (cap_get_capType(slot->cap) != cap_null_cap) {
+    uint32_t cap_type = cap_get_capType(slot->cap);
+    if (cap_type != cap_null_cap) {
         bool_t final;
         finaliseCap_ret_t fc_ret UNUSED;
 
+        /** 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);
         fc_ret = finaliseCap(slot->cap, final, true);
         /* Haskell error: "cteDeleteOne: cap should be removable" */

src/object/endpoint.c

@@ -261,6 +261,8 @@ ipcCancel(tcb_t *tptr)
 
         callerCap = CTE_PTR(mdb_node_get_mdbNext(slot->cteMDBNode));
         if (callerCap) {
+            /** GHOSTUPD: "(True,
+                gs_set_assn cteDeleteOne_'proc (ucast cap_reply_cap))" */
             cteDeleteOne(callerCap);
         }
 

src/object/interrupt.c

@@ -171,6 +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))" */
     cteDeleteOne(irqSlot);
     cteInsert(cap, slot, irqSlot);
 }
@@ -181,6 +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))" */
     cteDeleteOne(irqSlot);
 }
 
@@ -190,6 +192,7 @@ deletingIRQHandler(irq_t irq)
     cte_t *slot;
 
     slot = intStateIRQNode + irq;
+    /** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc (ucast cap_async_endpoint_cap))" */
     cteDeleteOne(slot);
 }
 

src/object/tcb.c

@@ -199,6 +199,7 @@ deleteCallerCap(tcb_t *receiver)
     cte_t *callerSlot;
 
     callerSlot = TCB_PTR_CTE_PTR(receiver, tcbCaller);
+    /** GHOSTUPD: "(True, gs_set_assn cteDeleteOne_'proc (ucast cap_reply_cap))" */
     cteDeleteOne(callerSlot);
 }