len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-18 18:57:46 -04:00
Code Issues Projects Releases Packages Wiki Activity

Add CBMC viewer configuration files (#683)

Browse source 
* Revert cbmc-viewer flags

* Add cbmc-viewer configuration files

* Repair CBMC patch to prvCopyDataToQueue

Authored-by: Mark R. Tuttle <mrtuttle@amazon.com>
This commit is contained in:
Mark Tuttle 2021-09-13 21:23:35 -04:00 • committed by GitHub
parent fe6e501488
commit 0390b0fc9b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
41 changed files with 1084 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

23
FreeRTOS/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch
View file

@ -1,8 +1,8 @@
diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c 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 --- a/FreeRTOS/Source/queue.c
+++ b/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 * Copies an item into the queue, either at the front of the queue or the
* back of the queue. * back of the queue.
*/ */
@ -10,12 +10,13 @@ index d2e27e55a..4b05e3c01 100644
+BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
const void * pvItemToQueue, const void * pvItemToQueue,
const BaseType_t xPosition ) PRIVILEGED_FUNCTION; const BaseType_t xPosition ) PRIVILEGED_FUNCTION;
/* @@ -2157,7 +2157,7 @@ void vQueueDelete( QueueHandle_t xQueue )
* Copies an item out of a queue. #endif /* configUSE_MUTEXES */
*/ /*-----------------------------------------------------------*/
-static void prvCopyDataFromQueue( Queue_t * const pxQueue,
+void prvCopyDataFromQueue( Queue_t * const pxQueue, -static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
void * const pvBuffer ) PRIVILEGED_FUNCTION; +BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
const void * pvItemToQueue,
#if ( configUSE_QUEUE_SETS == 1 ) const BaseType_t xPosition )
{

6
FreeRTOS/Test/CBMC/proofs/Makefile.template
View file

@ -138,11 +138,11 @@ report: cbmc.txt property.xml coverage.xml
$(VIEWER) \ $(VIEWER) \
--goto $(ENTRY).goto \ --goto $(ENTRY).goto \
--srcdir $(FREERTOS) \ --srcdir $(FREERTOS) \
--reportdir html \ --htmldir html \
--exclude "(.@FORWARD_SLASH@Demo)" \ --srcexclude "(.@FORWARD_SLASH@Demo)" \
--result cbmc.txt \ --result cbmc.txt \
--property property.xml \ --property property.xml \
--coverage coverage.xml --block coverage.xml
# This rule depends only on cbmc.txt and has no dependents, so it will # 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 # not block the report from being generated if it fails. This rule is

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskCheckForTimeOut/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskCreate/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskDelay/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskDelete/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskGetCurrentTaskHandle/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskGetSchedulerState/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskGetTaskNumber/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskGetTickCount/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskIncrementTick/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskPrioritySet/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskResumeAll/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskSetTimeOutState/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskStartScheduler/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskSuspendAll/cbmc-viewer.json Normal file
View file

@ -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"
}

28
FreeRTOS/Test/CBMC/proofs/Task/TaskSwitchContext/cbmc-viewer.json Normal file
View file

@ -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"
}

5
FreeRTOS/Test/CBMC/proofs/make_configuration_directories.py
View file

@ -129,10 +129,15 @@ def process(folder, files):
pathlib.Path(new_config_folder).mkdir(exist_ok=True, parents=True) pathlib.Path(new_config_folder).mkdir(exist_ok=True, parents=True)
harness_copied = False harness_copied = False
for file in files: for file in files:
# Copy cbmc proof harness into configuration directory
if file.endswith("harness.c"): if file.endswith("harness.c"):
shutil.copy(os.path.join(folder, file), shutil.copy(os.path.join(folder, file),
os.path.join(new_config_folder, file)) os.path.join(new_config_folder, file))
harness_copied = True 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: if not harness_copied:
LOGGER.error("Could not find a harness in folder %s.", folder) LOGGER.error("Could not find a harness in folder %s.", folder)