1 files changed, 31 insertions, 25 deletions

diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/QueuePeek_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/QueuePeek_harness.c
index 53c2c9050..019c47499 100644
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/QueuePeek_harness.c
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/QueuePeek_harness.c
@@ -34,46 +34,52 @@
 #include "cbmc.h"
 
 #ifndef LOCK_BOUND
-	#define LOCK_BOUND 4
+    #define LOCK_BOUND    4
 #endif
 
 #ifndef QUEUE_PEEK_BOUND
-	#define QUEUE_PEEK_BOUND 4
+    #define QUEUE_PEEK_BOUND    4
 #endif
 
 QueueHandle_t xQueue;
 
 
 /* This method is called to initialize pxTimeOut.
-   Setting up the data structure is not interesting for the proof,
-   but the harness uses it to model a release
-   on the queue after first check. */
-void vTaskInternalSetTimeOutState( TimeOut_t * const pxTimeOut ){
-	xQueue-> uxMessagesWaiting = nondet_BaseType_t();
+ * Setting up the data structure is not interesting for the proof,
+ * but the harness uses it to model a release
+ * on the queue after first check. */
+void vTaskInternalSetTimeOutState( TimeOut_t * const pxTimeOut )
+{
+    xQueue->uxMessagesWaiting = nondet_BaseType_t();
 }
 
-void harness(){
-	xQueue = xUnconstrainedQueueBoundedItemSize(10);
+void harness()
+{
+    xQueue = xUnconstrainedQueueBoundedItemSize( 10 );
 
-	//Initialise the tasksStubs
-	vInitTaskCheckForTimeOut(0, QUEUE_PEEK_BOUND - 1);
+    /*Initialise the tasksStubs */
+    vInitTaskCheckForTimeOut( 0, QUEUE_PEEK_BOUND - 1 );
 
-	TickType_t xTicksToWait;
-	if(xState == taskSCHEDULER_SUSPENDED){
-		xTicksToWait = 0;
-	}
+    TickType_t xTicksToWait;
 
-	if(xQueue){
-		__CPROVER_assume(xQueue->cTxLock < LOCK_BOUND - 1);
-		__CPROVER_assume(xQueue->cRxLock < LOCK_BOUND - 1);
+    if( xState == taskSCHEDULER_SUSPENDED )
+    {
+        xTicksToWait = 0;
+    }
 
-		void *pvItemToQueue = pvPortMalloc(xQueue->uxItemSize);
+    if( xQueue )
+    {
+        __CPROVER_assume( xQueue->cTxLock < LOCK_BOUND - 1 );
+        __CPROVER_assume( xQueue->cRxLock < LOCK_BOUND - 1 );
 
-		/* In case malloc fails as this is otherwise an invariant violation. */
-		if(!pvItemToQueue){
-			xQueue->uxItemSize = 0;
-		}
+        void * pvItemToQueue = pvPortMalloc( xQueue->uxItemSize );
 
-		xQueuePeek( xQueue, pvItemToQueue, xTicksToWait );
-	}
+        /* In case malloc fails as this is otherwise an invariant violation. */
+        if( !pvItemToQueue )
+        {
+            xQueue->uxItemSize = 0;
+        }
+
+        xQueuePeek( xQueue, pvItemToQueue, xTicksToWait );
+    }
 }