diff --git a/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch b/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch index 58fcae48dd..3eadf82d98 100644 --- a/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch +++ b/FreeRTOS/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch @@ -44,15 +44,6 @@ diff --git a/FreeRTOS/Source/tasks.c b/FreeRTOS/Source/tasks.c index c7be57cb2..9f76465d5 100644 --- a/FreeRTOS/Source/tasks.c +++ b/FreeRTOS/Source/tasks.c -@@ -296,7 +296,7 @@ typedef struct tskTaskControlBlock /* The old naming convention is used to - - #if ( configUSE_NEWLIB_REENTRANT == 1 ) - /* Allocate a Newlib reent structure that is specific to this task. -- * Note Newlib support has been included by popular demand, but is not -+ Note Newlib support has been included by popular demand, but is not - * used by the FreeRTOS maintainers themselves. FreeRTOS is not - * responsible for resulting newlib operation. User must be familiar with - * newlib and must provide system-wide implementations of the necessary @@ -343,8 +343,8 @@ PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL; PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ]; /*< Prioritised ready tasks. */ PRIVILEGED_DATA static List_t xDelayedTaskList1; /*< Delayed tasks. */ diff --git a/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch b/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch deleted file mode 100644 index 5665447062..0000000000 --- a/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch +++ /dev/null @@ -1,13 +0,0 @@ -diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c -index b01dfd11f..b219b599a 100644 ---- a/FreeRTOS/Source/queue.c -+++ b/FreeRTOS/Source/queue.c -@@ -395,7 +395,7 @@ BaseType_t xQueueGenericReset( QueueHandle_t xQueue, - xQueueSizeInBytes = ( size_t ) ( uxQueueLength * uxItemSize ); /*lint !e961 MISRA exception as the casts are only redundant for some ports. */ - - /* Check for multiplication overflow. */ -- configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); -+ /* configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); */ - - /* Check for addition overflow. */ - configASSERT( ( sizeof( Queue_t ) + xQueueSizeInBytes ) > xQueueSizeInBytes ); diff --git a/FreeRTOS/Test/CBMC/proofs/Makefile.template b/FreeRTOS/Test/CBMC/proofs/Makefile.template index fa5558f7fc..01d518ed5b 100644 --- a/FreeRTOS/Test/CBMC/proofs/Makefile.template +++ b/FreeRTOS/Test/CBMC/proofs/Makefile.template @@ -138,12 +138,11 @@ report: cbmc.txt property.xml coverage.xml $(VIEWER) \ --goto $(ENTRY).goto \ --srcdir $(FREERTOS) \ - --blddir $(FREERTOS) \ - --htmldir html \ - --srcexclude "(.@FORWARD_SLASH@Demo)" \ + --reportdir html \ + --exclude "(.@FORWARD_SLASH@Demo)" \ --result cbmc.txt \ --property property.xml \ - --block coverage.xml + --coverage 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/MakefileCommon.json b/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json index c7495bf29b..3b6c4bb2e7 100644 --- a/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json +++ b/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json @@ -3,18 +3,20 @@ "PROOFS": [ "." ], "DEF ": [ - "_DEBUG", - "__free_rtos__", - "_CONSOLE", - "_WIN32_WINNT=0x0500", - "WINVER=0x400", - "_CRT_SECURE_NO_WARNINGS", - "__PRETTY_FUNCTION__=__FUNCTION__", + "_DEBUG", + "__free_rtos__", + "_CONSOLE", + "_WIN32_WINNT=0x0500", + "WINVER=0x400", + "_CRT_SECURE_NO_WARNINGS", + "__PRETTY_FUNCTION__=__FUNCTION__", "CBMC", - "'configASSERT(X)=__CPROVER_assert(X,\"Assertion Error\")'", - "'configPRECONDITION(X)=__CPROVER_assume(X)'", - "'_static='", - "'_volatile='" + "'configASSERT(X)='", + "'configPRECONDITION(X)=__CPROVER_assume(X)'", + "'_static='", + "'_volatile='", + "QUEUE_LENGTH=15", + "QUEUE_ITEM_SIZE=990" ], "INC ": [ @@ -31,10 +33,10 @@ ], "CBMCFLAGS ": [ - "--object-bits 7", - "--32", - "--bounds-check", - "--pointer-check" + "--object-bits 7", + "--32", + "--bounds-check", + "--pointer-check" ], "FORWARD_SLASH": ["/"], diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/Makefile.json index 4e26b37f88..eec7cba78c 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/QueueCreateCountingSemaphore_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/QueueCreateCountingSemaphore_harness.c index f079ecbdfb..d0354bc7c0 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/QueueCreateCountingSemaphore_harness.c +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/QueueCreateCountingSemaphore_harness.c @@ -32,13 +32,10 @@ #include "cbmc.h" -void harness(){ +void harness() +{ UBaseType_t uxMaxCount; UBaseType_t uxInitialCount; - __CPROVER_assume(uxMaxCount != 0); - __CPROVER_assume(uxInitialCount <= uxMaxCount); - xQueueCreateCountingSemaphore( uxMaxCount, uxInitialCount ); } - diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/Makefile.json index d9a9a8ec87..10fa565967 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/QueueCreateCountingSemaphoreStatic_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/QueueCreateCountingSemaphoreStatic_harness.c index cb09c72b93..3b2a1a5578 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/QueueCreateCountingSemaphoreStatic_harness.c +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/QueueCreateCountingSemaphoreStatic_harness.c @@ -31,15 +31,12 @@ #include "cbmc.h" -void harness(){ +void harness() +{ UBaseType_t uxMaxCount; UBaseType_t uxInitialCount; + StaticQueue_t * pxStaticQueue = ( StaticQueue_t * ) pvPortMalloc( sizeof( StaticQueue_t ) ); - //xStaticQueue is required to be not null - StaticQueue_t xStaticQueue; - //Checked invariant - __CPROVER_assume(uxMaxCount != 0); - __CPROVER_assume(uxInitialCount <= uxMaxCount); - xQueueCreateCountingSemaphoreStatic( uxMaxCount, uxInitialCount, &xStaticQueue ); + xQueueCreateCountingSemaphoreStatic( uxMaxCount, uxInitialCount, pxStaticQueue ); } diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/Makefile.json index 6409cd15a2..51f3be6259 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/Makefile.json index 7de7e05dc6..3af3c5652d 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/QueueCreateMutexStatic_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/QueueCreateMutexStatic_harness.c index 36848b6bfc..45f1c379e8 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/QueueCreateMutexStatic_harness.c +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/QueueCreateMutexStatic_harness.c @@ -31,11 +31,10 @@ #include "cbmc.h" -void harness(){ +void harness() +{ uint8_t ucQueueType; + StaticQueue_t * pxStaticQueue = ( StaticQueue_t * ) pvPortMalloc( sizeof( StaticQueue_t ) ); - //The mutex storage is assumed to be not null. - StaticQueue_t xStaticQueue; - - xQueueCreateMutexStatic( ucQueueType, &xStaticQueue ); + xQueueCreateMutexStatic( ucQueueType, pxStaticQueue ); } diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/Configurations.json index d7c4e86ed7..f404c8f530 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/Configurations.json @@ -38,7 +38,6 @@ [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/QueueGenericCreate_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/QueueGenericCreate_harness.c index 4fa87f8d22..40c3e7a02a 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/QueueGenericCreate_harness.c +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/QueueGenericCreate_harness.c @@ -32,19 +32,14 @@ #include "cbmc.h" -void harness(){ - UBaseType_t uxQueueLength; - UBaseType_t uxItemSize; - uint8_t ucQueueType; +void harness() +{ + UBaseType_t uxQueueLength; + UBaseType_t uxItemSize; + uint8_t ucQueueType; - size_t uxQueueStorageSize; - __CPROVER_assume(uxQueueStorageSize < (UINT32_MAX>>8)); + /* Allow CBMC to run in a reasonable amount of time. */ + __CPROVER_assume( ( uxQueueLength == QUEUE_LENGTH ) || ( uxItemSize == QUEUE_ITEM_SIZE ) ); - // QueueGenericCreate does not check for multiplication overflow - __CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength); - - // QueueGenericCreate asserts positive queue length - __CPROVER_assume(uxQueueLength > ( UBaseType_t ) 0); - - xQueueGenericCreate( uxQueueLength, uxItemSize, ucQueueType ); + xQueueGenericCreate( uxQueueLength, uxItemSize, ucQueueType ); } diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/Configurations.json index 0acbc976e4..0e02630bdd 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/Configurations.json @@ -37,7 +37,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ @@ -48,8 +47,8 @@ "DEF": [ { "QeueuGenericCreateStatic_DynamicAllocation": [ - "CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}", - "CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}", + "CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}", + "CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}", "configUSE_TRACE_FACILITY=0", "configGENERATE_RUN_TIME_STATS=0", "configSUPPORT_STATIC_ALLOCATION=1", @@ -58,8 +57,8 @@ }, { "QeueuGenericCreateStatic_NoDynamicAllocation": [ - "CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}", - "CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}", + "CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}", + "CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}", "configUSE_TRACE_FACILITY=0", "configGENERATE_RUN_TIME_STATS=0", "configSUPPORT_STATIC_ALLOCATION=1", diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/QueueGenericCreateStatic_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/QueueGenericCreateStatic_harness.c index 553661cb2b..fa7960e9dc 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/QueueGenericCreateStatic_harness.c +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/QueueGenericCreateStatic_harness.c @@ -31,32 +31,22 @@ #include "queue_datastructure.h" #include "cbmc.h" -void harness(){ +void harness() +{ UBaseType_t uxQueueLength; UBaseType_t uxItemSize; - - size_t uxQueueStorageSize; - uint8_t *pucQueueStorage = (uint8_t *) pvPortMalloc(uxQueueStorageSize); - - StaticQueue_t *pxStaticQueue = - (StaticQueue_t *) pvPortMalloc(sizeof(StaticQueue_t)); - uint8_t ucQueueType; + size_t storageSize; - __CPROVER_assume(uxQueueStorageSize < (UINT32_MAX>>8)); + /* Allow CBMC to run in a reasonable amount of time. */ + __CPROVER_assume( ( uxQueueLength == QUEUE_LENGTH ) || ( uxItemSize == QUEUE_ITEM_SIZE ) ); - // QueueGenericReset does not check for multiplication overflow - __CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength); + /* Prevent overflow in this harness. */ + __CPROVER_assume( ( uxQueueLength > 0 ) && ( ( storageSize / uxQueueLength ) == uxItemSize ) ); - // QueueGenericCreateStatic asserts positive queue length - __CPROVER_assume(uxQueueLength > ( UBaseType_t ) 0); + uint8_t * pucQueueStorage = ( uint8_t * ) pvPortMalloc( storageSize ); - // QueueGenericCreateStatic asserts the following equivalence - __CPROVER_assume( ( pucQueueStorage && uxItemSize ) || - ( !pucQueueStorage && !uxItemSize ) ); - - // QueueGenericCreateStatic asserts nonnull pointer - __CPROVER_assume(pxStaticQueue); + StaticQueue_t * pxStaticQueue = ( StaticQueue_t * ) pvPortMalloc( sizeof( StaticQueue_t ) ); xQueueGenericCreateStatic( uxQueueLength, uxItemSize, pucQueueStorage, pxStaticQueue, ucQueueType ); } diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/Makefile.json index 1759310d85..d523842a20 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/QueueGenericReset_harness.c b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/QueueGenericReset_harness.c index fbe4883a08..d174a773e3 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/QueueGenericReset_harness.c +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/QueueGenericReset_harness.c @@ -34,12 +34,11 @@ struct QueueDefinition; -void harness() { - BaseType_t xNewQueue; +void harness() +{ + BaseType_t xNewQueue; - QueueHandle_t xQueue = xUnconstrainedQueue(); - if(xQueue != NULL) - { - xQueueGenericReset(xQueue, xNewQueue); - } + QueueHandle_t xQueue = xUnconstrainedQueue(); + + xQueueGenericReset( xQueue, xNewQueue ); } diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/Configurations.json index 64e3e67896..e4435b1c1b 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/Configurations.json @@ -33,7 +33,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check", "--unwindset xQueueGenericSend.0:{QUEUE_SEND_BOUND},prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}", "--nondet-static" diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/Configurations.json index 92892ca85b..ab240fc9a1 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/Configurations.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check", "--nondet-static" ], diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/Makefile.json index ecc2b62308..73f8bdedd4 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/Makefile.json index 647a0d03fa..6005db3596 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/Configurations.json index ff71fd6429..74e6418d41 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/Configurations.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check", "--nondet-static" ], diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/Makefile.json index 8d1720fcd7..bccd5db02b 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/Makefile.json index 6c8806b2cf..8e7bac96f1 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/Makefile.json index 797d788a18..c85000cb42 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/Makefile.json @@ -33,7 +33,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check", "--unwindset prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND},xQueuePeek.0:{QUEUE_PEEK_BOUND}", "--nondet-static" diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/Makefile.json index 568e517b1c..d5e70dd6a1 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/Makefile.json @@ -33,7 +33,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check", "--unwindset xQueueReceive.0:{QUEUE_RECEIVE_BOUND},prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}", "--nondet-static" diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/Makefile.json index e084d22f2a..ce5cd520a4 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/Makefile.json index 07f7c10340..8d164e0067 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/Makefile.json @@ -35,7 +35,6 @@ "CBMCFLAGS": [ "--unwind 2", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check", "--nondet-static", "--unwindset prvUnlockQueue.0:{QUEUE_BOUND},prvUnlockQueue.1:{QUEUE_BOUND},xQueueSemaphoreTake.0:3" diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/Makefile.json index 33b6e6cf25..b8c3d6e49e 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/Makefile.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/Makefile.json b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/Makefile.json index 210ead6b4a..6749aa463d 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/Makefile.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/Makefile.json @@ -38,7 +38,6 @@ "--unwind {QueueSemaphoreTake_BOUND}", "--unwindset prvUnlockQueue.0:{PRV_UNLOCK_UNWINDING_BOUND},prvUnlockQueue.1:{PRV_UNLOCK_UNWINDING_BOUND}", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/Configurations.json index 521839c3ce..a5ea435795 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/Configurations.json @@ -31,7 +31,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check" ], "OBJS": [ diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/Configurations.json index 516ea7df16..c3170fae08 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/Configurations.json @@ -32,7 +32,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check", "--unwindset prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}" ], diff --git a/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/Configurations.json b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/Configurations.json index 3d52cb4811..3f8549bf72 100644 --- a/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/Configurations.json +++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/Configurations.json @@ -32,7 +32,6 @@ "CBMCFLAGS": [ "--unwind 1", "--signed-overflow-check", - "--pointer-overflow-check", "--unsigned-overflow-check", "--unwindset prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}" ],