Justified memset of TCB fields in prvInitialiseNewTask.

Fields: `pxNewTCB->ucNotifyState` and `pxNewTCB->ulNotifiedValue`

include/list.h

@@ -400,6 +400,8 @@ void vListInitialise( List_t * const pxList ) PRIVILEGED_FUNCTION;
  * \ingroup LinkedList
  */
 void vListInitialiseItem( ListItem_t * const pxItem ) PRIVILEGED_FUNCTION;
+//@ requires true;
+//@ ensures true;
 
 /*
  * Insert a list item into a list.  The item will be inserted into the list in

tasks.c

@@ -29,6 +29,7 @@
     #include "verifast_proof_defs.h"
     #include "task_predicates.h"
     #include "verifast_RP2040_axioms.h"
+    #include "verifast_prelude_extended.h"
 #endif
 
 /* Standard includes. */
@@ -1546,6 +1547,11 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
              * string is not accessible (extremely unlikely). */
             if( pcName[ x ] == ( char ) 0x00 )
             {
+                /* TODO: Why does VeriFast not report a loop invariant
+                 *       violation when we don't close the predicate?
+                 *       This seems like a bug.
+                 */
+                //@ close TCB_p(_, _);
                 break;
             }
             else
@@ -1555,15 +1561,19 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
             //@ close TCB_p(_, _);
         }
 
+        //@ open TCB_p(_, _);
         /* Ensure the name string is terminated in the case that the string length
          * was greater or equal to configMAX_TASK_NAME_LEN. */
         pxNewTCB->pcTaskName[ configMAX_TASK_NAME_LEN - 1 ] = '\0';
+        //@ close TCB_p(_, _);
     }
     else
     {
+        //@ open TCB_p(_, _);
         /* The task has not been given a name, so just ensure there is a NULL
          * terminator when it is read out. */
         pxNewTCB->pcTaskName[ 0 ] = 0x00;
+        //@ close TCB_p(_, _);
     }
 
     /* This is used as an array index so must ensure it's not too large.  First
@@ -1577,6 +1587,7 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
         mtCOVERAGE_TEST_MARKER();
     }
 
+    //@ open TCB_p(_, _);
     pxNewTCB->uxPriority = uxPriority;
     #if ( configUSE_MUTEXES == 1 )
         {
@@ -1584,10 +1595,13 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
             pxNewTCB->uxMutexesHeld = 0;
         }
     #endif /* configUSE_MUTEXES */
+    //@ close TCB_p(_, _);
 
     vListInitialiseItem( &( pxNewTCB->xStateListItem ) );
     vListInitialiseItem( &( pxNewTCB->xEventListItem ) );
 
+    //@ open TCB_p(_, _);
+
     /* Set the pxNewTCB as a link back from the ListItem_t.  This is so we can get
      * back to  the containing TCB from a generic item in a list. */
     listSET_LIST_ITEM_OWNER( &( pxNewTCB->xStateListItem ), pxNewTCB );
@@ -1627,12 +1641,20 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
 
     #if ( configNUM_THREAD_LOCAL_STORAGE_POINTERS != 0 )
         {
+            //@ pointers__to_chars_(pxNewTCB->pvThreadLocalStoragePointers);
+            //@ assert(chars_((char*) pxNewTCB->pvThreadLocalStoragePointers, _, _));
+            //@ assert(chars_(_, sizeof( pxNewTCB->pvThreadLocalStoragePointers ), _));
             memset( ( void * ) &( pxNewTCB->pvThreadLocalStoragePointers[ 0 ] ), 0x00, sizeof( pxNewTCB->pvThreadLocalStoragePointers ) );
         }
     #endif
 
     #if ( configUSE_TASK_NOTIFICATIONS == 1 )
         {
+            ///@ assert( integers__(pxNewTCB->ulNotifiedValue, _, _, 1, _) );
+            ///@ integers___to_integers_(pxNewTCB->ulNotifiedValue);
+        	///@ integers__to_chars(pxNewTCB->ulNotifiedValue);
+            //@integers___to_integers_(pxNewTCB->ulNotifiedValue);
+            //@ integers__to_chars(pxNewTCB->ulNotifiedValue);
             memset( ( void * ) &( pxNewTCB->ulNotifiedValue[ 0 ] ), 0x00, sizeof( pxNewTCB->ulNotifiedValue ) );
             memset( ( void * ) &( pxNewTCB->ucNotifyState[ 0 ] ), 0x00, sizeof( pxNewTCB->ucNotifyState ) );
         }
@@ -1748,6 +1770,8 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
     {
         mtCOVERAGE_TEST_MARKER();
     }
+
+    //@ close TCB_p(_, _);
 }
 /*-----------------------------------------------------------*/
 

verification/verifast/proof/task_predicates.h

@@ -36,9 +36,11 @@ predicate TCB_p(TCB_t * tcb, int stackSize) =
     tcb->uxMutexesHeld |-> _ &*&
 
     // void * pvThreadLocalStoragePointers[ 5 ];
-    pointers_(tcb->pvThreadLocalStoragePointers, _, _) &*&
+    pointers_(tcb->pvThreadLocalStoragePointers, 5, _) &*&
 
-    integers__(tcb->ulNotifiedValue, _, _, _, _) &*&
+    // We assume that the macro `configTASK_NOTIFICATION_ARRAY_ENTRIES`
+    // evaluates to 1.
+    integers__(tcb->ulNotifiedValue, 4, false, 1, _) &*&
     
     uchars_(tcb->ucNotifyState, 1, _) &*&
 

verification/verifast/proof/verifast_prelude_extended.h

@@ -0,0 +1,53 @@
+#ifndef VERIFAST_PRELUDE_EXTENDED_H
+#define VERIFAST_PRELUDE_EXTENDED_H
+
+/* This file contains axioms that would naturally fit into prelude.h
+ * but are missing.
+ */
+
+/* Reminder:
+
+predicate chars_(char *array, int count; list<option<char> > cs) =
+    count == 0 ?
+        cs == nil
+    :
+        char_(array, ?c) &*& chars_(array + 1, count - 1, ?cs0) &*& cs == cons(c, cs0);
+
+predicate chars(char *array, int count; list<char> cs) =
+    count == 0 ?
+        cs == nil
+    :
+        character(array, ?c) &*& chars(array + 1, count - 1, ?cs0) &*& cs == cons(c, cs0);
+
+
+lemma_auto void chars__to_chars(char *array);
+    requires [?f]chars_(array, ?count, ?cs) &*& cs == map(some, map(the, cs));
+    ensures [f]chars(array, count, map(the, cs));
+
+
+
+predicate integers__(void *p, int size, bool signed_, int count; list<option<int> > vs) =
+    count == 0 ?
+        vs == nil
+    :
+        integer__(p, size, signed_, ?v0) &*& integers__(p + size, size, signed_, count - 1, ?vs0) &*& vs == cons(v0, vs0);
+
+predicate integers_(void *p, int size, bool signed_, int count; list<int> vs) =
+    count == 0 ?
+        vs == nil
+    :
+        integer_(p, size, signed_, ?v0) &*& integers_(p + size, size, signed_, count - 1, ?vs0) &*& vs == cons(v0, vs0);
+
+
+ */
+
+
+
+
+/*@
+lemma_auto void integers___to_integers_(void *p);
+    requires [?f]integers__(p, ?size, ?signed_, ?count, _);
+    ensures [f]integers_(p, size, signed_, count, _);
+@*/
+
+#endif /* VERIFAST_PRELUDE_EXTENDED_H */