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 <mrtuttle@amazon.com>

41 files changed, 1084 insertions, 14 deletions

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)