summaryrefslogtreecommitdiff
path: root/FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/TaskDelay_harness.c
diff options
context:
space:
mode:
Diffstat (limited to 'FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/TaskDelay_harness.c')
-rw-r--r--FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/TaskDelay_harness.c23
1 files changed, 11 insertions, 12 deletions
diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/TaskDelay_harness.c b/FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/TaskDelay_harness.c
index 2ef21dedb..d38eb5579 100644
--- a/FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/TaskDelay_harness.c
+++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/TaskDelay_harness.c
@@ -40,8 +40,9 @@ BaseType_t xTaskResumeAllStub( void );
* This is a trick to overcome the "redefined twice" error
* when stubbing out the `xTaskResumeAll` function in the header
*/
-BaseType_t xTaskResumeAll( void ) {
- return xTaskResumeAllStub();
+BaseType_t xTaskResumeAll( void )
+{
+ return xTaskResumeAllStub();
}
/*
@@ -50,16 +51,14 @@ BaseType_t xTaskResumeAll( void ) {
*/
void harness()
{
- TickType_t xTicksToDelay;
- BaseType_t xTasksPrepared;
+ TickType_t xTicksToDelay;
+ BaseType_t xTasksPrepared;
- vSetGlobalVariables();
- xTasksPrepared = xPrepareTaskLists();
+ vSetGlobalVariables();
+ xTasksPrepared = xPrepareTaskLists();
- if ( xTasksPrepared != pdFAIL )
- {
- vTaskDelay( xTicksToDelay );
- }
+ if( xTasksPrepared != pdFAIL )
+ {
+ vTaskDelay( xTicksToDelay );
+ }
}
-
-