diff options
Diffstat (limited to 'FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/QueueMessagesWaiting_harness.c')
| -rw-r--r-- | FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/QueueMessagesWaiting_harness.c | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/QueueMessagesWaiting_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/QueueMessagesWaiting_harness.c index 8e5f3d050..2a2bef755 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/QueueMessagesWaiting_harness.c +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/QueueMessagesWaiting_harness.c @@ -32,10 +32,12 @@ #include "cbmc.h" -void harness(){ - QueueHandle_t xQueue = pvPortMalloc(sizeof(Queue_t)); +void harness() +{ + QueueHandle_t xQueue = pvPortMalloc( sizeof( Queue_t ) ); - if(xQueue){ - uxQueueMessagesWaiting( xQueue ); - } + if( xQueue ) + { + uxQueueMessagesWaiting( xQueue ); + } } |