begriffs open source - cmsis-freertos/blob - Test/VeriFast/include/proof/queue.h

   1 /*
   2  * FreeRTOS V202104.00
   3  * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
   4  *
   5  * Permission is hereby granted, free of charge, to any person obtaining a copy of
   6  * this software and associated documentation files (the "Software"), to deal in
   7  * the Software without restriction, including without limitation the rights to
   8  * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
   9  * the Software, and to permit persons to whom the Software is furnished to do so,
  10  * subject to the following conditions:
  11  *
  12  * The above copyright notice and this permission notice shall be included in all
  13  * copies or substantial portions of the Software.
  14  *
  15  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  16  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
  17  * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
  18  * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
  19  * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  20  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  21  */
  22
  23 #ifndef QUEUE_H
  24 #define QUEUE_H
  25
  26 #define VERIFAST
  27 #include <stdlib.h>
  28 #include <stdint.h>
  29 #include <string.h>
  30 #include <threading.h>
  31 /*@#include "common.gh"@*/
  32
  33 typedef size_t TickType_t;
  34 typedef size_t UBaseType_t;
  35 typedef ssize_t BaseType_t;
  36
  37 /* Empty/no-op macros */
  38 /* Tracing */
  39 #define traceBLOCKING_ON_QUEUE_PEEK(x)
  40 #define traceBLOCKING_ON_QUEUE_RECEIVE(x)
  41 #define traceBLOCKING_ON_QUEUE_SEND(x)
  42 #define traceQUEUE_CREATE(x)
  43 #define traceQUEUE_CREATE_FAILED(x)
  44 #define traceQUEUE_DELETE(x)
  45 #define traceQUEUE_PEEK(x)
  46 #define traceQUEUE_PEEK_FAILED(x)
  47 #define traceQUEUE_PEEK_FROM_ISR(x)
  48 #define traceQUEUE_PEEK_FROM_ISR_FAILED(x)
  49 #define traceQUEUE_RECEIVE(x)
  50 #define traceQUEUE_RECEIVE_FAILED(x)
  51 #define traceQUEUE_RECEIVE_FROM_ISR(x)
  52 #define traceQUEUE_RECEIVE_FROM_ISR_FAILED(x)
  53 #define traceQUEUE_SEND(x)
  54 #define traceQUEUE_SEND_FAILED(x)
  55 #define traceQUEUE_SEND_FROM_ISR(x)
  56 #define traceQUEUE_SEND_FROM_ISR_FAILED(x)
  57 /* Coverage */
  58 #define mtCOVERAGE_TEST_MARKER()
  59 /* Asserts */
  60 #define configASSERT(x)
  61 #define portASSERT_IF_INTERRUPT_PRIORITY_INVALID()
  62
  63 /* Map portable memory management functions */
  64 #define pvPortMalloc malloc
  65 #define vPortFree free
  66
  67 #define queueSEND_TO_BACK                     ( ( BaseType_t ) 0 )
  68 #define queueSEND_TO_FRONT                    ( ( BaseType_t ) 1 )
  69 #define queueOVERWRITE                        ( ( BaseType_t ) 2 )
  70
  71 #define pdTRUE 1
  72 #define pdFALSE 0
  73
  74 #define pdPASS pdTRUE
  75 #define pdFAIL pdFALSE
  76 #define errQUEUE_FULL 0
  77 #define errQUEUE_EMPTY 0
  78
  79 /* Constants used with the cRxLock and cTxLock structure members. */
  80 #define queueUNLOCKED             ( ( int8_t ) -1 )
  81 #define queueLOCKED_UNMODIFIED    ( ( int8_t ) 0 )
  82 #define queueINT8_MAX             ( ( int8_t ) 127 )
  83
  84 typedef struct QueuePointers
  85 {
  86     int8_t * pcTail;     /*< Points to the byte at the end of the queue storage area.  Once more byte is allocated than necessary to store the queue items, this is used as a marker. */
  87     int8_t * pcReadFrom; /*< Points to the last place that a queued item was read from when the structure is used as a queue. */
  88 } QueuePointers_t;
  89
  90 typedef struct SemaphoreData
  91 {
  92 #ifdef VERIFAST /*< do not model xMutexHolder */
  93     void *xMutexHolder;
  94 #else
  95     TaskHandle_t xMutexHolder;        /*< The handle of the task that holds the mutex. */
  96 #endif
  97     UBaseType_t uxRecursiveCallCount; /*< Maintains a count of the number of times a recursive mutex has been recursively 'taken' when the structure is used as a mutex. */
  98 } SemaphoreData_t;
  99
 100 /* VeriFast does not support unions so we replace with a struct */
 101 struct fake_union_t {
 102     QueuePointers_t xQueue;
 103     SemaphoreData_t xSemaphore;
 104 };
 105
 106 typedef struct xLIST {
 107     UBaseType_t uxNumberOfItems;
 108 #ifndef VERIFAST /*< do not model pxIndex and xListEnd of xLIST struct */
 109     struct xLIST_ITEM *pxIndex;
 110     MiniListItem_t xListEnd;
 111 #endif
 112 } List_t;
 113
 114 typedef struct QueueDefinition /* The old naming convention is used to prevent breaking kernel aware debuggers. */
 115 {
 116     int8_t * pcHead;           /*< Points to the beginning of the queue storage area. */
 117     int8_t * pcWriteTo;        /*< Points to the free next place in the storage area. */
 118
 119 #ifdef VERIFAST /*< VeriFast does not model unions */
 120     struct fake_union_t u;
 121 #else
 122     union
 123     {
 124         QueuePointers_t xQueue;     /*< Data required exclusively when this structure is used as a queue. */
 125         SemaphoreData_t xSemaphore; /*< Data required exclusively when this structure is used as a semaphore. */
 126     } u;
 127 #endif
 128
 129     List_t xTasksWaitingToSend;             /*< List of tasks that are blocked waiting to post onto this queue.  Stored in priority order. */
 130     List_t xTasksWaitingToReceive;          /*< List of tasks that are blocked waiting to read from this queue.  Stored in priority order. */
 131
 132     volatile UBaseType_t uxMessagesWaiting; /*< The number of items currently in the queue. */
 133     UBaseType_t uxLength;                   /*< The length of the queue defined as the number of items it will hold, not the number of bytes. */
 134     UBaseType_t uxItemSize;                 /*< The size of each items that the queue will hold. */
 135
 136     volatile int8_t cRxLock;                /*< Stores the number of items received from the queue (removed from the queue) while the queue was locked.  Set to queueUNLOCKED when the queue is not locked. */
 137     volatile int8_t cTxLock;                /*< Stores the number of items transmitted to the queue (added to the queue) while the queue was locked.  Set to queueUNLOCKED when the queue is not locked. */
 138
 139     #if ( ( configSUPPORT_STATIC_ALLOCATION == 1 ) && ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) )
 140         uint8_t ucStaticallyAllocated; /*< Set to pdTRUE if the memory used by the queue was statically allocated to ensure no attempt is made to free the memory. */
 141     #endif
 142
 143     #if ( configUSE_QUEUE_SETS == 1 )
 144         struct QueueDefinition * pxQueueSetContainer;
 145     #endif
 146
 147     #if ( configUSE_TRACE_FACILITY == 1 )
 148         UBaseType_t uxQueueNumber;
 149         uint8_t ucQueueType;
 150     #endif
 151
 152     /*@struct mutex *irqMask;@*/            /*< Ghost mutex simulates the effect of irq masking */
 153     /*@struct mutex *schedulerSuspend;@*/   /*< Ghost mutex simulates the effect of scheduler suspension */
 154     /*@struct mutex *locked;@*/             /*< Ghost mutex simulates the effect of queue locking */
 155 } xQUEUE;
 156
 157 typedef xQUEUE Queue_t;
 158
 159 typedef struct QueueDefinition * QueueHandle_t;
 160
 161 /*@
 162 #define QUEUE_SHAPE(q, Storage, N, M, K)                 \
 163     malloc_block_QueueDefinition(q) &*&                  \
 164     q->pcHead |-> Storage &*&                            \
 165     q->pcWriteTo |-> ?WPtr &*&                           \
 166     q->u.xQueue.pcTail |-> ?End &*&                      \
 167     q->u.xQueue.pcReadFrom |-> ?RPtr &*&                 \
 168     q->uxItemSize |-> M &*&                              \
 169     q->uxLength |-> N &*&                                \
 170     q->uxMessagesWaiting |-> K &*&                       \
 171     q->cRxLock |-> ?rxLock &*&                           \
 172     q->cTxLock |-> ?txLock &*&                           \
 173     struct_QueuePointers_padding(&q->u.xQueue) &*&       \
 174     struct_SemaphoreData_padding(&q->u.xSemaphore) &*&   \
 175     struct_fake_union_t_padding(&q->u) &*&               \
 176     struct_xLIST_padding(&q->xTasksWaitingToSend) &*&    \
 177     struct_xLIST_padding(&q->xTasksWaitingToReceive) &*& \
 178     q->u.xSemaphore.xMutexHolder |-> _ &*&               \
 179     q->u.xSemaphore.uxRecursiveCallCount |-> _ &*&       \
 180     true
 181
 182 predicate queue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) =
 183     QUEUE_SHAPE(q, Storage, N, M, K) &*&
 184     0 < N &*&
 185     0 < M &*&
 186     0 <= W &*& W < N &*&
 187     0 <= R &*& R < N &*&
 188     0 <= K &*& K <= N &*&
 189     W == (R + 1 + K) % N &*&
 190     (-1) <= rxLock &*&
 191     (-1) <= txLock &*&
 192     (is_locked ? 0 <= rxLock : (-1) == rxLock) &*&
 193     (is_locked ? 0 <= txLock : (-1) == txLock) &*&
 194     WPtr == Storage + (W*M) &*&
 195     RPtr == Storage + (R*M) &*&
 196     End == Storage + (N*M) &*&
 197     buffer(Storage, N, M, ?contents) &*&
 198     length(contents) == N &*&
 199     abs == take(K, rotate_left((R+1)%N, contents)) &*&
 200     malloc_block(Storage, N*M) &*&
 201     true
 202     ;
 203 @*/
 204
 205 /* A buffer allows us to interpret a flat character array of `N*M` bytes as a
 206 list of `N` elements where each element is `M` bytes */
 207 /*@
 208 predicate buffer(char *buffer, size_t N, size_t M; list<list<char> > elements) =
 209     N == 0
 210         ? elements == nil
 211         : chars(buffer, M, ?x) &*& buffer(buffer + M, N - 1, M, ?xs) &*& elements == cons(x, xs);
 212
 213 lemma void buffer_length(char *buffer, size_t N, size_t M)
 214 requires buffer(buffer, N, M, ?elements);
 215 ensures buffer(buffer, N, M, elements) &*& length(elements) == N;
 216 {
 217     if (N == 0) {
 218         open buffer(buffer, N, M, elements);
 219         close buffer(buffer, N, M, elements);
 220     } else {
 221         open buffer(buffer, N, M, elements);
 222         buffer_length(buffer+M, N-1, M);
 223     }
 224 }
 225 @*/
 226
 227 /*
 228 There is no need in the queue proofs to preserve a relationship between `cs`
 229 and `elements` (i.e., `flatten(elements) == cs`) because we only move in one
 230 direction from `cs` to `elements` during queue creation when the contents is
 231 fresh from `malloc` (i.e., uninitialized). If we needed to do a roundtrip from
 232 elements back to cs then this would require a stronger lemma.
 233 */
 234 /*@
 235 lemma void buffer_from_chars(char *buffer, size_t N, size_t M)
 236 requires chars(buffer, N*M, ?cs) &*& 0 <= N &*& 0 < M;
 237 ensures exists<list<list<char> > >(?elements) &*& buffer(buffer, N, M, elements) &*& length(elements) == N;
 238 {
 239     if (N == 0) {
 240         close exists(nil);
 241     } else {
 242         int i = 0;
 243         while (i < N)
 244         invariant 0 <= i &*& i <= N &*&
 245             chars(buffer, (N-i)*M, ?xs) &*& xs == take((N-i)*M, cs) &*&
 246             buffer(buffer + (N-i)*M, i, M, ?ys);
 247         decreases N-i;
 248         {
 249             mul_mono_l(0, N-i-1, M);
 250             chars_split(buffer, (N-i-1)*M);
 251             mul_mono_l(i, N, M);
 252             mul_mono_l(N-i, N, M);
 253             take_take((N-i-1)*M, (N-i)*M, cs);
 254             i++;
 255         }
 256         close exists(ys);
 257         buffer_length(buffer, N, M);
 258     }
 259 }
 260
 261 lemma void append_buffer(char *buffer, size_t N1, size_t N2, size_t M)
 262 requires
 263     buffer(buffer, N1, M, ?elements1) &*&
 264     buffer(buffer + N1 * M, N2, M, ?elements2) &*&
 265     0 <= N1 &*& 0 <= N2;
 266 ensures buffer(buffer, N1+N2, M, append(elements1, elements2));
 267 {
 268     if (N1 == 0) {
 269         open buffer(buffer, 0, M, _);
 270     } else if (N2 == 0) {
 271         open buffer(buffer + N1 * M, 0, M, _);
 272     } else {
 273         open buffer(buffer, N1, M, elements1);
 274         append_buffer(buffer + M, N1-1, N2, M);
 275         close buffer(buffer, N1+N2, M, cons(?x, append(xs, elements2)));
 276     }
 277 }
 278
 279 lemma void split_element<t>(char *buffer, size_t N, size_t M, size_t i)
 280 requires buffer(buffer, N, M, ?elements) &*& 0 <= i &*& i < N;
 281 ensures
 282     buffer(buffer, i, M, take(i, elements)) &*&
 283     chars(buffer + i * M, M, nth(i, elements)) &*&
 284     buffer(buffer + (i + 1) * M, (N-1-i), M, drop(i+1, elements));
 285 {
 286     if (i == 0) {
 287         // straightforward
 288     } else {
 289         buffer_length(buffer, N, M);
 290         int j = 0;
 291         while (j < i)
 292         invariant 0 <= j &*& j <= i &*&
 293             buffer(buffer, j, M, take(j, elements)) &*&
 294             buffer(buffer + j * M, N-j, M, drop(j, elements));
 295         decreases i-j;
 296         {
 297             drop_drop(1, j, elements);
 298             nth_drop2(elements, j);
 299             open buffer(buffer + j * M, N-j, M, drop(j, elements));
 300             assert chars(buffer + j * M, M, ?x) &*& x == nth(j, elements);
 301             close buffer(buffer + j * M, 1, M, singleton(x));
 302             append_buffer(buffer, j, 1, M);
 303             take_plus_one(j, elements);
 304             j++;
 305         }
 306         drop_drop(1, j, elements);
 307         nth_drop2(elements, i);
 308     }
 309 }
 310
 311 lemma void join_element(char *buffer, size_t N, size_t M, size_t i)
 312 requires
 313     0 <= i &*& i < N &*&
 314     buffer(buffer, i, M, ?prefix) &*&
 315     chars(buffer + i * M, M, ?element) &*&
 316     buffer(buffer + (i + 1) * M, (N-1-i), M, ?suffix);
 317 ensures buffer(buffer, N, M, append(prefix, cons(element, suffix)));
 318 {
 319     if (i == 0) {
 320         open buffer(buffer, i, M, prefix);
 321         assert prefix == nil;
 322         close buffer(buffer, N, M, cons(element, suffix));
 323     } else {
 324         close buffer(buffer + i * M, N-i, M, cons(element, suffix));
 325         append_buffer(buffer, i, N-i, M);
 326     }
 327 }
 328
 329 predicate list(List_t *l;) =
 330     l->uxNumberOfItems |-> _;
 331
 332 predicate queuelists(QueueHandle_t q;) =
 333     list(&q->xTasksWaitingToSend) &*&
 334     list(&q->xTasksWaitingToReceive);
 335 @*/
 336
 337 /* Because prvCopyDataFromQueue does *not* decrement uxMessagesWaiting (K) the
 338 queue predicate above does not hold as a postcondition. If the caller
 339 subsequently decrements K then the queue predicate can be reinstated. */
 340 /*@
 341 predicate queue_after_prvCopyDataFromQueue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) =
 342     QUEUE_SHAPE(q, Storage, N, M, K) &*&
 343     0 < N &*&
 344     0 < M &*&
 345     0 <= W &*& W < N &*&
 346     0 <= R &*& R < N &*&
 347     0 <= K &*& K <= N &*&
 348     W == (R + K) % N &*& //< Differs from queue predicate
 349     (-1) <= rxLock &*&
 350     (-1) <= txLock &*&
 351     (is_locked ? 0 <= rxLock : (-1) == rxLock) &*&
 352     (is_locked ? 0 <= txLock : (-1) == txLock) &*&
 353     WPtr == Storage + (W*M) &*&
 354     RPtr == Storage + (R*M) &*&
 355     End == Storage + (N*M) &*&
 356     buffer(Storage, N, M, ?contents) &*&
 357     length(contents) == N &*&
 358     abs == take(K, rotate_left(R, contents)) &*& //< Differs from queue predicate
 359     malloc_block(Storage, N*M) &*&
 360     true
 361     ;
 362 @*/
 363
 364 /* Can't be called `mutex` as this clashes with VeriFast's predicate */
 365 /*@
 366 predicate freertos_mutex(QueueHandle_t q, int8_t *Storage, size_t N, size_t K;) =
 367     QUEUE_SHAPE(q, Storage, N, 0, K) &*&
 368     queuelists(q) &*&
 369     0 < N &*&
 370     0 <= K &*& K <= N &*&
 371     (-1) <= rxLock &*&
 372     (-1) <= txLock &*&
 373     WPtr == Storage &*&
 374     RPtr == Storage &*&
 375     End == Storage &*&
 376     malloc_block(Storage, 0) &*&
 377     chars(Storage, 0, _) &*&
 378     true
 379     ;
 380 @*/
 381
 382 /* A queuehandle can be shared between tasks and ISRs. Acquiring the ghost
 383 `irqMask` gives access to the core queue resources. The permissions granted
 384 after masking interrupts depends on the caller:
 385 - A task has access to the queue and the queuelists
 386 - An ISR has access to the queue and, if the queue is unlocked, the queuelists */
 387 /*@
 388 predicate queuehandle(QueueHandle_t q, size_t N, size_t M, bool is_isr;) =
 389     q->irqMask |-> ?m &*& mutex(m, irqs_masked_invariant(q, N, M, is_isr));
 390
 391 predicate_ctor irqs_masked_invariant(QueueHandle_t queue, size_t N, size_t M, bool is_isr)() =
 392     queue(queue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
 393     (is_isr && is_locked ? true : queuelists(queue));
 394 @*/
 395
 396 /* A queuesuspend can be shared between tasks. Acquiring the ghost `schedulerSuspend` gives access to the `locked` mutex. */
 397 /*@
 398 predicate_ctor scheduler_suspended_invariant(QueueHandle_t queue)() =
 399     queue->locked |-> ?m &*&
 400     mutex(m, queue_locked_invariant(queue));
 401
 402 predicate queuesuspend(QueueHandle_t q;) =
 403     q->schedulerSuspend |-> ?m &*&
 404     mutex(m, scheduler_suspended_invariant(q));
 405 @*/
 406
 407 /* A queuelock is exclusively acquired by a task. Acquiring the ghost `queuelock` gives access to the queue list resources. */
 408 /*@
 409 predicate queuelock(QueueHandle_t q;) =
 410     q->locked |-> ?m &*&
 411     mutex(m, queue_locked_invariant(q));
 412
 413 predicate_ctor queue_locked_invariant(QueueHandle_t queue)() =
 414     queuelists(queue);
 415 @*/
 416
 417 BaseType_t vListInitialise(List_t *list);
 418 /*@requires list(list);@*/
 419 /*@ensures list(list);@*/
 420
 421 BaseType_t listLIST_IS_EMPTY(List_t *list);
 422 /*@requires list->uxNumberOfItems |-> ?len;@*/
 423 /*@ensures list->uxNumberOfItems |-> len &*& result == (len == 0 ? pdTRUE : pdFALSE);@*/
 424
 425 typedef struct xTIME_OUT
 426 {
 427     BaseType_t xOverflowCount;
 428     TickType_t xTimeOnEntering;
 429 } TimeOut_t;
 430
 431 /*@
 432 predicate xTIME_OUT(struct xTIME_OUT *to;) =
 433     to->xOverflowCount |-> _ &*&
 434     to->xTimeOnEntering |-> _ &*&
 435     struct_xTIME_OUT_padding(to);
 436 @*/
 437
 438 void vTaskInternalSetTimeOutState( TimeOut_t * x);
 439 /*@requires xTIME_OUT(x);@*/
 440 /*@ensures xTIME_OUT(x);@*/
 441
 442 BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait );
 443 /*@requires xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/
 444 /*@ensures xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/
 445
 446 BaseType_t xTaskRemoveFromEventList(List_t *list);
 447 /*@requires list(list);@*/
 448 /*@ensures list(list);@*/
 449
 450 void vTaskPlaceOnEventList( List_t * const pxEventList, const TickType_t xTicksToWait );
 451 /*@requires list(pxEventList);@*/
 452 /*@ensures list(pxEventList);@*/
 453
 454 void vTaskMissedYield();
 455 /*@requires true;@*/
 456 /*@ensures true;@*/
 457
 458 void vTaskSuspendAll();
 459 /*@requires exists<QueueHandle_t>(?xQueue) &*&
 460     [1/2]xQueue->schedulerSuspend |-> ?m &*&
 461     [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/
 462 /*@ensures [1/2]xQueue->schedulerSuspend |-> m &*&
 463     mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*&
 464     xQueue->locked |-> ?m2 &*&
 465     mutex(m2, queue_locked_invariant(xQueue));@*/
 466
 467 BaseType_t xTaskResumeAll( void );
 468 /*@requires exists<QueueHandle_t>(?xQueue) &*&
 469     [1/2]xQueue->schedulerSuspend |-> ?m &*&
 470     mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*&
 471     xQueue->locked |-> ?m2 &*&
 472     mutex(m2, queue_locked_invariant(xQueue));@*/
 473 /*@ensures [1/2]xQueue->schedulerSuspend |-> m &*&
 474     [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/
 475
 476 void prvLockQueue( QueueHandle_t xQueue );
 477 /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
 478     [1/2]queuelock(xQueue); @*/
 479 /*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
 480     [1/2]xQueue->locked |-> ?m &*&
 481     mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*&
 482     queue_locked_invariant(xQueue)();@*/
 483
 484 void prvUnlockQueue( QueueHandle_t xQueue );
 485 /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
 486     [1/2]xQueue->locked |-> ?m &*&
 487     mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*&
 488     queue_locked_invariant(xQueue)();@*/
 489 /*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
 490     [1/2]queuelock(xQueue);@*/
 491
 492 void setInterruptMask(QueueHandle_t xQueue)
 493 /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/
 494 /*@ensures [1/2]xQueue->irqMask |-> ?m &*&
 495     mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*&
 496     queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
 497     queuelists(xQueue);@*/
 498 {
 499     /*@open queuehandle(xQueue, N, M, is_isr);@*/
 500     mutex_acquire(xQueue->irqMask);
 501     /*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/
 502 }
 503
 504 void clearInterruptMask(QueueHandle_t xQueue)
 505 /*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
 506     [1/2]xQueue->irqMask |-> ?m &*&
 507     mutex_held(m, irqs_masked_invariant(xQueue, N, M, false), currentThread, 1/2) &*&
 508     queuelists(xQueue);@*/
 509 /*@ensures [1/2]queuehandle(xQueue, N, M, false);@*/
 510 {
 511     /*@close irqs_masked_invariant(xQueue, N, M, false)();@*/
 512     mutex_release(xQueue->irqMask);
 513     /*@close [1/2]queuehandle(xQueue, N, M, false);@*/
 514 }
 515
 516 #define taskENTER_CRITICAL() setInterruptMask(xQueue)
 517 #define taskEXIT_CRITICAL() clearInterruptMask(xQueue)
 518 #define portYIELD_WITHIN_API()
 519 #define queueYIELD_IF_USING_PREEMPTION()
 520
 521 UBaseType_t setInterruptMaskFromISR(QueueHandle_t xQueue)
 522 /*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true;@*/
 523 /*@ensures [1/2]xQueue->irqMask |-> ?m &*&
 524     mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*&
 525     queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
 526     (is_locked ? true : queuelists(xQueue));@*/
 527 {
 528     /*@open queuehandle(xQueue, N, M, is_isr);@*/
 529     mutex_acquire(xQueue->irqMask);
 530     /*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/
 531     return 0;
 532 }
 533
 534 void clearInterruptMaskFromISR(QueueHandle_t xQueue, UBaseType_t uxSavedInterruptStatus)
 535 /*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
 536     [1/2]xQueue->irqMask |-> ?m &*&
 537     mutex_held(m, irqs_masked_invariant(xQueue, N, M, true), currentThread, 1/2) &*&
 538     (is_locked ? true : queuelists(xQueue));@*/
 539 /*@ensures [1/2]queuehandle(xQueue, N, M, true);@*/
 540 {
 541     /*@close irqs_masked_invariant(xQueue, N, M, true)();@*/
 542     mutex_release(xQueue->irqMask);
 543     /*@close [1/2]queuehandle(xQueue, N, M, true);@*/
 544 }
 545
 546 #define portSET_INTERRUPT_MASK_FROM_ISR() setInterruptMaskFromISR(xQueue)
 547 #define portCLEAR_INTERRUPT_MASK_FROM_ISR(uxSavedInterruptStatus) clearInterruptMaskFromISR(xQueue, uxSavedInterruptStatus)
 548
 549 #endif /* QUEUE_H */