FreeRTOS-Kernel/FreeRTOS/Test/CBMC/proofs/Queue
Dan Good b6624fa44d
Remove or rework assumptions in queue proofs (#603)
This commit is paired with another to queue.c in the kernel.  To
accomodate changes in newer versions of CBMC, the
--pointer-overflow-check is removed.
2021-06-04 15:42:14 -04:00
..
prvCopyDataToQueue Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
prvNotifyQueueSetContainer Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
prvUnlockQueue Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueCreateCountingSemaphore Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueCreateCountingSemaphoreStatic Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueCreateMutex Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueCreateMutexStatic Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueGenericCreate Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueGenericCreateStatic Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueGenericReset Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueGenericSend Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueGenericSendFromISR Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueGetMutexHolder Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueGetMutexHolderFromISR Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueGiveFromISR Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueGiveMutexRecursive Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueMessagesWaiting Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueuePeek Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueReceive Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueReceiveFromISR Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueSemaphoreTake Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueSpacesAvailable Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00
QueueTakeMutexRecursive Remove or rework assumptions in queue proofs (#603) 2021-06-04 15:42:14 -04:00