diff options
Diffstat (limited to 'FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c')
| -rw-r--r-- | FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c | 39 |
1 files changed, 20 insertions, 19 deletions
diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c b/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c index 6331c785b..148fa1ca2 100644 --- a/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/TaskCreate_harness.c @@ -33,31 +33,32 @@ void vNondetSetCurrentTCB( void ); void vSetGlobalVariables( void ); void vPrepareTaskLists( void ); -TaskHandle_t *pxNondetSetTaskHandle( void ); -char *pcNondetSetString( size_t xSizeLength ); +TaskHandle_t * pxNondetSetTaskHandle( void ); +char * pcNondetSetString( size_t xSizeLength ); void harness() { - TaskFunction_t pxTaskCode; - char * pcName; - configSTACK_DEPTH_TYPE usStackDepth = STACK_DEPTH; - void * pvParameters; - TaskHandle_t * pxCreatedTask; + TaskFunction_t pxTaskCode; + char * pcName; + configSTACK_DEPTH_TYPE usStackDepth = STACK_DEPTH; + void * pvParameters; + TaskHandle_t * pxCreatedTask; + + UBaseType_t uxPriority; - UBaseType_t uxPriority; __CPROVER_assume( uxPriority < configMAX_PRIORITIES ); - vNondetSetCurrentTCB(); - vSetGlobalVariables(); - vPrepareTaskLists(); + vNondetSetCurrentTCB(); + vSetGlobalVariables(); + vPrepareTaskLists(); - pxCreatedTask = pxNondetSetTaskHandle(); - pcName = pcNondetSetString( configMAX_TASK_NAME_LEN ); + pxCreatedTask = pxNondetSetTaskHandle(); + pcName = pcNondetSetString( configMAX_TASK_NAME_LEN ); - xTaskCreate(pxTaskCode, - pcName, - usStackDepth, - pvParameters, - uxPriority, - pxCreatedTask ); + xTaskCreate( pxTaskCode, + pcName, + usStackDepth, + pvParameters, + uxPriority, + pxCreatedTask ); } |