diff options
Diffstat (limited to 'FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/QueueCreateMutex_harness.c')
| -rw-r--r-- | FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/QueueCreateMutex_harness.c | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/QueueCreateMutex_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/QueueCreateMutex_harness.c index 3528d9640..628e95423 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/QueueCreateMutex_harness.c +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/QueueCreateMutex_harness.c @@ -31,8 +31,9 @@ #include "cbmc.h" -void harness() { - uint8_t ucQueueType; +void harness() +{ + uint8_t ucQueueType; - xQueueCreateMutex(ucQueueType); + xQueueCreateMutex( ucQueueType ); } |