Remove or rework assumptions in queue proofs (#603)

This commit is paired with another to queue.c in the kernel.  To
accomodate changes in newer versions of CBMC, the
--pointer-overflow-check is removed.

33 files changed, 57 insertions, 124 deletions

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 58fcae48d..3eadf82d9 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 566544706..000000000
--- 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 fa5558f7f..01d518ed5 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 c7495bf29..3b6c4bb2e 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 4e26b37f8..eec7cba78 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 f079ecbdf..d0354bc7c 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 d9a9a8ec8..10fa56596 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 cb09c72b9..3b2a1a557 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 6409cd15a..51f3be625 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 7de7e05dc..3af3c5652 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 36848b6bf..45f1c379e 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 d7c4e86ed..f404c8f53 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 4fa87f8d2..40c3e7a02 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 0acbc976e..0e02630bd 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 553661cb2..fa7960e9d 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));
-
-    // QueueGenericReset does not check for multiplication overflow
-    __CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength);
+    /* Allow CBMC to run in a reasonable amount of time. */
+    __CPROVER_assume( ( uxQueueLength == QUEUE_LENGTH ) || ( uxItemSize == QUEUE_ITEM_SIZE ) );
 
-    // QueueGenericCreateStatic asserts positive queue length
-    __CPROVER_assume(uxQueueLength > ( UBaseType_t ) 0);
+    /* Prevent overflow in this harness. */
+    __CPROVER_assume( ( uxQueueLength > 0 ) && ( ( storageSize / uxQueueLength ) == uxItemSize ) );
 
-    // QueueGenericCreateStatic asserts the following equivalence
-    __CPROVER_assume( ( pucQueueStorage && uxItemSize ) ||
-                      ( !pucQueueStorage && !uxItemSize ) );
+    uint8_t * pucQueueStorage = ( uint8_t * ) pvPortMalloc( storageSize );
 
-    // 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 1759310d8..d523842a2 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 fbe4883a0..d174a773e 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 64e3e6789..e4435b1c1 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 92892ca85..ab240fc9a 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 ecc2b6230..73f8bdedd 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 647a0d03f..6005db359 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 ff71fd642..74e6418d4 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 8d1720fcd..bccd5db02 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 6c8806b2c..8e7bac96f 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 797d788a1..c85000cb4 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 568e517b1..d5e70dd6a 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 e084d22f2..ce5cd520a 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 07f7c1034..8d164e006 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 33b6e6cf2..b8c3d6e49 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 210ead6b4..6749aa463 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 521839c3c..a5ea43579 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 516ea7df1..c3170fae0 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 3d52cb481..3f8549bf7 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}"
   ],