path: root/FreeRTOS/Test/VeriFast/include/proof/queue.h

/*
 * FreeRTOS V202112.00
 * Copyright (C) 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
 * the Software without restriction, including without limitation the rights to
 * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
 * the Software, and to permit persons to whom the Software is furnished to do so,
 * subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in all
 * copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
 * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
 * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
 * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 *
 * https://www.FreeRTOS.org
 * https://github.com/FreeRTOS
 *
 */

#ifndef QUEUE_H
#define QUEUE_H

#define VERIFAST
#include <stdlib.h>
#include <stdint.h>
#include <string.h>
#include <threading.h>
/*@#include "common.gh"@*/

typedef size_t    TickType_t;
typedef size_t    UBaseType_t;
typedef ssize_t   BaseType_t;

/* Empty/no-op macros */
/* Tracing */
#define traceBLOCKING_ON_QUEUE_PEEK( x )
#define traceBLOCKING_ON_QUEUE_RECEIVE( x )
#define traceBLOCKING_ON_QUEUE_SEND( x )
#define traceQUEUE_CREATE( x )
#define traceQUEUE_CREATE_FAILED( x )
#define traceQUEUE_DELETE( x )
#define traceQUEUE_PEEK( x )
#define traceQUEUE_PEEK_FAILED( x )
#define traceQUEUE_PEEK_FROM_ISR( x )
#define traceQUEUE_PEEK_FROM_ISR_FAILED( x )
#define traceQUEUE_RECEIVE( x )
#define traceQUEUE_RECEIVE_FAILED( x )
#define traceQUEUE_RECEIVE_FROM_ISR( x )
#define traceQUEUE_RECEIVE_FROM_ISR_FAILED( x )
#define traceQUEUE_SEND( x )
#define traceQUEUE_SEND_FAILED( x )
#define traceQUEUE_SEND_FROM_ISR( x )
#define traceQUEUE_SEND_FROM_ISR_FAILED( x )
/* Coverage */
#define mtCOVERAGE_TEST_MARKER()
/* Asserts */
#define configASSERT( x )
#define portASSERT_IF_INTERRUPT_PRIORITY_INVALID()

/* Map portable memory management functions */
#define pvPortMalloc              malloc
#define vPortFree                 free

#define queueSEND_TO_BACK         ( ( BaseType_t ) 0 )
#define queueSEND_TO_FRONT        ( ( BaseType_t ) 1 )
#define queueOVERWRITE            ( ( BaseType_t ) 2 )

#define pdTRUE                    1
#define pdFALSE                   0

#define pdPASS                    pdTRUE
#define pdFAIL                    pdFALSE
#define errQUEUE_FULL             0
#define errQUEUE_EMPTY            0

/* Constants used with the cRxLock and cTxLock structure members. */
#define queueUNLOCKED             ( ( int8_t ) -1 )
#define queueLOCKED_UNMODIFIED    ( ( int8_t ) 0 )
#define queueINT8_MAX             ( ( int8_t ) 127 )

typedef struct QueuePointers
{
    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. */
    int8_t * pcReadFrom; /*< Points to the last place that a queued item was read from when the structure is used as a queue. */
} QueuePointers_t;

typedef struct SemaphoreData
{
    #ifdef VERIFAST /*< do not model xMutexHolder */
        void * xMutexHolder;
    #else
        TaskHandle_t xMutexHolder;    /*< The handle of the task that holds the mutex. */
    #endif
    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. */
} SemaphoreData_t;

/* VeriFast does not support unions so we replace with a struct */
struct fake_union_t
{
    QueuePointers_t xQueue;
    SemaphoreData_t xSemaphore;
};

typedef struct xLIST
{
    UBaseType_t uxNumberOfItems;
    #ifndef VERIFAST /*< do not model pxIndex and xListEnd of xLIST struct */
        struct xLIST_ITEM * pxIndex;
        MiniListItem_t xListEnd;
    #endif
} List_t;

typedef struct QueueDefinition /* The old naming convention is used to prevent breaking kernel aware debuggers. */
{
    int8_t * pcHead;           /*< Points to the beginning of the queue storage area. */
    int8_t * pcWriteTo;        /*< Points to the free next place in the storage area. */

    #ifdef VERIFAST            /*< VeriFast does not model unions */
        struct fake_union_t u;
    #else
        union
        {
            QueuePointers_t xQueue;     /*< Data required exclusively when this structure is used as a queue. */
            SemaphoreData_t xSemaphore; /*< Data required exclusively when this structure is used as a semaphore. */
        } u;
    #endif

    List_t xTasksWaitingToSend;             /*< List of tasks that are blocked waiting to post onto this queue.  Stored in priority order. */
    List_t xTasksWaitingToReceive;          /*< List of tasks that are blocked waiting to read from this queue.  Stored in priority order. */

    volatile UBaseType_t uxMessagesWaiting; /*< The number of items currently in the queue. */
    UBaseType_t uxLength;                   /*< The length of the queue defined as the number of items it will hold, not the number of bytes. */
    UBaseType_t uxItemSize;                 /*< The size of each items that the queue will hold. */

    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. */
    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. */

    #if ( ( configSUPPORT_STATIC_ALLOCATION == 1 ) && ( configSUPPORT_DYNAMIC_ALLOCATION == 1 ) )
        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. */
    #endif

    #if ( configUSE_QUEUE_SETS == 1 )
        struct QueueDefinition * pxQueueSetContainer;
    #endif

    #if ( configUSE_TRACE_FACILITY == 1 )
        UBaseType_t uxQueueNumber;
        uint8_t ucQueueType;
    #endif

    /*@struct mutex *irqMask;@*/            /*< Ghost mutex simulates the effect of irq masking */
    /*@struct mutex *schedulerSuspend;@*/   /*< Ghost mutex simulates the effect of scheduler suspension */
    /*@struct mutex *locked;@*/             /*< Ghost mutex simulates the effect of queue locking */
} xQUEUE;

typedef xQUEUE                   Queue_t;

typedef struct QueueDefinition   * QueueHandle_t;

/*@
 #define QUEUE_SHAPE(q, Storage, N, M, K)                 \
 *  malloc_block_QueueDefinition(q) &*&                  \
 *  q->pcHead |-> Storage &*&                            \
 *  q->pcWriteTo |-> ?WPtr &*&                           \
 *  q->u.xQueue.pcTail |-> ?End &*&                      \
 *  q->u.xQueue.pcReadFrom |-> ?RPtr &*&                 \
 *  q->uxItemSize |-> M &*&                              \
 *  q->uxLength |-> N &*&                                \
 *  q->uxMessagesWaiting |-> K &*&                       \
 *  q->cRxLock |-> ?rxLock &*&                           \
 *  q->cTxLock |-> ?txLock &*&                           \
 *  struct_QueuePointers_padding(&q->u.xQueue) &*&       \
 *  struct_SemaphoreData_padding(&q->u.xSemaphore) &*&   \
 *  struct_fake_union_t_padding(&q->u) &*&               \
 *  struct_xLIST_padding(&q->xTasksWaitingToSend) &*&    \
 *  struct_xLIST_padding(&q->xTasksWaitingToReceive) &*& \
 *  q->u.xSemaphore.xMutexHolder |-> _ &*&               \
 *  q->u.xSemaphore.uxRecursiveCallCount |-> _ &*&       \
 *  true
 *
 * 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) =
 *  QUEUE_SHAPE(q, Storage, N, M, K) &*&
 *  0 < N &*&
 *  0 < M &*&
 *  0 <= W &*& W < N &*&
 *  0 <= R &*& R < N &*&
 *  0 <= K &*& K <= N &*&
 *  W == (R + 1 + K) % N &*&
 *  (-1) <= rxLock &*&
 *  (-1) <= txLock &*&
 *  (is_locked ? 0 <= rxLock : (-1) == rxLock) &*&
 *  (is_locked ? 0 <= txLock : (-1) == txLock) &*&
 *  WPtr == Storage + (W*M) &*&
 *  RPtr == Storage + (R*M) &*&
 *  End == Storage + (N*M) &*&
 *  buffer(Storage, N, M, ?contents) &*&
 *  length(contents) == N &*&
 *  abs == take(K, rotate_left((R+1)%N, contents)) &*&
 *  malloc_block(Storage, N*M) &*&
 *  true
 *  ;
 * @*/

/* A buffer allows us to interpret a flat character array of `N*M` bytes as a
 * list of `N` elements where each element is `M` bytes */

/*@
 * predicate buffer(char *buffer, size_t N, size_t M; list<list<char> > elements) =
 *  N == 0
 *      ? elements == nil
 *      : chars(buffer, M, ?x) &*& buffer(buffer + M, N - 1, M, ?xs) &*& elements == cons(x, xs);
 *
 * lemma void buffer_length(char *buffer, size_t N, size_t M)
 * requires buffer(buffer, N, M, ?elements);
 * ensures buffer(buffer, N, M, elements) &*& length(elements) == N;
 * {
 *  if (N == 0) {
 *      open buffer(buffer, N, M, elements);
 *      close buffer(buffer, N, M, elements);
 *  } else {
 *      open buffer(buffer, N, M, elements);
 *      buffer_length(buffer+M, N-1, M);
 *  }
 * }
 * @*/

/*
 * There is no need in the queue proofs to preserve a relationship between `cs`
 * and `elements` (i.e., `flatten(elements) == cs`) because we only move in one
 * direction from `cs` to `elements` during queue creation when the contents is
 * fresh from `malloc` (i.e., uninitialized). If we needed to do a roundtrip from
 * elements back to cs then this would require a stronger lemma.
 */

/*@
 * lemma void buffer_from_chars(char *buffer, size_t N, size_t M)
 * requires chars(buffer, N*M, ?cs) &*& 0 <= N &*& 0 < M;
 * ensures exists<list<list<char> > >(?elements) &*& buffer(buffer, N, M, elements) &*& length(elements) == N;
 * {
 *  if (N == 0) {
 *      close exists(nil);
 *  } else {
 *      int i = 0;
 *      while (i < N)
 *      invariant 0 <= i &*& i <= N &*&
 *          chars(buffer, (N-i)*M, ?xs) &*& xs == take((N-i)*M, cs) &*&
 *          buffer(buffer + (N-i)*M, i, M, ?ys);
 *      decreases N-i;
 *      {
 *          mul_mono_l(0, N-i-1, M);
 *          chars_split(buffer, (N-i-1)*M);
 *          mul_mono_l(i, N, M);
 *          mul_mono_l(N-i, N, M);
 *          take_take((N-i-1)*M, (N-i)*M, cs);
 *          i++;
 *      }
 *      close exists(ys);
 *      buffer_length(buffer, N, M);
 *  }
 * }
 *
 * lemma void append_buffer(char *buffer, size_t N1, size_t N2, size_t M)
 * requires
 *  buffer(buffer, N1, M, ?elements1) &*&
 *  buffer(buffer + N1 * M, N2, M, ?elements2) &*&
 *  0 <= N1 &*& 0 <= N2;
 * ensures buffer(buffer, N1+N2, M, append(elements1, elements2));
 * {
 *  if (N1 == 0) {
 *      open buffer(buffer, 0, M, _);
 *  } else if (N2 == 0) {
 *      open buffer(buffer + N1 * M, 0, M, _);
 *  } else {
 *      open buffer(buffer, N1, M, elements1);
 *      append_buffer(buffer + M, N1-1, N2, M);
 *      close buffer(buffer, N1+N2, M, cons(?x, append(xs, elements2)));
 *  }
 * }
 *
 * lemma void split_element<t>(char *buffer, size_t N, size_t M, size_t i)
 * requires buffer(buffer, N, M, ?elements) &*& 0 <= i &*& i < N;
 * ensures
 *  buffer(buffer, i, M, take(i, elements)) &*&
 *  chars(buffer + i * M, M, nth(i, elements)) &*&
 *  buffer(buffer + (i + 1) * M, (N-1-i), M, drop(i+1, elements));
 * {
 *  if (i == 0) {
 *      // straightforward
 *  } else {
 *      buffer_length(buffer, N, M);
 *      int j = 0;
 *      while (j < i)
 *      invariant 0 <= j &*& j <= i &*&
 *          buffer(buffer, j, M, take(j, elements)) &*&
 *          buffer(buffer + j * M, N-j, M, drop(j, elements));
 *      decreases i-j;
 *      {
 *          drop_drop(1, j, elements);
 *          nth_drop2(elements, j);
 *          open buffer(buffer + j * M, N-j, M, drop(j, elements));
 *          assert chars(buffer + j * M, M, ?x) &*& x == nth(j, elements);
 *          close buffer(buffer + j * M, 1, M, singleton(x));
 *          append_buffer(buffer, j, 1, M);
 *          take_plus_one(j, elements);
 *          j++;
 *      }
 *      drop_drop(1, j, elements);
 *      nth_drop2(elements, i);
 *  }
 * }
 *
 * lemma void join_element(char *buffer, size_t N, size_t M, size_t i)
 * requires
 *  0 <= i &*& i < N &*&
 *  buffer(buffer, i, M, ?prefix) &*&
 *  chars(buffer + i * M, M, ?element) &*&
 *  buffer(buffer + (i + 1) * M, (N-1-i), M, ?suffix);
 * ensures buffer(buffer, N, M, append(prefix, cons(element, suffix)));
 * {
 *  if (i == 0) {
 *      open buffer(buffer, i, M, prefix);
 *      assert prefix == nil;
 *      close buffer(buffer, N, M, cons(element, suffix));
 *  } else {
 *      close buffer(buffer + i * M, N-i, M, cons(element, suffix));
 *      append_buffer(buffer, i, N-i, M);
 *  }
 * }
 *
 * predicate list(List_t *l;) =
 *  l->uxNumberOfItems |-> _;
 *
 * predicate queuelists(QueueHandle_t q;) =
 *  list(&q->xTasksWaitingToSend) &*&
 *  list(&q->xTasksWaitingToReceive);
 * @*/

/* Because prvCopyDataFromQueue does *not* decrement uxMessagesWaiting (K) the
 * queue predicate above does not hold as a postcondition. If the caller
 * subsequently decrements K then the queue predicate can be reinstated. */

/*@
 * 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) =
 *  QUEUE_SHAPE(q, Storage, N, M, K) &*&
 *  0 < N &*&
 *  0 < M &*&
 *  0 <= W &*& W < N &*&
 *  0 <= R &*& R < N &*&
 *  0 <= K &*& K <= N &*&
 *  W == (R + K) % N &*& //< Differs from queue predicate
 *  (-1) <= rxLock &*&
 *  (-1) <= txLock &*&
 *  (is_locked ? 0 <= rxLock : (-1) == rxLock) &*&
 *  (is_locked ? 0 <= txLock : (-1) == txLock) &*&
 *  WPtr == Storage + (W*M) &*&
 *  RPtr == Storage + (R*M) &*&
 *  End == Storage + (N*M) &*&
 *  buffer(Storage, N, M, ?contents) &*&
 *  length(contents) == N &*&
 *  abs == take(K, rotate_left(R, contents)) &*& //< Differs from queue predicate
 *  malloc_block(Storage, N*M) &*&
 *  true
 *  ;
 * @*/

/* Can't be called `mutex` as this clashes with VeriFast's predicate */

/*@
 * predicate freertos_mutex(QueueHandle_t q, int8_t *Storage, size_t N, size_t K;) =
 *  QUEUE_SHAPE(q, Storage, N, 0, K) &*&
 *  queuelists(q) &*&
 *  0 < N &*&
 *  0 <= K &*& K <= N &*&
 *  (-1) <= rxLock &*&
 *  (-1) <= txLock &*&
 *  WPtr == Storage &*&
 *  RPtr == Storage &*&
 *  End == Storage &*&
 *  malloc_block(Storage, 0) &*&
 *  chars(Storage, 0, _) &*&
 *  true
 *  ;
 * @*/

/* A queuehandle can be shared between tasks and ISRs. Acquiring the ghost
 * `irqMask` gives access to the core queue resources. The permissions granted
 * after masking interrupts depends on the caller:
 * - A task has access to the queue and the queuelists
 * - An ISR has access to the queue and, if the queue is unlocked, the queuelists */

/*@
 * predicate queuehandle(QueueHandle_t q, size_t N, size_t M, bool is_isr;) =
 *  q->irqMask |-> ?m &*& mutex(m, irqs_masked_invariant(q, N, M, is_isr));
 *
 * predicate_ctor irqs_masked_invariant(QueueHandle_t queue, size_t N, size_t M, bool is_isr)() =
 *  queue(queue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
 *  (is_isr && is_locked ? true : queuelists(queue));
 * @*/

/* A queuesuspend can be shared between tasks. Acquiring the ghost `schedulerSuspend` gives access to the `locked` mutex. */

/*@
 * predicate_ctor scheduler_suspended_invariant(QueueHandle_t queue)() =
 *  queue->locked |-> ?m &*&
 *  mutex(m, queue_locked_invariant(queue));
 *
 * predicate queuesuspend(QueueHandle_t q;) =
 *  q->schedulerSuspend |-> ?m &*&
 *  mutex(m, scheduler_suspended_invariant(q));
 * @*/

/* A queuelock is exclusively acquired by a task. Acquiring the ghost `queuelock` gives access to the queue list resources. */

/*@
 * predicate queuelock(QueueHandle_t q;) =
 *  q->locked |-> ?m &*&
 *  mutex(m, queue_locked_invariant(q));
 *
 * predicate_ctor queue_locked_invariant(QueueHandle_t queue)() =
 *  queuelists(queue);
 * @*/

BaseType_t vListInitialise( List_t * list );
/*@requires list(list);@*/
/*@ensures list(list);@*/

BaseType_t listLIST_IS_EMPTY( List_t * list );
/*@requires list->uxNumberOfItems |-> ?len;@*/
/*@ensures list->uxNumberOfItems |-> len &*& result == (len == 0 ? pdTRUE : pdFALSE);@*/

typedef struct xTIME_OUT
{
    BaseType_t xOverflowCount;
    TickType_t xTimeOnEntering;
} TimeOut_t;

/*@
 * predicate xTIME_OUT(struct xTIME_OUT *to;) =
 *  to->xOverflowCount |-> _ &*&
 *  to->xTimeOnEntering |-> _ &*&
 *  struct_xTIME_OUT_padding(to);
 * @*/

void vTaskInternalSetTimeOutState( TimeOut_t * x );
/*@requires xTIME_OUT(x);@*/
/*@ensures xTIME_OUT(x);@*/

BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
                                 TickType_t * const pxTicksToWait );
/*@requires xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/
/*@ensures xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/

BaseType_t xTaskRemoveFromEventList( List_t * list );
/*@requires list(list);@*/
/*@ensures list(list);@*/

void vTaskPlaceOnEventList( List_t * const pxEventList,
                            const TickType_t xTicksToWait );
/*@requires list(pxEventList);@*/
/*@ensures list(pxEventList);@*/

void vTaskMissedYield();
/*@requires true;@*/
/*@ensures true;@*/

void vTaskSuspendAll();

/*@requires exists<QueueHandle_t>(?xQueue) &*&
 *  [1/2]xQueue->schedulerSuspend |-> ?m &*&
 *  [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/

/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*&
 *  mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*&
 *  xQueue->locked |-> ?m2 &*&
 *  mutex(m2, queue_locked_invariant(xQueue));@*/

BaseType_t xTaskResumeAll( void );

/*@requires exists<QueueHandle_t>(?xQueue) &*&
 *  [1/2]xQueue->schedulerSuspend |-> ?m &*&
 *  mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*&
 *  xQueue->locked |-> ?m2 &*&
 *  mutex(m2, queue_locked_invariant(xQueue));@*/

/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*&
 *  [1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/

void prvLockQueue( QueueHandle_t xQueue );

/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
 *  [1/2]queuelock(xQueue); @*/

/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
 *  [1/2]xQueue->locked |-> ?m &*&
 *  mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*&
 *  queue_locked_invariant(xQueue)();@*/

void prvUnlockQueue( QueueHandle_t xQueue );

/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
 *  [1/2]xQueue->locked |-> ?m &*&
 *  mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*&
 *  queue_locked_invariant(xQueue)();@*/

/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
 *  [1/2]queuelock(xQueue);@*/

void setInterruptMask( QueueHandle_t xQueue )
/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/

/*@ensures [1/2]xQueue->irqMask |-> ?m &*&
 *  mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*&
 *  queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
 *  queuelists(xQueue);@*/
{
    /*@open queuehandle(xQueue, N, M, is_isr);@*/
    mutex_acquire( xQueue->irqMask );
    /*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/
}

void clearInterruptMask( QueueHandle_t xQueue )

/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
 *  [1/2]xQueue->irqMask |-> ?m &*&
 *  mutex_held(m, irqs_masked_invariant(xQueue, N, M, false), currentThread, 1/2) &*&
 *  queuelists(xQueue);@*/
/*@ensures [1/2]queuehandle(xQueue, N, M, false);@*/
{
    /*@close irqs_masked_invariant(xQueue, N, M, false)();@*/
    mutex_release( xQueue->irqMask );
    /*@close [1/2]queuehandle(xQueue, N, M, false);@*/
}

#define taskENTER_CRITICAL()    setInterruptMask( xQueue )
#define taskEXIT_CRITICAL()     clearInterruptMask( xQueue )
#define portYIELD_WITHIN_API()
#define queueYIELD_IF_USING_PREEMPTION()

UBaseType_t setInterruptMaskFromISR( QueueHandle_t xQueue )
/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true;@*/

/*@ensures [1/2]xQueue->irqMask |-> ?m &*&
 *  mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*&
 *  queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
 *  (is_locked ? true : queuelists(xQueue));@*/
{
    /*@open queuehandle(xQueue, N, M, is_isr);@*/
    mutex_acquire( xQueue->irqMask );
    /*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/
    return 0;
}

void clearInterruptMaskFromISR( QueueHandle_t xQueue,
                                UBaseType_t uxSavedInterruptStatus )

/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
 *  [1/2]xQueue->irqMask |-> ?m &*&
 *  mutex_held(m, irqs_masked_invariant(xQueue, N, M, true), currentThread, 1/2) &*&
 *  (is_locked ? true : queuelists(xQueue));@*/
/*@ensures [1/2]queuehandle(xQueue, N, M, true);@*/
{
    /*@close irqs_masked_invariant(xQueue, N, M, true)();@*/
    mutex_release( xQueue->irqMask );
    /*@close [1/2]queuehandle(xQueue, N, M, true);@*/
}

#define portSET_INTERRUPT_MASK_FROM_ISR()                              setInterruptMaskFromISR( xQueue )
#define portCLEAR_INTERRUPT_MASK_FROM_ISR( uxSavedInterruptStatus )    clearInterruptMaskFromISR( xQueue, uxSavedInterruptStatus )

#endif /* QUEUE_H */