From 0390b0fc9b62181428a66ccefd854ec82e992848 Mon Sep 17 00:00:00 2001 From: Mark Tuttle Date: Mon, 13 Sep 2021 21:23:35 -0400 Subject: Add CBMC viewer configuration files (#683) * Revert cbmc-viewer flags * Add cbmc-viewer configuration files * Repair CBMC patch to prvCopyDataToQueue Authored-by: Mark R. Tuttle --- ...005-remove-static-from-prvCopyDataToQueue.patch | 23 +++++++++--------- FreeRTOS/Test/CBMC/proofs/Makefile.template | 6 ++--- .../QueueCreateCountingSemaphore/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Queue/QueueCreateMutex/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueCreateMutexStatic/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueGenericCreate/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../QueueGenericCreateStatic/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueGenericReset/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Queue/QueueGenericSend/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueGenericSendFromISR/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueGetMutexHolder/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../QueueGetMutexHolderFromISR/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Queue/QueueGiveFromISR/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueGiveMutexRecursive/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueMessagesWaiting/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../CBMC/proofs/Queue/QueuePeek/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Queue/QueueReceive/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueReceiveFromISR/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueSemaphoreTake/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueSpacesAvailable/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/QueueTakeMutexRecursive/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Queue/prvCopyDataToQueue/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../prvNotifyQueueSetContainer/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Queue/prvUnlockQueue/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Task/TaskCheckForTimeOut/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../CBMC/proofs/Task/TaskCreate/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../CBMC/proofs/Task/TaskDelay/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../CBMC/proofs/Task/TaskDelete/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Task/TaskGetCurrentTaskHandle/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Task/TaskGetSchedulerState/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Task/TaskGetTaskNumber/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Task/TaskGetTickCount/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Task/TaskIncrementTick/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Task/TaskPrioritySet/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Task/TaskResumeAll/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Task/TaskSetTimeOutState/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../Task/TaskStartScheduler/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Task/TaskSuspendAll/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../proofs/Task/TaskSwitchContext/cbmc-viewer.json | 28 ++++++++++++++++++++++ .../CBMC/proofs/make_configuration_directories.py | 5 ++++ 41 files changed, 1084 insertions(+), 14 deletions(-) create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskCheckForTimeOut/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskDelete/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskGetCurrentTaskHandle/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskGetTaskNumber/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskGetTickCount/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskIncrementTick/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskPrioritySet/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskSetTimeOutState/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskStartScheduler/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskSuspendAll/cbmc-viewer.json create mode 100644 FreeRTOS/Test/CBMC/proofs/Task/TaskSwitchContext/cbmc-viewer.json diff --git a/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch b/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch index b72c91a0b..6414bdf2d 100644 --- a/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch +++ b/FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch @@ -1,8 +1,8 @@ diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c -index d2e27e55a..4b05e3c01 100644 +index 08d3799da..6681a34f1 100644 --- a/FreeRTOS/Source/queue.c +++ b/FreeRTOS/Source/queue.c -@@ -191,14 +191,14 @@ static BaseType_t prvIsQueueFull( const Queue_t * pxQueue ) PRIVILEGED_FUNCTION; +@@ -193,7 +193,7 @@ static BaseType_t prvIsQueueFull( const Queue_t * pxQueue ) PRIVILEGED_FUNCTION; * Copies an item into the queue, either at the front of the queue or the * back of the queue. */ @@ -10,12 +10,13 @@ index d2e27e55a..4b05e3c01 100644 +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void * pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION; - - /* - * Copies an item out of a queue. - */ --static void prvCopyDataFromQueue( Queue_t * const pxQueue, -+void prvCopyDataFromQueue( Queue_t * const pxQueue, - void * const pvBuffer ) PRIVILEGED_FUNCTION; - - #if ( configUSE_QUEUE_SETS == 1 ) + +@@ -2157,7 +2157,7 @@ void vQueueDelete( QueueHandle_t xQueue ) + #endif /* configUSE_MUTEXES */ + /*-----------------------------------------------------------*/ + +-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, ++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, + const void * pvItemToQueue, + const BaseType_t xPosition ) + { diff --git a/FreeRTOS/Test/CBMC/proofs/Makefile.template b/FreeRTOS/Test/CBMC/proofs/Makefile.template index 01d518ed5..c7692c9b4 100644 --- a/FreeRTOS/Test/CBMC/proofs/Makefile.template +++ b/FreeRTOS/Test/CBMC/proofs/Makefile.template @@ -138,11 +138,11 @@ report: cbmc.txt property.xml coverage.xml $(VIEWER) \ --goto $(ENTRY).goto \ --srcdir $(FREERTOS) \ - --reportdir html \ - --exclude "(.@FORWARD_SLASH@Demo)" \ + --htmldir html \ + --srcexclude "(.@FORWARD_SLASH@Demo)" \ --result cbmc.txt \ --property property.xml \ - --coverage coverage.xml + --block coverage.xml # This rule depends only on cbmc.txt and has no dependents, so it will # not block the report from being generated if it fails. This rule is diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/cbmc-viewer.json new file mode 100644 index 000000000..9e1bf4cc5 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueCreateCountingSemaphore", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/cbmc-viewer.json new file mode 100644 index 000000000..099141fe8 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueCreateCountingSemaphoreStatic", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/cbmc-viewer.json new file mode 100644 index 000000000..d9ea71f0e --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueCreateMutex", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/cbmc-viewer.json new file mode 100644 index 000000000..c68b26bcc --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueCreateMutexStatic", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/cbmc-viewer.json new file mode 100644 index 000000000..be05bc102 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueGenericCreate", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/cbmc-viewer.json new file mode 100644 index 000000000..cd9e3e614 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueGenericCreateStatic", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/cbmc-viewer.json new file mode 100644 index 000000000..10861aa9c --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueGenericReset", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/cbmc-viewer.json new file mode 100644 index 000000000..4c8a74fcb --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueGenericSend", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/cbmc-viewer.json new file mode 100644 index 000000000..b736b92d5 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueGenericSendFromISR", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/cbmc-viewer.json new file mode 100644 index 000000000..9e439d3bf --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueGetMutexHolder", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/cbmc-viewer.json new file mode 100644 index 000000000..6d2a3e5bf --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueGetMutexHolderFromISR", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/cbmc-viewer.json new file mode 100644 index 000000000..0a36bd254 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueGiveFromISR", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/cbmc-viewer.json new file mode 100644 index 000000000..4497bf511 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueGiveMutexRecursive", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/cbmc-viewer.json new file mode 100644 index 000000000..37d51de5f --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueMessagesWaiting", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/cbmc-viewer.json new file mode 100644 index 000000000..123df55ac --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueuePeek", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/cbmc-viewer.json new file mode 100644 index 000000000..34442ecec --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueReceive", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/cbmc-viewer.json new file mode 100644 index 000000000..aef886a0e --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueReceiveFromISR", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/cbmc-viewer.json new file mode 100644 index 000000000..db6472fe0 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueSemaphoreTake", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/cbmc-viewer.json new file mode 100644 index 000000000..27d9e7f9a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueSpacesAvailable", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/cbmc-viewer.json new file mode 100644 index 000000000..c4adb5754 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "QueueTakeMutexRecursive", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/cbmc-viewer.json new file mode 100644 index 000000000..edd82f7dd --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "prvCopyDataToQueue", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/cbmc-viewer.json new file mode 100644 index 000000000..308955d58 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "prvNotifyQueueSetContainer", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/cbmc-viewer.json new file mode 100644 index 000000000..87f943515 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "prvUnlockQueue", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskCheckForTimeOut/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskCheckForTimeOut/cbmc-viewer.json new file mode 100644 index 000000000..ca8ab6954 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskCheckForTimeOut/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskCheckForTimeOut", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/cbmc-viewer.json new file mode 100644 index 000000000..06b4bc2fd --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskCreate", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/cbmc-viewer.json new file mode 100644 index 000000000..e0a7a2bb0 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskDelay", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskDelete/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskDelete/cbmc-viewer.json new file mode 100644 index 000000000..69a5ae4a0 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskDelete/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskDelete", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskGetCurrentTaskHandle/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskGetCurrentTaskHandle/cbmc-viewer.json new file mode 100644 index 000000000..3d51dfe28 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskGetCurrentTaskHandle/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskGetCurrentTaskHandle", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/cbmc-viewer.json new file mode 100644 index 000000000..511679596 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskGetSchedulerState", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskGetTaskNumber/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskGetTaskNumber/cbmc-viewer.json new file mode 100644 index 000000000..e1f087307 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskGetTaskNumber/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskGetTaskNumber", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskGetTickCount/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskGetTickCount/cbmc-viewer.json new file mode 100644 index 000000000..46eb86ccb --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskGetTickCount/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskGetTickCount", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskIncrementTick/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskIncrementTick/cbmc-viewer.json new file mode 100644 index 000000000..0be12e650 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskIncrementTick/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskIncrementTick", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskPrioritySet/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskPrioritySet/cbmc-viewer.json new file mode 100644 index 000000000..adb3e1626 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskPrioritySet/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskPrioritySet", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/cbmc-viewer.json new file mode 100644 index 000000000..0b5453c11 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskResumeAll", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskSetTimeOutState/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskSetTimeOutState/cbmc-viewer.json new file mode 100644 index 000000000..49c70c8c3 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskSetTimeOutState/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskSetTimeOutState", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskStartScheduler/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskStartScheduler/cbmc-viewer.json new file mode 100644 index 000000000..4f42c1e10 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskStartScheduler/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskStartScheduler", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskSuspendAll/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskSuspendAll/cbmc-viewer.json new file mode 100644 index 000000000..5e5249dd3 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskSuspendAll/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskSuspendAll", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/Task/TaskSwitchContext/cbmc-viewer.json b/FreeRTOS/Test/CBMC/proofs/Task/TaskSwitchContext/cbmc-viewer.json new file mode 100644 index 000000000..70bf3bd2c --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/Task/TaskSwitchContext/cbmc-viewer.json @@ -0,0 +1,28 @@ +{ "expected-missing-functions": + [ + "vApplicationTickHook", + + "pxPortInitialiseStack", + "vPortCloseRunningThread", + "vPortDeleteThread", + "vPortEnterCritical", + "vPortExitCritical", + "vPortGenerateSimulatedInterrupt", + "xPortStartScheduler", + + "pvTaskIncrementMutexHeldCount", + "uxTaskGetTaskNumber", + "vTaskInternalSetTimeOutState", + "vTaskMissedYield", + "vTaskPlaceOnEventList", + "vTaskPriorityDisinheritAfterTimeout", + "vTaskSuspendAll", + "xTaskGetCurrentTaskHandle", + "xTaskPriorityDisinherit", + "xTaskPriorityInherit", + "xTaskRemoveFromEventList", + "xTaskResumeAll" + ], + "proof-name": "TaskSwitchContext", + "proof-root": "Test/CBMC/proofs" +} diff --git a/FreeRTOS/Test/CBMC/proofs/make_configuration_directories.py b/FreeRTOS/Test/CBMC/proofs/make_configuration_directories.py index 9e006e9ed..8ac0ed316 100755 --- a/FreeRTOS/Test/CBMC/proofs/make_configuration_directories.py +++ b/FreeRTOS/Test/CBMC/proofs/make_configuration_directories.py @@ -129,10 +129,15 @@ def process(folder, files): pathlib.Path(new_config_folder).mkdir(exist_ok=True, parents=True) harness_copied = False for file in files: + # Copy cbmc proof harness into configuration directory if file.endswith("harness.c"): shutil.copy(os.path.join(folder, file), os.path.join(new_config_folder, file)) harness_copied = True + # Copy cbmc-viewer configuration file into configuration directory + if file == "cbmc-viewer.json": + shutil.copy(os.path.join(folder, file), + os.path.join(new_config_folder, file)) if not harness_copied: LOGGER.error("Could not find a harness in folder %s.", folder) -- cgit v1.2.1