Change uxPendedTicks to xPendedTicks in all proofs (#1758)

This ensures that CBMC proofs are able to build after the name-change in
commit 23839bb.

Author: karkhaz

tools/cbmc/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch

@@ -65,12 +65,15 @@ index ff657733..8b57d198 100644
  PRIVILEGED_DATA static List_t xPendingReadyList;						/*< Tasks that have been readied while the scheduler was suspended.  They will be moved to the ready list when the scheduler is resumed. */
 
  #if( INCLUDE_vTaskDelete == 1 )
-@@ -368,7 +368,7 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks 	= ( UBaseTyp
+@@ -368,10 +368,10 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks 	= ( UBaseTyp
+ 
+ /* Other file private variables. --------------------------------*/
+ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks 	= ( UBaseType_t ) 0U;
  PRIVILEGED_DATA static volatile TickType_t xTickCount 				= ( TickType_t ) configINITIAL_TICK_COUNT;
  PRIVILEGED_DATA static volatile UBaseType_t uxTopReadyPriority 		= tskIDLE_PRIORITY;
  PRIVILEGED_DATA static volatile BaseType_t xSchedulerRunning 		= pdFALSE;
--PRIVILEGED_DATA static volatile UBaseType_t uxPendedTicks 			= ( UBaseType_t ) 0U;
-+PRIVILEGED_DATA static UBaseType_t uxPendedTicks 					= ( UBaseType_t ) 0U;
+-PRIVILEGED_DATA static volatile TickType_t xPendedTicks 			= ( TickType_t ) 0U;
++PRIVILEGED_DATA static TickType_t xPendedTicks 			= ( TickType_t ) 0U;
  PRIVILEGED_DATA static volatile BaseType_t xYieldPending 			= pdFALSE;
  PRIVILEGED_DATA static volatile BaseType_t xNumOfOverflows 			= ( BaseType_t ) 0;
  PRIVILEGED_DATA static UBaseType_t uxTaskNumber 					= ( UBaseType_t ) 0U;

tools/cbmc/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch

@@ -6,17 +6,17 @@ index 17a6964e..24a40c29 100644
  	 * Checks to see if a queue is a member of a queue set, and if so, notifies
  	 * the queue set that the queue contains data.
  	 */
--	static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition ) PRIVILEGED_FUNCTION;
-+	BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition ) PRIVILEGED_FUNCTION;
+-	static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
++	BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
  #endif
 
  /*
 @@ -2887,7 +2887,7 @@ Queue_t * const pxQueue = xQueue;
 
  #if ( configUSE_QUEUE_SETS == 1 )
 
--	static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition )
-+	BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition )
+-	static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue )
++	BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue )
  	{
  	Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer;
  	BaseType_t xReturn = pdFALSE;

tools/cbmc/proofs/Queue/QueueGenericSend/QueueGenericSend_harness.c

@@ -59,7 +59,7 @@ BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueu
 	}
 }
 #else
-	BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue, const BaseType_t xCopyPosition )
+	BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue )
 	{
 		Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer;
 		configASSERT( pxQueueSetContainer );
@@ -69,7 +69,7 @@ BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueu
 		configASSERT( pxQueue );
 		if( pxQueue->pxQueueSetContainer != NULL )
 		{
-			prvNotifyQueueSetContainer(pxQueue, queueSEND_TO_BACK);
+			prvNotifyQueueSetContainer(pxQueue);
 		}
 		listLIST_IS_EMPTY( &( pxQueue->xTasksWaitingToReceive ) );
 		pxQueue->cTxLock = queueUNLOCKED;

tools/cbmc/proofs/TaskPool/TaskDelay/README.md

@@ -2,7 +2,7 @@ This proof demonstrates the memory safety of the TaskDelay function.  We assume
 that `pxCurrentTCB` is initialized and inserted in one of the ready tasks lists
 (with and without another task in the same list). We abstract function
 `xTaskResumeAll` by assuming that `xPendingReadyList` is empty and
-`uxPendedTicks` is `0`. Finally, we assume nondeterministic values for global
+`xPendedTicks` is `0`. Finally, we assume nondeterministic values for global
 variables `xTickCount` and `xNextTaskUnblockTime`, and `pdFALSE` for
 `uxSchedulerSuspended` (to avoid assertion failure).
 

tools/cbmc/proofs/TaskPool/TaskDelay/tasks_test_access_functions.h

@@ -124,7 +124,7 @@ BaseType_t xPrepareTaskLists( void )
 /*
  * We stub out `xTaskResumeAll` including the assertion and change on
  * variables `uxSchedulerSuspended`. We assume that `xPendingReadyList`
- * is empty to avoid the first loop, and uxPendedTicks to avoid the second
+ * is empty to avoid the first loop, and xPendedTicks to avoid the second
  * one. Finally, we return a nondeterministic value (overapproximation)
  */
 BaseType_t xTaskResumeAllStub( void )
@@ -137,7 +137,7 @@ BaseType_t xTaskResumeAllStub( void )
 	{
 		--uxSchedulerSuspended;
 		__CPROVER_assert( listLIST_IS_EMPTY( &xPendingReadyList ), "Pending ready tasks list not empty." );
-		__CPROVER_assert( uxPendedTicks == 0 , "uxPendedTicks is not equal to zero.");
+		__CPROVER_assert( xPendedTicks == 0 , "xPendedTicks is not equal to zero.");
 	}
 	taskEXIT_CRITICAL();
 

tools/cbmc/proofs/TaskPool/TaskIncrementTick/tasks_test_access_functions.h

@@ -72,7 +72,7 @@ TaskHandle_t xUnconstrainedTCB( void )
  */
 void vSetGlobalVariables()
 {
-	uxPendedTicks = nondet_ubasetype();
+	xPendedTicks = nondet_ubasetype();
 	uxSchedulerSuspended = nondet_ubasetype();
 	xYieldPending = nondet_basetype();
 	xTickCount = nondet_ticktype();

tools/cbmc/proofs/TaskPool/TaskResumeAll/README.md

@@ -1,7 +1,7 @@
 This proof demonstrates the memory safety of the TaskResumeAll function.  We
 assume that task lists are initialized and filled with a few list items. We
 also assume that some global variables are set to a nondeterministic value,
-except for `uxSchedulerSuspended` which cannot be 0 and `uxPendedTicks` which
+except for `uxSchedulerSuspended` which cannot be 0 and `xPendedTicks` which
 is either `1` (to unwind a loop in a reasonable amount of time) or `0`.
 
 Configurations available:

tools/cbmc/proofs/TaskPool/TaskResumeAll/tasks_test_access_functions.h

@@ -67,7 +67,7 @@ TaskHandle_t xUnconstrainedTCB( void )
 }
 
 /*
- * We set uxPendedTicks since __CPROVER_assume does not work
+ * We set xPendedTicks since __CPROVER_assume does not work
  * well with statically initialised variables
  */
 void vSetGlobalVariables( void ) {
@@ -76,7 +76,7 @@ void vSetGlobalVariables( void ) {
 	__CPROVER_assume( uxNonZeroValue != 0 );
 
 	uxSchedulerSuspended = uxNonZeroValue;
-	uxPendedTicks = nondet_bool() ? PENDED_TICKS : 0;
+	xPendedTicks = nondet_bool() ? PENDED_TICKS : 0;
 	uxCurrentNumberOfTasks = nondet_ubasetype();
 	xTickCount = nondet_ticktype();
 }