Added rewrite to remove const qualifiers from pointers.

tasks.c

@@ -62,7 +62,11 @@
     #include "verifast_bitops_extended.h"
     #include "verifast_asm.h"
 
+    //#include "verifast_lock_predicates.h"
+
     #include "snippets/rp2040_port_c_snippets.c"
+
+    #include "list.c"
 #endif
 
 /* Lint e9021, e961 and e750 are suppressed as a MISRA exception justified
@@ -1673,7 +1677,10 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
         }
     #endif /* configUSE_MUTEXES */
 
+    // TODO: Add contract
+    // TODO: Why does VeriFast not complain?
     vListInitialiseItem( &( pxNewTCB->xStateListItem ) );
+    //@ assert(false);
     vListInitialiseItem( &( pxNewTCB->xEventListItem ) );
 
 

verification/verifast/custom_build_scripts_RP2040/vf_rewrite.sh

@@ -24,6 +24,7 @@ rewrite()
 echo "Commenting out line/file pragmas"
 rewrite "^#" "// &"
 
+echo "Fixing order of 'long', 'unsigned'"
 rewrite "long unsigned int" "unsigned long int"
 
 echo "Delete fixed-sized array typedefs"
@@ -35,6 +36,9 @@ rewrite "__attribute__(([_a-z]*))" ""
 # TODO: Why does matching `\s` or `:space:` not work on MacOs?
 rewrite "__attribute__( ( [_a-z]* ) )" ""
 
+echo "Removing const qualifiers from pointers"
+rewrite "* const" "*"
+
 #echo "VF RW: 'long unsigned int' -> 'unsinged long int'"
 #echo "backup : $VF_RW_WD/$SOURCE_FILE.backup-$BACKUP_IDX"
 #echo backup index $BACKUP_IDX

verification/verifast/proof/verifast_lock_predicates.h

@@ -0,0 +1,34 @@
+#ifndef VERIFAST_LOCK_PREDICATES_H
+#define VERIFAST_LOCK_PREDICATES_H
+
+
+/* We assume that macros evaluate as follows:
+ * - `configMAX_PRIORITIES` -> 32
+*/
+/*@
+predicate tasks_global_vars() = 
+    // Lists for ready and blocked tasks.
+	//chars((char*) pxReadyTasksLists, 32 * sizeof(List_t), _) &*&
+    //chars((char*) xDelayedTaskList1) &*&
+
+    // Other file private variables. --------------------------------
+    integer_((void*) uxCurrentNumberOfTasks, sizeof(UBaseType_t), false, _) 
+    &*&
+    
+    
+    true;
+@*/
+
+
+
+void vf_validate_lock_predicaet()
+//@ requires module(tasks__pp, true);
+//@ ensures true;
+{
+ //@ open_module();
+ uxCurrentNumberOfTasks = 0;
+ 
+ //@ close tasks_global_vars();
+}
+
+#endif /* VERIFAST_LOCK_PREDICATES_H */