1 files changed, 53 insertions, 47 deletions

diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskSwitchContext/tasks_test_access_functions.h b/FreeRTOS/Test/CBMC/proofs/Task/TaskSwitchContext/tasks_test_access_functions.h
index 2b5ebff7f..b7fcddbb7 100644
--- a/FreeRTOS/Test/CBMC/proofs/Task/TaskSwitchContext/tasks_test_access_functions.h
+++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskSwitchContext/tasks_test_access_functions.h
@@ -33,38 +33,41 @@
  */
 TaskHandle_t xUnconstrainedTCB( UBaseType_t uxPriority )
 {
-	TCB_t * pxTCB = pvPortMalloc(sizeof(TCB_t));
-
-	if ( pxTCB == NULL )
-		return NULL;
-
-	/* uxPriority is set to a specific priority */
-	pxTCB->uxPriority = uxPriority;
-
-	vListInitialiseItem( &( pxTCB->xStateListItem ) );
-	vListInitialiseItem( &( pxTCB->xEventListItem ) );
-
-	listSET_LIST_ITEM_OWNER( &( pxTCB->xStateListItem ), pxTCB );
-	listSET_LIST_ITEM_OWNER( &( pxTCB->xEventListItem ), pxTCB );
-
-	if ( nondet_bool() )
-	{
-		listSET_LIST_ITEM_VALUE( &( pxTCB->xStateListItem ), pxTCB->uxPriority );
-	}
-	else
-	{
-		listSET_LIST_ITEM_VALUE( &( pxTCB->xStateListItem ), portMAX_DELAY );
-	}
-
-	if ( nondet_bool() )
-	{
-		listSET_LIST_ITEM_VALUE( &( pxTCB->xEventListItem ), ( TickType_t ) configMAX_PRIORITIES - ( TickType_t ) pxTCB->uxPriority );
-	}
-	else
-	{
-		listSET_LIST_ITEM_VALUE( &( pxTCB->xEventListItem ), portMAX_DELAY );
-	}
-	return pxTCB;
+    TCB_t * pxTCB = pvPortMalloc( sizeof( TCB_t ) );
+
+    if( pxTCB == NULL )
+    {
+        return NULL;
+    }
+
+    /* uxPriority is set to a specific priority */
+    pxTCB->uxPriority = uxPriority;
+
+    vListInitialiseItem( &( pxTCB->xStateListItem ) );
+    vListInitialiseItem( &( pxTCB->xEventListItem ) );
+
+    listSET_LIST_ITEM_OWNER( &( pxTCB->xStateListItem ), pxTCB );
+    listSET_LIST_ITEM_OWNER( &( pxTCB->xEventListItem ), pxTCB );
+
+    if( nondet_bool() )
+    {
+        listSET_LIST_ITEM_VALUE( &( pxTCB->xStateListItem ), pxTCB->uxPriority );
+    }
+    else
+    {
+        listSET_LIST_ITEM_VALUE( &( pxTCB->xStateListItem ), portMAX_DELAY );
+    }
+
+    if( nondet_bool() )
+    {
+        listSET_LIST_ITEM_VALUE( &( pxTCB->xEventListItem ), ( TickType_t ) configMAX_PRIORITIES - ( TickType_t ) pxTCB->uxPriority );
+    }
+    else
+    {
+        listSET_LIST_ITEM_VALUE( &( pxTCB->xEventListItem ), portMAX_DELAY );
+    }
+
+    return pxTCB;
 }
 
 /*
@@ -73,7 +76,7 @@ TaskHandle_t xUnconstrainedTCB( UBaseType_t uxPriority )
  */
 void vSetGlobalVariables( void )
 {
-	uxSchedulerSuspended = nondet_ubasetype();
+    uxSchedulerSuspended = nondet_ubasetype();
 }
 
 /*
@@ -82,22 +85,25 @@ void vSetGlobalVariables( void )
  */
 BaseType_t xPrepareTaskLists( void )
 {
-	TCB_t * pxTCB = NULL;
+    TCB_t * pxTCB = NULL;
+
+    __CPROVER_assert_zero_allocation();
+
+    prvInitialiseTaskLists();
+
+    for( int i = 0; i < configMAX_PRIORITIES; ++i )
+    {
+        pxTCB = xUnconstrainedTCB( i );
 
-	__CPROVER_assert_zero_allocation();
+        if( pxTCB == NULL )
+        {
+            return pdFAIL;
+        }
 
-	prvInitialiseTaskLists();
+        vListInsert( &pxReadyTasksLists[ pxTCB->uxPriority ], &( pxTCB->xStateListItem ) );
+    }
 
-	for ( int i = 0; i < configMAX_PRIORITIES; ++i )
-	{
-		pxTCB = xUnconstrainedTCB( i );
-		if ( pxTCB == NULL )
-		{
-			return pdFAIL;
-		}
-		vListInsert( &pxReadyTasksLists[ pxTCB->uxPriority ], &( pxTCB->xStateListItem ) );
-	}
-	listGET_OWNER_OF_NEXT_ENTRY( pxCurrentTCB, &pxReadyTasksLists[ configMAX_PRIORITIES - 1 ] );
+    listGET_OWNER_OF_NEXT_ENTRY( pxCurrentTCB, &pxReadyTasksLists[ configMAX_PRIORITIES - 1 ] );
 
-	return pdPASS;
+    return pdPASS;
 }