| 29 | #include "proof/queue.h" |
| 30 | |
| 31 | static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, |
| 32 | const void * pvItemToQueue, |
| 33 | const BaseType_t xPosition ) |
| 34 | /*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& |
| 35 | (K < N || xPosition == queueOVERWRITE) &*& |
| 36 | chars(pvItemToQueue, M, ?x) &*& |
| 37 | (xPosition == queueSEND_TO_BACK || xPosition == queueSEND_TO_FRONT || (xPosition == queueOVERWRITE && N == 1));@*/ |
| 38 | /*@ensures |
| 39 | (xPosition == queueSEND_TO_BACK |
| 40 | ? queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x))) |
| 41 | : (xPosition == queueSEND_TO_FRONT |
| 42 | ? (R == 0 |
| 43 | ? queue(pxQueue, Storage, N, M, W, (N-1), (K+1), is_locked, cons(x, abs)) |
| 44 | : queue(pxQueue, Storage, N, M, W, (R-1), (K+1), is_locked, cons(x, abs))) |
| 45 | : xPosition == queueOVERWRITE &*& queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x))) |
| 46 | ) &*& |
| 47 | chars(pvItemToQueue, M, x);@*/ |
| 48 | { |
| 49 | BaseType_t xReturn = pdFALSE; |
| 50 | UBaseType_t uxMessagesWaiting; |
| 51 | |
| 52 | /* This function is called from a critical section. */ |
| 53 | |
| 54 | uxMessagesWaiting = pxQueue->uxMessagesWaiting; |
| 55 | |
| 56 | /* The abstract list of list of chars of `Storage` is `contents` */ |
| 57 | /*@assert buffer(Storage, N, M, ?contents);@*/ |
| 58 | if( pxQueue->uxItemSize == ( UBaseType_t ) 0 ) |
| 59 | { |
| 60 | /* This case is unreachable for queues */ |
| 61 | /*@assert false;@*/ |
| 62 | #if ( configUSE_MUTEXES == 1 ) |
| 63 | { |
| 64 | if( pxQueue->uxQueueType == queueQUEUE_IS_MUTEX ) |
| 65 | { |
| 66 | /* The mutex is no longer being held. */ |
| 67 | xReturn = xTaskPriorityDisinherit( pxQueue->u.xSemaphore.xMutexHolder ); |
| 68 | pxQueue->u.xSemaphore.xMutexHolder = NULL; |
| 69 | } |
| 70 | else |
| 71 | { |
| 72 | mtCOVERAGE_TEST_MARKER(); |
| 73 | } |
| 74 | } |
| 75 | #endif /* configUSE_MUTEXES */ |
| 76 | } |
| 77 | else if( xPosition == queueSEND_TO_BACK ) |
| 78 | { |
| 79 | #ifdef VERIFAST /*< void cast of unused return value */ |
| 80 | /* Now we focus the proof on the logical element of the buffer that |
| 81 | * will be updated using the following lemma to split the buffer into 3 |
| 82 | * parts: a prefix, the element we want to update, and the suffix. This |
| 83 | * enables the subsequent memcpy to verify. */ |
| 84 | /*@split_element(Storage, N, M, W);@*/ |
| 85 | /*@assert |
| 86 | buffer(Storage, W, M, ?prefix) &*& |
| 87 | chars(Storage + W * M, M, _) &*& |
| 88 | buffer(Storage + (W + 1) * M, (N-1-W), M, ?suffix);@*/ |
no test coverage detected