diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c index ec8e5f0cd..9ad48cd73 100644 --- a/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c +++ b/FreeRTOS/Test/VeriFast/queue/xQueueIsQueueFullFromISR.c @@ -1,6 +1,6 @@ /* * FreeRTOS V202112.00 - * Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved. + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. * * Permission is hereby granted, free of charge, to any person obtaining a copy of * this software and associated documentation files (the "Software"), to deal in @@ -24,21 +24,22 @@ * */ +/* *INDENT-OFF* */ + #include "proof/queue.h" BaseType_t xQueueIsQueueFullFromISR( const QueueHandle_t xQueue ) /*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs);@*/ - /*@ensures queue(xQueue, Storage, N, M, W, R, K, is_locked, abs) &*& - * result == ((K == N) ? pdTRUE : pdFALSE);@*/ + result == ((K == N) ? pdTRUE : pdFALSE);@*/ { BaseType_t xReturn; - #ifdef VERIFAST /*< const pointer declaration */ - Queue_t * pxQueue = xQueue; - #else - Queue_t * const pxQueue = xQueue; - #endif +#ifdef VERIFAST /*< const pointer declaration */ + Queue_t * pxQueue = xQueue; +#else + Queue_t * const pxQueue = xQueue; +#endif configASSERT( pxQueue ); @@ -53,3 +54,5 @@ BaseType_t xQueueIsQueueFullFromISR( const QueueHandle_t xQueue ) return xReturn; } /*lint !e818 xQueue could not be pointer to const because it is a typedef. */ + +/* *INDENT-ON* */ |