From 49af8fd30fa80748572f540fe33443b8c89441c5 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Wed, 23 Nov 2022 15:18:11 -0500
Subject: [PATCH] Finished verification of iteration updates in
 `prvSelectHighestPriorityTask`.

---
 tasks.c                                       | 44 +++++++++++++++++--
 .../scp_list_predicates_extended.h            |  5 +++
 2 files changed, 46 insertions(+), 3 deletions(-)

diff --git a/tasks.c b/tasks.c
index d397bb9de..90e722d98 100644
--- a/tasks.c
+++ b/tasks.c
@@ -1130,11 +1130,48 @@ static void prvYieldForTask( TCB_t * pxTCB,
                     //@ assert( mem(gTaskItem_3, gCells) == true );
                    
 
-// TODO: Remove
-// Ensure that we covered all cases until this point
-//@ assume(false);
+                    /*@
+                    if( gTaskItem_3 == gListEnd ) {
+                        open DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList);
+                    } else{
+                        split(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gTaskItem_3, gTaskItemIndex_3);
+                        open DLS(gTaskItem_3, _, gListEnd, gEndPrev2, _, _, gReadyList);
+                    }
+                    @*/
+
                     pxTCB = pxTaskItem->pvOwner;
 
+                    //@ close xLIST_ITEM(gTaskItem_3, ?gTaskItem_3_val, ?gTaskItem_3_next, _, gReadyList);
+
+                    /*@
+                    if( gTaskItem_3 == gListEnd ) {
+                        close DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList);
+                    } else{
+                        assert( DLS(gListEnd, gEndPrev2, gTaskItem_3, ?gTaskItem_3_prev, ?gCellsPrefix, ?gValsPrefix, gReadyList) );
+
+                        if( gTaskItem_3 == gEndPrev2 ) {
+                            close DLS(gTaskItem_3, gTaskItem_3_prev, gListEnd, gEndPrev2, 
+                                      cons(gTaskItem_3, nil), cons(gTaskItem_3_val, nil), 
+                                      gReadyList);
+                        } else {
+                            assert( DLS(gTaskItem_3_next, gTaskItem_3, gListEnd, gEndPrev2, 
+                                        ?gCellsSuffix2, ?gValsSuffix2, gReadyList));
+                            close DLS(gTaskItem_3, gTaskItem_3_prev, gListEnd, gEndPrev2, 
+                                      cons(gTaskItem_3, gCellsSuffix2), 
+                                      cons(gTaskItem_3_val, gValsSuffix2), 
+                                      gReadyList);
+                        }
+                        assert( DLS(gTaskItem_3, gTaskItem_3_prev, gListEnd, gEndPrev2, ?gCellsSuffix, ?gValsSuffix, gReadyList) );
+                        join(gListEnd, gEndPrev2, gTaskItem_3, gTaskItem_3_prev, gCellsPrefix, gValsPrefix,
+                             gTaskItem_3, gTaskItem_3_prev, gListEnd, gEndPrev2, gCellsSuffix, gValsSuffix);
+                    }
+                    @*/
+                    //@ assert( DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList) );
+
+// Make sure that we covered all cases so far
+//@ assume(false);
+#ifdef IGNORED
+
                     /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */
 
                     #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) )
@@ -1193,6 +1230,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                         vListInsertEnd( pxReadyList, pxTaskItem );
                         break;
                     }
+#endif /* IGNORED */
                 } while( pxTaskItem != pxLastTaskItem );
             }
             else
diff --git a/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h b/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h
index 752561446..d0ffb5972 100644
--- a/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h
+++ b/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h
@@ -3,6 +3,11 @@
 
 #include "single_core_proofs/scp_list_predicates.h"
 
+/* =============================================================================
+ * The lemmas below assist in opening and closing DLS predicates in a way that
+ * allows accesses to `pxItem->pxNext`.
+*/
+
 /*@
 lemma void DLS_end_next_open(struct xLIST* pxList, struct xLIST_ITEM* pxItem)
 requires