diff --git a/FreeRTOS-Plus/Test/CBMC/.gitignore b/FreeRTOS-Plus/Test/CBMC/.gitignore
new file mode 100644
index 000000000..225be8104
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/.gitignore
@@ -0,0 +1,5 @@
+cbmc.txt
+property.xml
+coverage.xml
+*.goto
+**/html/*
\ No newline at end of file
diff --git a/FreeRTOS-Plus/Test/CBMC/README.md b/FreeRTOS-Plus/Test/CBMC/README.md
new file mode 100644
index 000000000..09d5e1481
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/README.md
@@ -0,0 +1,133 @@
+CBMC Proof Infrastructure
+=========================
+
+This directory contains automated proofs of the memory safety of various parts
+of the FreeRTOS codebase. A continuous integration system validates every
+pull request posted to the repository against these proofs, and developers can
+also run the proofs on their local machines.
+
+The proofs are checked using the
+[C Bounded Model Checker](http://www.cprover.org/cbmc/), an open-source static
+analysis tool
+([GitHub repository](https://github.com/diffblue/cbmc)). This README describes
+how to run the proofs on your local clone of a:FR.
+
+
+Bulding and running proofs
+--------------------------
+
+For historical reasons, some of the proofs are built and run using CMake
+and CTest. Others use a custom python-based build system. New proofs
+should use CMake. This README describes how to build and run both kinds
+of proof.
+
+
+CMake-based build
+-----------------
+
+Follow the CBMC installation instructions below.
+
+Suppose that the freertos source tree is located at
+`~/src/freertos` and you wish to build the proofs into
+`~/build/freertos`. The following three commands build and run
+the proofs:
+
+```sh
+cmake -S~/src/freertos -B~/build/freertos -DCOMPILER=cbmc
+-DBOARD=windows -DVENDOR=pc
+cmake --build ~/build/freertos --target all-proofs
+cd ~/build/freertos && ctest -L cbmc
+```
+
+Alternatively, this single command does the same thing, assuming you
+have the Ninja build tool installed:
+
+```sh
+ctest --build-and-test                \
+    ~/src/freertos             \
+    ~/build/freertos           \
+    --build-target cbmc               \
+    --build-generator Ninja           \
+    --build-options                   \
+      -DCOMPILER=cbmc                 \
+      -DBOARD=windows                 \
+      -DVENDOR=pc                     \
+    --test-command ctest -j4 -L cbmc --output-on-failure
+```
+
+
+
+Python-based build
+------------------
+
+### Prerequisites
+
+You will need Python 3. On Windows, you will need Visual Studio 2015 or later
+(in particular, you will need the Developer Command Prompt and NMake). On macOS
+and Linux, you will need Make.
+
+
+### Installing CBMC
+
+- Clone the [CBMC repository](https://github.com/diffblue/cbmc).
+
+- The canonical compilation and installation instructions are in the
+  [COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md)
+  file in the CBMC repository; we reproduce the most important steps for
+  Windows users here, but refer to that document if in doubt.
+  - Download and install CMake from the [CMake website](https://cmake.org/download).
+  - Download and install the "git for Windows" package, which also
+    provides the `patch` command, from [here](https://git-scm.com/download/win).
+  - Download the flex and bison for Windows package from
+    [this sourceforge site](https://sourceforge.net/projects/winflexbison).
+    "Install" it by dropping the contents of the entire unzipped
+    package into the top-level CBMC source directory.
+  - Change into the top-level CBMC source directory and run
+    ```
+    cmake -H. -Bbuild -DCMAKE_BUILD_TYPE=Release -DWITH_JBMC=OFF
+    cmake --build build
+    ```
+
+- Ensure that you can run the programs `cbmc`, `goto-cc` (or `goto-cl`
+  on Windows), and `goto-instrument` from the command line. If you build
+  CBMC with CMake, the programs will have been installed under the
+  `build/bin/Debug` directory under the top-level `cbmc` directory; you
+  should add that directory to your `$PATH`. If you built CBMC using
+  Make, then those programs will have been installed in the `src/cbmc`,
+  `src/goto-cc`, and `src/goto-instrument` directories respectively.
+
+
+### Setting up the proofs
+
+Change into the `proofs` directory. On Windows, run
+```
+python prepare.py
+```
+On macOS or Linux, run
+```
+./prepare.py
+```
+If you are on a Windows machine but want to generate Linux Makefiles (or vice
+versa), you can pass the `--system linux` or `--system windows` options to those
+programs.
+
+
+### Running the proofs
+
+Each of the leaf directories under `proofs` is a proof of the memory
+safety of a single entry point in FreeRTOS. The scripts that you ran in the
+previous step will have left a Makefile in each of those directories. To
+run a proof, change into the directory for that proof and run `nmake` on
+Windows or `make` on Linux or macOS. The proofs may take some time to
+run; they eventually write their output to `cbmc.txt`, which should have
+the text `VERIFICATION SUCCESSFUL` at the end.
+
+
+### Proof directory structure
+
+This directory contains the following subdirectories:
+
+- `proofs` contains the proofs run against each pull request
+- `patches` contains a set of patches that get applied to the codebase prior to
+  running the proofs
+- `include` and `windows` contain header files used by the proofs.
diff --git a/FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake b/FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake
new file mode 100644
index 000000000..819fa11bb
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/cmake/compute-coverage.cmake
@@ -0,0 +1,14 @@
+execute_process(
+    COMMAND
+        cbmc --cover location --xml-ui
+        ${cbmc_flags} ${cbmc_verbosity} ${goto_binary}
+    OUTPUT_FILE ${out_file}
+    ERROR_FILE ${out_file}
+    RESULT_VARIABLE res
+)
+
+if(NOT (${res} EQUAL 0 OR ${res} EQUAL 10))
+    message(FATAL_ERROR
+        "Unexpected CBMC coverage return code '${res}' for proof ${proof_name}. Log written to ${out_file}."
+    )
+endif()
diff --git a/FreeRTOS-Plus/Test/CBMC/cmake/compute-property.cmake b/FreeRTOS-Plus/Test/CBMC/cmake/compute-property.cmake
new file mode 100644
index 000000000..3192aa99a
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/cmake/compute-property.cmake
@@ -0,0 +1,14 @@
+execute_process(
+    COMMAND
+        cbmc --show-properties --unwinding-assertions --xml-ui
+        ${cbmc_flags} ${cbmc_verbosity} ${goto_binary}
+    OUTPUT_FILE ${out_file}
+    ERROR_FILE ${out_file}
+    RESULT_VARIABLE res
+)
+
+if(NOT (${res} EQUAL 0 OR ${res} EQUAL 10))
+    message(FATAL_ERROR
+        "Unexpected CBMC property return code '${res}' for proof ${proof_name}. Log written to ${out_file}."
+    )
+endif()
diff --git a/FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake b/FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake
new file mode 100644
index 000000000..8dc37b094
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/cmake/model-check.cmake
@@ -0,0 +1,14 @@
+execute_process(
+    COMMAND
+        cbmc --trace --unwinding-assertions
+        ${cbmc_flags} ${cbmc_verbosity} ${goto_binary}
+    OUTPUT_FILE ${out_file}
+    ERROR_FILE ${out_file}
+    RESULT_VARIABLE res
+)
+
+if(NOT (${res} EQUAL 0 OR ${res} EQUAL 10))
+    message(FATAL_ERROR
+        "Unexpected CBMC return code '${res}' for proof ${proof_name}. Log written to ${out_file}."
+    )
+endif()
diff --git a/FreeRTOS-Plus/Test/CBMC/include/README.md b/FreeRTOS-Plus/Test/CBMC/include/README.md
new file mode 100644
index 000000000..fa317dc04
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/include/README.md
@@ -0,0 +1,2 @@
+This directory contains include files used by the CBMC proofs:
+* cbmc.h defines some macros used in the proof test harnesses
diff --git a/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h
new file mode 100644
index 000000000..22434a91c
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h
@@ -0,0 +1,3 @@
+eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer ) {
+	prvProcessIPPacket(pxIPPacket, pxNetworkBuffer);
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h
new file mode 100644
index 000000000..01075d2ba
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h
@@ -0,0 +1,12 @@
+int32_t publicTCPPrepareSend( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer, UBaseType_t uxOptionsLength ) {
+	prvTCPPrepareSend( pxSocket, ppxNetworkBuffer, uxOptionsLength );
+}
+
+BaseType_t publicTCPHandleState( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer ) {
+	prvTCPHandleState(pxSocket, ppxNetworkBuffer);
+}
+
+void publicTCPReturnPacket( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer,
+	uint32_t ulLen, BaseType_t xReleaseAfterSend ) {
+	prvTCPReturnPacket(pxSocket, pxNetworkBuffer, ulLen, xReleaseAfterSend );
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/include/cbmc.h b/FreeRTOS-Plus/Test/CBMC/include/cbmc.h
new file mode 100644
index 000000000..a609dfcdb
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/include/cbmc.h
@@ -0,0 +1,67 @@
+/*
+ * CBMC models a pointer as an object id and an offset into that
+ * object.  The top bits of a pointer encode the object id and the
+ * remaining bits encode the offset.  This means there is a bound on
+ * the maximum offset into an object in CBMC, and hence a bound on the
+ * size of objects in CBMC.
+ */
+#define CBMC_BITS 7
+#define CBMC_MAX_OBJECT_SIZE (0xFFFFFFFF >> CBMC_BITS)
+
+enum CBMC_LOOP_CONDITION { CBMC_LOOP_BREAK, CBMC_LOOP_CONTINUE, CBMC_LOOP_RETURN };
+
+// CBMC specification: capture old value for precondition /
+// postcondition checking
+
+#define OLDVAL(var) _old_ ## var
+#define SAVE_OLDVAL(var,typ) const typ OLDVAL(var) = var
+
+// CBMC specification: capture old value for values passed by
+// reference in function abstractions
+
+#define OBJ(var) (*var)
+#define OLDOBJ(var) _oldobj_ ## var
+#define SAVE_OLDOBJ(var,typ) const typ OLDOBJ(var) = OBJ(var)
+
+// CBMC debugging: printfs for expressions
+
+#define __CPROVER_printf(var) { uint32_t ValueOf_ ## var = (uint32_t) var; }
+#define __CPROVER_printf2(str,exp) { uint32_t ValueOf_ ## str = (uint32_t) (exp); }
+
+// CBMC debugging: printfs for pointer expressions
+
+#define __CPROVER_printf_ptr(var) { uint8_t *ValueOf_ ## var = (uint8_t *) var; }
+#define __CPROVER_printf2_ptr(str,exp) { uint8_t *ValueOf_ ## str = (uint8_t *) (exp); }
+
+/*
+ * An assertion that pvPortMalloc returns NULL when asked to allocate 0 bytes.
+ * This assertion is used in some of the Task proofs.
+ */
+#define __CPROVER_assert_zero_allocation() \
+        __CPROVER_assert( pvPortMalloc(0) == NULL, \
+			  "pvPortMalloc allows zero-allocated memory.")
+
+/*
+ * A stub for pvPortMalloc that nondeterministically chooses to return
+ * either NULL or an allocation of the requested space.  The stub is
+ * guaranteed to return NULL when asked to allocate 0 bytes.
+ * This stub is used in some of the Task proofs.
+ */
+void *pvPortMalloc( size_t xWantedSize )
+{
+	if ( xWantedSize == 0 )
+	{
+		return NULL;
+	}
+	return nondet_bool() ? malloc( xWantedSize ) : NULL;
+}
+
+void vPortFree( void *pv )
+{
+	(void)pv;
+	free(pv);
+}
+
+BaseType_t nondet_basetype();
+UBaseType_t nondet_ubasetype();
+TickType_t nondet_ticktype();
diff --git a/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h b/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h
new file mode 100644
index 000000000..a0dd6de4a
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/include/tasksStubs.h
@@ -0,0 +1,10 @@
+#ifndef INC_TASK_STUBS_H
+#define INC_TASK_STUBS_H
+
+#include "FreeRTOS.h"
+#include "task.h"
+
+BaseType_t xState;
+void vInitTaskCheckForTimeOut(BaseType_t maxCounter, BaseType_t maxCounter_limit);
+
+#endif /* INC_TASK_STUBS_H */
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/.gitattributes b/FreeRTOS-Plus/Test/CBMC/patches/.gitattributes
new file mode 100644
index 000000000..a41fc7b45
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/.gitattributes
@@ -0,0 +1,2 @@
+# It seems git apply does not want crlf line endings on Windows
+*.patch eol=lf
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/.gitignore b/FreeRTOS-Plus/Test/CBMC/patches/.gitignore
new file mode 100644
index 000000000..4dec98ff0
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/.gitignore
@@ -0,0 +1,2 @@
+auto_patch*
+patched
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0001-Remove-static-storage-class-from-entry-points.patch b/FreeRTOS-Plus/Test/CBMC/patches/0001-Remove-static-storage-class-from-entry-points.patch
new file mode 100644
index 000000000..fa7d7451f
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/0001-Remove-static-storage-class-from-entry-points.patch
@@ -0,0 +1,121 @@
+From 884e69144abac08d203bbf8257c6b4a96a2a91ea Mon Sep 17 00:00:00 2001
+From: "Mark R. Tuttle" <mrtuttle@amazon.com>
+Date: Mon, 21 Oct 2019 14:17:50 -0400
+Subject: [PATCH] Remove static storage class from entry points
+
+Many of the entry points we wish to test are marked as being static.
+This commit removes the static keyword from all entry points that we
+test.
+
+Patch revised on October 21, 2019.
+---
+ .../freertos_plus_tcp/source/FreeRTOS_DHCP.c         |  6 +++---
+ .../standard/freertos_plus_tcp/source/FreeRTOS_DNS.c | 12 ++++++------
+ .../freertos_plus_tcp/source/FreeRTOS_TCP_WIN.c      |  2 +-
+ 3 files changed, 10 insertions(+), 10 deletions(-)
+
+diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
+index c4f79e8e7..d8089a5e7 100644
+--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
++++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
+@@ -198,7 +198,7 @@ static void prvSendDHCPDiscover( void );
+ /*
+  * Interpret message received on the DHCP socket.
+  */
+-static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
++BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
+
+ /*
+  * Generate a DHCP request packet, and send it on the DHCP socket.
+@@ -234,7 +234,7 @@ static void prvCreateDHCPSocket( void );
+ /*-----------------------------------------------------------*/
+
+ /* The next DHCP transaction Id to be used. */
+-static DHCPData_t xDHCPData;
++DHCPData_t xDHCPData;
+
+ /*-----------------------------------------------------------*/
+
+@@ -607,7 +607,7 @@ static void prvInitialiseDHCP( void )
+ }
+ /*-----------------------------------------------------------*/
+
+-static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType )
++BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType )
+ {
+ uint8_t *pucUDPPayload, *pucLastByte;
+ struct freertos_sockaddr xClient;
+diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
+index e511ca324..d6f335304 100644
+--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
++++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
+@@ -116,7 +116,7 @@ static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
+ /*
+  * Simple routine that jumps over the NAME field of a resource record.
+  */
+-static uint8_t * prvSkipNameField( uint8_t *pucByte,
++uint8_t * prvSkipNameField( uint8_t *pucByte,
+ 								   size_t uxSourceLen );
+
+ /*
+@@ -124,7 +124,7 @@ static uint8_t * prvSkipNameField( uint8_t *pucByte,
+  * The parameter 'xExpected' indicates whether the identifier in the reply
+  * was expected, and thus if the DNS cache may be updated with the reply.
+  */
+-static uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
++uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
+ 								  size_t uxBufferLength,
+ 								  BaseType_t xExpected );
+
+@@ -152,7 +152,7 @@ static uint32_t prvGetHostByName( const char *pcHostName,
+
+
+ #if( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 )
+-	static uint8_t * prvReadNameField( uint8_t *pucByte,
++	uint8_t * prvReadNameField( uint8_t *pucByte,
+ 									   size_t uxSourceLen,
+ 									   char *pcName,
+ 									   size_t uxLen );
+@@ -765,7 +765,7 @@ static const DNSMessage_t xDefaultPartDNSHeader =
+
+ #if( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 )
+
+-	static uint8_t * prvReadNameField( uint8_t *pucByte,
++	uint8_t * prvReadNameField( uint8_t *pucByte,
+ 									   size_t uxSourceLen,
+ 									   char *pcName,
+ 									   size_t uxDestLen )
+@@ -843,7 +843,7 @@ static const DNSMessage_t xDefaultPartDNSHeader =
+ #endif /* ipconfigUSE_DNS_CACHE || ipconfigDNS_USE_CALLBACKS */
+ /*-----------------------------------------------------------*/
+
+-static uint8_t * prvSkipNameField( uint8_t *pucByte,
++uint8_t * prvSkipNameField( uint8_t *pucByte,
+ 								   size_t uxSourceLen )
+ {
+ size_t uxChunkLength;
+@@ -949,7 +949,7 @@ DNSMessage_t *pxDNSMessageHeader;
+ #endif /* ipconfigUSE_NBNS */
+ /*-----------------------------------------------------------*/
+
+-static uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
++uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
+ 								  size_t uxBufferLength,
+ 								  BaseType_t xExpected )
+ {
+diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c
+index 1f5a845fa..1a69807c0 100644
+--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c
++++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c
+@@ -206,7 +206,7 @@ extern void vListInsertGeneric( List_t * const pxList, ListItem_t * const pxNewL
+
+ /* List of free TCP segments. */
+ #if( ipconfigUSE_TCP_WIN == 1 )
+-	static List_t xSegmentList;
++	List_t xSegmentList;
+ #endif
+
+ /* Logging verbosity level. */
+--
+2.20.1 (Apple Git-117)
+
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch b/FreeRTOS-Plus/Test/CBMC/patches/0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch
new file mode 100644
index 000000000..8e096a5a9
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch
@@ -0,0 +1,26 @@
+From b7fbcc3979324838ec240b28717bfd7918bbb388 Mon Sep 17 00:00:00 2001
+From: Kareem Khazem <karkhaz@amazon.com>
+Date: Thu, 31 Jan 2019 15:07:52 -0800
+Subject: [PATCH 2/4] Change FreeRTOS_IP_Private.h union to struct
+
+This patch should be removed soon: It is for a CBMC issue being fixed now.
+---
+ libraries/freertos_plus/standard/freertos_plus_tcp/include/FreeRTOS_IP_Private.h | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h
+index 6006f89f0..d1a0cf898 100644
+--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h
++++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h
+@@ -643,7 +643,7 @@ typedef struct XSOCKET
+ 	/* Before accessing any member of this structure, it should be confirmed */
+ 	/* that the protocol corresponds with the type of structure */
+ 
+-	union
++	struct
+ 	{
+ 		IPUDPSocket_t xUDP;
+ 		#if( ipconfigUSE_TCP == 1 )
+-- 
+2.21.0
+
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch b/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch
new file mode 100644
index 000000000..29cde0e77
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/0005-Remove-volatile-qualifier-from-tasks-variables.patch
@@ -0,0 +1,79 @@
+This patch removes the volatile qualifier from some global variable
+declarations in the tasks.c file.  For task pool proofs, we are running
+`goto-instrument` with the `--nondet-volatile` flag on, which causes reads from
+volatile variable to be nondeterministic (i.e., any possible value can be
+returned).  This is actually the desired behavior for volatile variables
+regarding verification purposes. However, this causes a lot of trouble when
+such variables are pointers, since one of the possible values we can get when
+dereferencing a volatile pointer is `NULL`.
+
+In the case of `uxPendedTicks`, a non-volatile copy of the variable is done
+before the following loop in tasks.c (lines 2231-2255):
+
+{
+	UBaseType_t uxPendedCounts = uxPendedTicks; /* Non-volatile copy. */
+
+	if( uxPendedCounts > ( UBaseType_t ) 0U )
+	{
+		do
+		{
+			if( xTaskIncrementTick() != pdFALSE )
+			{
+				xYieldPending = pdTRUE;
+			}
+			else
+			{
+				mtCOVERAGE_TEST_MARKER();
+			}
+			--uxPendedCounts;
+		} while( uxPendedCounts > ( UBaseType_t ) 0U );
+
+		uxPendedTicks = 0;
+	}
+	else
+	{
+		mtCOVERAGE_TEST_MARKER();
+	}
+}
+
+Here, `uxPendedTicks` could return any value, making it impossible to unwind
+(or unroll) this loop in CBMC.  Therefore, we require `uxPendedTicks` to behave
+as a regular variable so that the loop can be unwound.
+
+---
+diff --git a/FreeRTOS/Source/tasks.c b/FreeRTOS/Source/tasks.c
+index ff657733..8b57d198 100644
+--- a/FreeRTOS/Source/tasks.c
++++ b/FreeRTOS/Source/tasks.c
+@@ -331,7 +331,7 @@ typedef tskTCB TCB_t;
+ 
+ /*lint -save -e956 A manual analysis and inspection has been used to determine
+ which static variables must be declared volatile. */
+-PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL;
++PRIVILEGED_DATA TCB_t * pxCurrentTCB = NULL;
+ 
+ /* Lists for ready and blocked tasks. --------------------
+ xDelayedTaskList1 and xDelayedTaskList2 could be move to function scople but
+@@ -340,8 +340,8 @@ the static qualifier. */
+ PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ];/*< Prioritised ready tasks. */
+ PRIVILEGED_DATA static List_t xDelayedTaskList1;						/*< Delayed tasks. */
+ PRIVILEGED_DATA static List_t xDelayedTaskList2;						/*< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */
+-PRIVILEGED_DATA static List_t * volatile pxDelayedTaskList;				/*< Points to the delayed task list currently being used. */
+-PRIVILEGED_DATA static List_t * volatile pxOverflowDelayedTaskList;		/*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */
++PRIVILEGED_DATA static List_t * pxDelayedTaskList;				/*< Points to the delayed task list currently being used. */
++PRIVILEGED_DATA static List_t * pxOverflowDelayedTaskList;		/*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */
+ PRIVILEGED_DATA static List_t xPendingReadyList;						/*< Tasks that have been readied while the scheduler was suspended.  They will be moved to the ready list when the scheduler is resumed. */
+ 
+ #if( INCLUDE_vTaskDelete == 1 )
+@@ -368,10 +368,10 @@ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks 	= ( UBaseTyp
+ 
+ /* Other file private variables. --------------------------------*/
+ PRIVILEGED_DATA static volatile UBaseType_t uxCurrentNumberOfTasks 	= ( UBaseType_t ) 0U;
+ PRIVILEGED_DATA static volatile TickType_t xTickCount 				= ( TickType_t ) configINITIAL_TICK_COUNT;
+ PRIVILEGED_DATA static volatile UBaseType_t uxTopReadyPriority 		= tskIDLE_PRIORITY;
+ PRIVILEGED_DATA static volatile BaseType_t xSchedulerRunning 		= pdFALSE;
+-PRIVILEGED_DATA static volatile TickType_t xPendedTicks 			= ( TickType_t ) 0U;
++PRIVILEGED_DATA static TickType_t xPendedTicks 			= ( TickType_t ) 0U;
+ PRIVILEGED_DATA static volatile BaseType_t xYieldPending 			= pdFALSE;
+ PRIVILEGED_DATA static volatile BaseType_t xNumOfOverflows 			= ( BaseType_t ) 0;
+ PRIVILEGED_DATA static UBaseType_t uxTaskNumber 					= ( UBaseType_t ) 0U;
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch b/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch
new file mode 100644
index 000000000..5a79ae8cd
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/0005-remove-static-from-prvCopyDataToQueue.patch
@@ -0,0 +1,22 @@
+diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
+index df2b9c8c..c2265c26 100644
+--- a/FreeRTOS/Source/queue.c
++++ b/FreeRTOS/Source/queue.c
+@@ -105,7 +105,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.
+  */
+-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION;
++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition ) PRIVILEGED_FUNCTION;
+
+ /*
+  * Copies an item out of a queue.
+@@ -1985,7 +1985,7 @@ Queue_t * const pxQueue = xQueue;
+ #endif /* configUSE_MUTEXES */
+ /*-----------------------------------------------------------*/
+
+-static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition )
++BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition )
+ {
+ BaseType_t xReturn = pdFALSE;
+ UBaseType_t uxMessagesWaiting;
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch b/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch
new file mode 100644
index 000000000..9cbe7cf5f
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/0006-Remove-static-from-prvNotifyQueueSetContainer.patch
@@ -0,0 +1,22 @@
+diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
+index 17a6964e..24a40c29 100644
+--- a/FreeRTOS/Source/queue.c
++++ b/FreeRTOS/Source/queue.c
+@@ -207,7 +207,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer
+ 	 * Checks to see if a queue is a member of a queue set, and if so, notifies
+ 	 * the queue set that the queue contains data.
+ 	 */
+-	static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
++	BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
+ #endif
+
+ /*
+@@ -2887,7 +2887,7 @@ Queue_t * const pxQueue = xQueue;
+
+ #if ( configUSE_QUEUE_SETS == 1 )
+
+-	static BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue )
++	BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue )
+ 	{
+ 	Queue_t *pxQueueSetContainer = pxQueue->pxQueueSetContainer;
+ 	BaseType_t xReturn = pdFALSE;
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch b/FreeRTOS-Plus/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch
new file mode 100644
index 000000000..eaae401c6
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/0007-Remove-static-from-prvUnlockQueue.patch
@@ -0,0 +1,22 @@
+diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
+index 17a6964e..60ea3e69 100644
+--- a/FreeRTOS/Source/queue.c
++++ b/FreeRTOS/Source/queue.c
+@@ -175,7 +175,7 @@ typedef xQUEUE Queue_t;
+  * to indicate that a task may require unblocking.  When the queue in unlocked
+  * these lock counts are inspected, and the appropriate action taken.
+  */
+-static void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
++void prvUnlockQueue( Queue_t * const pxQueue ) PRIVILEGED_FUNCTION;
+
+ /*
+  * Uses a critical section to determine if there is any data in a queue.
+@@ -2175,7 +2175,7 @@ static void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer
+ }
+ /*-----------------------------------------------------------*/
+
+-static void prvUnlockQueue( Queue_t * const pxQueue )
++void prvUnlockQueue( Queue_t * const pxQueue )
+ {
+ 	/* THIS FUNCTION MUST BE CALLED WITH THE SCHEDULER SUSPENDED. */
+
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/0008-Remove-static-attributes-from-functions-implementing.patch b/FreeRTOS-Plus/Test/CBMC/patches/0008-Remove-static-attributes-from-functions-implementing.patch
new file mode 100644
index 000000000..c8f9c36e6
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/0008-Remove-static-attributes-from-functions-implementing.patch
@@ -0,0 +1,68 @@
+From 18ca738652bd0ce0a1345cb3dcd7ffacbc196bfa Mon Sep 17 00:00:00 2001
+From: "Mark R. Tuttle" <mrtuttle@amazon.com>
+Date: Wed, 30 Oct 2019 09:38:56 -0400
+Subject: [PATCH] Remove static attributes from functions implementing
+ prvCheckOptions for CBMC proofs.
+
+---
+ .../freertos_plus_tcp/source/FreeRTOS_TCP_IP.c       | 12 ++++++------
+ 1 file changed, 6 insertions(+), 6 deletions(-)
+
+diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c
+index 4378e28de..2cd072d24 100644
+--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c
++++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c
+@@ -225,20 +225,20 @@ static BaseType_t prvTCPPrepareConnect( FreeRTOS_Socket_t *pxSocket );
+ /*
+  * Parse the TCP option(s) received, if present.
+  */
+-static void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer );
++void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer );
+ 
+ /*
+  * Identify and deal with a single TCP header option, advancing the pointer to
+  * the header. This function returns pdTRUE or pdFALSE depending on whether the
+  * caller should continue to parse more header options or break the loop.
+  */
+-static BaseType_t prvSingleStepTCPHeaderOptions( const unsigned char ** const ppucPtr, const unsigned char ** const ppucLast, FreeRTOS_Socket_t ** const ppxSocket, TCPWindow_t ** const ppxTCPWindow);
++BaseType_t prvSingleStepTCPHeaderOptions( const unsigned char ** const ppucPtr, const unsigned char ** const ppucLast, FreeRTOS_Socket_t ** const ppxSocket, TCPWindow_t ** const ppxTCPWindow);
+ 
+ /*
+  * Skip past TCP header options when doing Selective ACK, until there are no
+  * more options left.
+  */
+-static void prvSkipPastRemainingOptions( const unsigned char ** const ppucPtr, FreeRTOS_Socket_t ** const ppxSocket, unsigned char * const ppucLen );
++void prvSkipPastRemainingOptions( const unsigned char ** const ppucPtr, FreeRTOS_Socket_t ** const ppxSocket, unsigned char * const ppucLen );
+ 
+ /*
+  * Set the initial properties in the options fields, like the preferred
+@@ -1157,7 +1157,7 @@ uint32_t ulInitialSequenceNumber = 0;
+  * that: ((pxTCPHeader->ucTCPOffset & 0xf0) > 0x50), meaning that the TP header
+  * is longer than the usual 20 (5 x 4) bytes.
+  */
+-static void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer )
++void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer )
+ {
+ TCPPacket_t * pxTCPPacket;
+ TCPHeader_t * pxTCPHeader;
+@@ -1191,7 +1191,7 @@ BaseType_t xShouldContinueLoop;
+ 
+ /*-----------------------------------------------------------*/
+ 
+-static BaseType_t prvSingleStepTCPHeaderOptions( const unsigned char ** const ppucPtr, const unsigned char ** const ppucLast, FreeRTOS_Socket_t ** const ppxSocket, TCPWindow_t ** const ppxTCPWindow)
++BaseType_t prvSingleStepTCPHeaderOptions( const unsigned char ** const ppucPtr, const unsigned char ** const ppucLast, FreeRTOS_Socket_t ** const ppxSocket, TCPWindow_t ** const ppxTCPWindow)
+ {
+ 	UBaseType_t uxNewMSS;
+ 	UBaseType_t xRemainingOptionsBytes = ( *ppucLast ) - ( *ppucPtr );
+@@ -1319,7 +1319,7 @@ static BaseType_t prvSingleStepTCPHeaderOptions( const unsigned char ** const pp
+ 
+ /*-----------------------------------------------------------*/
+ 
+-static void prvSkipPastRemainingOptions( const unsigned char ** const ppucPtr, FreeRTOS_Socket_t ** const ppxSocket, unsigned char * const pucLen )
++void prvSkipPastRemainingOptions( const unsigned char ** const ppucPtr, FreeRTOS_Socket_t ** const ppxSocket, unsigned char * const pucLen )
+ {
+ uint32_t ulFirst = ulChar2u32( ( *ppucPtr ) );
+ uint32_t ulLast  = ulChar2u32( ( *ppucPtr ) + 4 );
+-- 
+2.20.1 (Apple Git-117)
+
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h
new file mode 100644
index 000000000..28de2bd15
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSConfig.h
@@ -0,0 +1,237 @@
+/*
+ * FreeRTOS Kernel V10.0.1
+ * Copyright (C) 2017 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * http://aws.amazon.com/freertos
+ * http://www.FreeRTOS.org
+ */
+
+#ifndef FREERTOS_CONFIG_H
+#define FREERTOS_CONFIG_H
+
+/*-----------------------------------------------------------
+* Application specific definitions.
+*
+* These definitions should be adjusted for your particular hardware and
+* application requirements.
+*
+* THESE PARAMETERS ARE DESCRIBED WITHIN THE 'CONFIGURATION' SECTION OF THE
+* FreeRTOS API DOCUMENTATION AVAILABLE ON THE FreeRTOS.org WEB SITE.
+* http://www.freertos.org/a00110.html
+*
+* The bottom of this file contains some constants specific to running the UDP
+* stack in this demo.  Constants specific to FreeRTOS+TCP itself (rather than
+* the demo) are contained in FreeRTOSIPConfig.h.
+*----------------------------------------------------------*/
+#define configENABLE_BACKWARD_COMPATIBILITY        1
+#define configUSE_PREEMPTION                       1
+#define configUSE_PORT_OPTIMISED_TASK_SELECTION    1
+#define configMAX_PRIORITIES                       ( 7 )
+#define configTICK_RATE_HZ                         ( 1000 )                  /* In this non-real time simulated environment the tick frequency has to be at least a multiple of the Win32 tick frequency, and therefore very slow. */
+#define configMINIMAL_STACK_SIZE                   ( ( unsigned short ) 60 ) /* In this simulated case, the stack only has to hold one small structure as the real stack is part of the Win32 thread. */
+#define configTOTAL_HEAP_SIZE                      ( ( size_t ) ( 2048U * 1024U ) )
+#define configMAX_TASK_NAME_LEN                    ( 15 )
+#define configUSE_16_BIT_TICKS                     0
+#define configIDLE_SHOULD_YIELD                    1
+#define configUSE_CO_ROUTINES                      0
+#ifndef configUSE_MUTEXES
+    #define configUSE_MUTEXES                          1
+#endif
+#ifndef configUSE_RECURSIVE_MUTEXES
+    #define configUSE_RECURSIVE_MUTEXES                1
+#endif
+#define configQUEUE_REGISTRY_SIZE                  0
+#define configUSE_APPLICATION_TASK_TAG             1
+#define configUSE_COUNTING_SEMAPHORES              1
+#define configUSE_ALTERNATIVE_API                  0
+#define configNUM_THREAD_LOCAL_STORAGE_POINTERS    3      /* FreeRTOS+FAT requires 2 pointers if a CWD is supported. */
+#define configRECORD_STACK_HIGH_ADDRESS            1
+
+/* Hook function related definitions. */
+#ifndef configUSE_TICK_HOOK
+    #define configUSE_TICK_HOOK                        0
+#endif
+#define configUSE_IDLE_HOOK                        1
+#define configUSE_MALLOC_FAILED_HOOK               1
+#define configCHECK_FOR_STACK_OVERFLOW             0      /* Not applicable to the Win32 port. */
+
+/* Software timer related definitions. */
+#define configUSE_TIMERS                           1
+#define configTIMER_TASK_PRIORITY                  ( configMAX_PRIORITIES - 1 )
+#define configTIMER_QUEUE_LENGTH                   5
+#define configTIMER_TASK_STACK_DEPTH               ( configMINIMAL_STACK_SIZE * 2 )
+
+/* Event group related definitions. */
+#define configUSE_EVENT_GROUPS                     1
+
+/* Co-routine definitions. */
+#define configUSE_CO_ROUTINES                   0
+#define configMAX_CO_ROUTINE_PRIORITIES         ( 2 )
+
+/* Memory allocation strategy. */
+#ifndef configSUPPORT_DYNAMIC_ALLOCATION
+    #define configSUPPORT_DYNAMIC_ALLOCATION        1
+#endif
+#ifndef configSUPPORT_STATIC_ALLOCATION
+    #define configSUPPORT_STATIC_ALLOCATION         1
+#endif
+
+
+/* Set the following definitions to 1 to include the API function, or zero
+ * to exclude the API function. */
+#define INCLUDE_vTaskPrioritySet                1
+#define INCLUDE_uxTaskPriorityGet               1
+#define INCLUDE_vTaskDelete                     1
+#define INCLUDE_vTaskCleanUpResources           0
+#ifndef INCLUDE_vTaskSuspend
+    #define INCLUDE_vTaskSuspend                    1
+#endif
+#define INCLUDE_vTaskDelayUntil                 1
+#define INCLUDE_vTaskDelay                      1
+#define INCLUDE_uxTaskGetStackHighWaterMark     1
+#ifndef INCLUDE_xTaskGetSchedulerState
+    #define INCLUDE_xTaskGetSchedulerState          1
+#endif
+#define INCLUDE_xTimerGetTimerTaskHandle        0
+#define INCLUDE_xTaskGetIdleTaskHandle          0
+#define INCLUDE_xQueueGetMutexHolder            1
+#define INCLUDE_eTaskGetState                   1
+#define INCLUDE_xEventGroupSetBitsFromISR       1
+#define INCLUDE_xTimerPendFunctionCall          1
+#define INCLUDE_xTaskGetCurrentTaskHandle       1
+#define INCLUDE_xTaskAbortDelay                 1
+
+/* This demo makes use of one or more example stats formatting functions.  These
+ * format the raw data provided by the uxTaskGetSystemState() function in to human
+ * readable ASCII form.  See the notes in the implementation of vTaskList() within
+ * FreeRTOS/Source/tasks.c for limitations.  configUSE_STATS_FORMATTING_FUNCTIONS
+ * is set to 2 so the formatting functions are included without the stdio.h being
+ * included in tasks.c.  That is because this project defines its own sprintf()
+ * functions. */
+#define configUSE_STATS_FORMATTING_FUNCTIONS    1
+
+/* Assert call defined for debug builds. */
+extern void vAssertCalled( const char * pcFile,
+                           uint32_t ulLine );
+#ifndef configASSERT
+#define configASSERT( x )    if( ( x ) == 0 ) vAssertCalled( __FILE__, __LINE__ )
+#endif
+
+/* Remove logging in formal verification */
+#define configPRINTF( X )
+
+/* Non-format version thread-safe print. */
+#define configPRINT_STRING( X )
+
+/* Application specific definitions follow. **********************************/
+
+/* If configINCLUDE_DEMO_DEBUG_STATS is set to one, then a few basic IP trace
+ * macros are defined to gather some UDP stack statistics that can then be viewed
+ * through the CLI interface. */
+#define configINCLUDE_DEMO_DEBUG_STATS       1
+
+/* The size of the global output buffer that is available for use when there
+ * are multiple command interpreters running at once (for example, one on a UART
+ * and one on TCP/IP).  This is done to prevent an output buffer being defined by
+ * each implementation - which would waste RAM.  In this case, there is only one
+ * command interpreter running, and it has its own local output buffer, so the
+ * global buffer is just set to be one byte long as it is not used and should not
+ * take up unnecessary RAM. */
+#define configCOMMAND_INT_MAX_OUTPUT_SIZE    1
+
+/* Only used when running in the FreeRTOS Windows simulator.  Defines the
+ * priority of the task used to simulate Ethernet interrupts. */
+#define configMAC_ISR_SIMULATOR_PRIORITY     ( configMAX_PRIORITIES - 1 )
+
+/* This demo creates a virtual network connection by accessing the raw Ethernet
+ * or WiFi data to and from a real network connection.  Many computers have more
+ * than one real network port, and configNETWORK_INTERFACE_TO_USE is used to tell
+ * the demo which real port should be used to create the virtual port.  The ports
+ * available are displayed on the console when the application is executed.  For
+ * example, on my development laptop setting configNETWORK_INTERFACE_TO_USE to 4
+ * results in the wired network being used, while setting
+ * configNETWORK_INTERFACE_TO_USE to 2 results in the wireless network being
+ * used. */
+#define configNETWORK_INTERFACE_TO_USE       ( 0L )
+
+/* The address of an echo server that will be used by the two demo echo client
+ * tasks:
+ * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Echo_Clients.html,
+ * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/UDP_Echo_Clients.html. */
+#define configECHO_SERVER_ADDR0              192
+#define configECHO_SERVER_ADDR1              168
+#define configECHO_SERVER_ADDR2              2
+#define configECHO_SERVER_ADDR3              6
+#define configTCP_ECHO_CLIENT_PORT           7
+
+/* Default MAC address configuration.  The demo creates a virtual network
+ * connection that uses this MAC address by accessing the raw Ethernet/WiFi data
+ * to and from a real network connection on the host PC.  See the
+ * configNETWORK_INTERFACE_TO_USE definition above for information on how to
+ * configure the real network connection to use. */
+#define configMAC_ADDR0                      0x00
+#define configMAC_ADDR1                      0x11
+#define configMAC_ADDR2                      0x22
+#define configMAC_ADDR3                      0x33
+#define configMAC_ADDR4                      0x44
+#define configMAC_ADDR5                      0x21
+
+/* Default IP address configuration.  Used in ipconfigUSE_DHCP is set to 0, or
+ * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */
+#define configIP_ADDR0                       192
+#define configIP_ADDR1                       168
+#define configIP_ADDR2                       0
+#define configIP_ADDR3                       105
+
+/* Default gateway IP address configuration.  Used in ipconfigUSE_DHCP is set to
+ * 0, or ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */
+#define configGATEWAY_ADDR0                  192
+#define configGATEWAY_ADDR1                  168
+#define configGATEWAY_ADDR2                  0
+#define configGATEWAY_ADDR3                  1
+
+/* Default DNS server configuration.  OpenDNS addresses are 208.67.222.222 and
+ * 208.67.220.220.  Used in ipconfigUSE_DHCP is set to 0, or ipconfigUSE_DHCP is
+ * set to 1 but a DNS server cannot be contacted.*/
+#define configDNS_SERVER_ADDR0               208
+#define configDNS_SERVER_ADDR1               67
+#define configDNS_SERVER_ADDR2               222
+#define configDNS_SERVER_ADDR3               222
+
+/* Default netmask configuration.  Used in ipconfigUSE_DHCP is set to 0, or
+ * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */
+#define configNET_MASK0                      255
+#define configNET_MASK1                      255
+#define configNET_MASK2                      255
+#define configNET_MASK3                      0
+
+/* The UDP port to which print messages are sent. */
+#define configPRINT_PORT                     ( 15000 )
+
+#define configPROFILING                      ( 0 )
+
+/* Pseudo random number generater used by some demo tasks. */
+extern uint32_t ulRand();
+#define configRAND32()    ulRand()
+
+/* The platform that FreeRTOS is running on. */
+#define configPLATFORM_NAME    "WinSim"
+
+#endif /* FREERTOS_CONFIG_H */
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSIPConfig.h b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSIPConfig.h
new file mode 100644
index 000000000..81165e3bd
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/FreeRTOSIPConfig.h
@@ -0,0 +1,305 @@
+/*
+FreeRTOS Kernel V10.2.0
+Copyright (C) 2017 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the "Software"), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+the Software, and to permit persons to whom the Software is furnished to do so,
+subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+ http://aws.amazon.com/freertos
+ http://www.FreeRTOS.org
+*/
+
+
+/*****************************************************************************
+*
+* See the following URL for configuration information.
+* http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_IP_Configuration.html
+*
+*****************************************************************************/
+
+#ifndef FREERTOS_IP_CONFIG_H
+#define FREERTOS_IP_CONFIG_H
+
+/* Set to 1 to print out debug messages.  If ipconfigHAS_DEBUG_PRINTF is set to
+ * 1 then FreeRTOS_debug_printf should be defined to the function used to print
+ * out the debugging messages. */
+#define ipconfigHAS_DEBUG_PRINTF    0
+#if ( ipconfigHAS_DEBUG_PRINTF == 1 )
+    #define FreeRTOS_debug_printf( X )    configPRINTF( X )
+#endif
+
+/* Set to 1 to print out non debugging messages, for example the output of the
+ * FreeRTOS_netstat() command, and ping replies.  If ipconfigHAS_PRINTF is set to 1
+ * then FreeRTOS_printf should be set to the function used to print out the
+ * messages. */
+#define FreeRTOS_printf( X )
+
+
+/* Define the byte order of the target MCU (the MCU FreeRTOS+TCP is executing
+ * on).  Valid options are pdFREERTOS_BIG_ENDIAN and pdFREERTOS_LITTLE_ENDIAN. */
+#define ipconfigBYTE_ORDER                         pdFREERTOS_LITTLE_ENDIAN
+
+/* If the network card/driver includes checksum offloading (IP/TCP/UDP checksums)
+ * then set ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM to 1 to prevent the software
+ * stack repeating the checksum calculations. */
+#define ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM     1
+
+/* Several API's will block until the result is known, or the action has been
+ * performed, for example FreeRTOS_send() and FreeRTOS_recv().  The timeouts can be
+ * set per socket, using setsockopt().  If not set, the times below will be
+ * used as defaults. */
+#define ipconfigSOCK_DEFAULT_RECEIVE_BLOCK_TIME    ( 5000 )
+#define ipconfigSOCK_DEFAULT_SEND_BLOCK_TIME       ( 5000 )
+
+/* Include support for DNS caching.  For TCP, having a small DNS cache is very
+ * useful.  When a cache is present, ipconfigDNS_REQUEST_ATTEMPTS can be kept low
+ * and also DNS may use small timeouts.  If a DNS reply comes in after the DNS
+ * socket has been destroyed, the result will be stored into the cache.  The next
+ * call to FreeRTOS_gethostbyname() will return immediately, without even creating
+ * a socket. */
+#define ipconfigUSE_DNS_CACHE                      ( 1 )
+#define ipconfigDNS_REQUEST_ATTEMPTS               ( 2 )
+
+/* The IP stack executes it its own task (although any application task can make
+ * use of its services through the published sockets API). ipconfigUDP_TASK_PRIORITY
+ * sets the priority of the task that executes the IP stack.  The priority is a
+ * standard FreeRTOS task priority so can take any value from 0 (the lowest
+ * priority) to (configMAX_PRIORITIES - 1) (the highest priority).
+ * configMAX_PRIORITIES is a standard FreeRTOS configuration parameter defined in
+ * FreeRTOSConfig.h, not FreeRTOSIPConfig.h. Consideration needs to be given as to
+ * the priority assigned to the task executing the IP stack relative to the
+ * priority assigned to tasks that use the IP stack. */
+#define ipconfigIP_TASK_PRIORITY                   ( configMAX_PRIORITIES - 2 )
+
+/* The size, in words (not bytes), of the stack allocated to the FreeRTOS+TCP
+ * task.  This setting is less important when the FreeRTOS Win32 simulator is used
+ * as the Win32 simulator only stores a fixed amount of information on the task
+ * stack.  FreeRTOS includes optional stack overflow detection, see:
+ * http://www.freertos.org/Stacks-and-stack-overflow-checking.html. */
+#define ipconfigIP_TASK_STACK_SIZE_WORDS           ( configMINIMAL_STACK_SIZE * 5 )
+
+/* ipconfigRAND32() is called by the IP stack to generate random numbers for
+ * things such as a DHCP transaction number or initial sequence number.  Random
+ * number generation is performed via this macro to allow applications to use their
+ * own random number generation method.  For example, it might be possible to
+ * generate a random number by sampling noise on an analogue input. */
+extern uint32_t ulRand();
+#define ipconfigRAND32()    ulRand()
+
+/* If ipconfigUSE_NETWORK_EVENT_HOOK is set to 1 then FreeRTOS+TCP will call the
+ * network event hook at the appropriate times.  If ipconfigUSE_NETWORK_EVENT_HOOK
+ * is not set to 1 then the network event hook will never be called. See:
+ * http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_UDP/API/vApplicationIPNetworkEventHook.shtml.
+ */
+#define ipconfigUSE_NETWORK_EVENT_HOOK           1
+
+/* Sockets have a send block time attribute.  If FreeRTOS_sendto() is called but
+ * a network buffer cannot be obtained then the calling task is held in the Blocked
+ * state (so other tasks can continue to executed) until either a network buffer
+ * becomes available or the send block time expires.  If the send block time expires
+ * then the send operation is aborted.  The maximum allowable send block time is
+ * capped to the value set by ipconfigMAX_SEND_BLOCK_TIME_TICKS.  Capping the
+ * maximum allowable send block time prevents prevents a deadlock occurring when
+ * all the network buffers are in use and the tasks that process (and subsequently
+ * free) the network buffers are themselves blocked waiting for a network buffer.
+ * ipconfigMAX_SEND_BLOCK_TIME_TICKS is specified in RTOS ticks.  A time in
+ * milliseconds can be converted to a time in ticks by dividing the time in
+ * milliseconds by portTICK_PERIOD_MS. */
+#define ipconfigUDP_MAX_SEND_BLOCK_TIME_TICKS    ( 5000 / portTICK_PERIOD_MS )
+
+/* If ipconfigUSE_DHCP is 1 then FreeRTOS+TCP will attempt to retrieve an IP
+ * address, netmask, DNS server address and gateway address from a DHCP server.  If
+ * ipconfigUSE_DHCP is 0 then FreeRTOS+TCP will use a static IP address.  The
+ * stack will revert to using the static IP address even when ipconfigUSE_DHCP is
+ * set to 1 if a valid configuration cannot be obtained from a DHCP server for any
+ * reason.  The static configuration used is that passed into the stack by the
+ * FreeRTOS_IPInit() function call. */
+#define ipconfigUSE_DHCP                         1
+#define ipconfigDHCP_REGISTER_HOSTNAME           1
+#define ipconfigDHCP_USES_UNICAST                1
+
+/* If ipconfigDHCP_USES_USER_HOOK is set to 1 then the application writer must
+ * provide an implementation of the DHCP callback function,
+ * xApplicationDHCPUserHook(). */
+#define ipconfigUSE_DHCP_HOOK                    0
+
+/* When ipconfigUSE_DHCP is set to 1, DHCP requests will be sent out at
+ * increasing time intervals until either a reply is received from a DHCP server
+ * and accepted, or the interval between transmissions reaches
+ * ipconfigMAXIMUM_DISCOVER_TX_PERIOD.  The IP stack will revert to using the
+ * static IP address passed as a parameter to FreeRTOS_IPInit() if the
+ * re-transmission time interval reaches ipconfigMAXIMUM_DISCOVER_TX_PERIOD without
+ * a DHCP reply being received. */
+#define ipconfigMAXIMUM_DISCOVER_TX_PERIOD \
+    ( 120000 / portTICK_PERIOD_MS )
+
+/* The ARP cache is a table that maps IP addresses to MAC addresses.  The IP
+ * stack can only send a UDP message to a remove IP address if it knowns the MAC
+ * address associated with the IP address, or the MAC address of the router used to
+ * contact the remote IP address.  When a UDP message is received from a remote IP
+ * address the MAC address and IP address are added to the ARP cache.  When a UDP
+ * message is sent to a remote IP address that does not already appear in the ARP
+ * cache then the UDP message is replaced by a ARP message that solicits the
+ * required MAC address information.  ipconfigARP_CACHE_ENTRIES defines the maximum
+ * number of entries that can exist in the ARP table at any one time. */
+#define ipconfigARP_CACHE_ENTRIES                 6
+
+/* ARP requests that do not result in an ARP response will be re-transmitted a
+ * maximum of ipconfigMAX_ARP_RETRANSMISSIONS times before the ARP request is
+ * aborted. */
+#define ipconfigMAX_ARP_RETRANSMISSIONS           ( 5 )
+
+/* ipconfigMAX_ARP_AGE defines the maximum time between an entry in the ARP
+ * table being created or refreshed and the entry being removed because it is stale.
+ * New ARP requests are sent for ARP cache entries that are nearing their maximum
+ * age.  ipconfigMAX_ARP_AGE is specified in tens of seconds, so a value of 150 is
+ * equal to 1500 seconds (or 25 minutes). */
+#define ipconfigMAX_ARP_AGE                       150
+
+/* Implementing FreeRTOS_inet_addr() necessitates the use of string handling
+ * routines, which are relatively large.  To save code space the full
+ * FreeRTOS_inet_addr() implementation is made optional, and a smaller and faster
+ * alternative called FreeRTOS_inet_addr_quick() is provided.  FreeRTOS_inet_addr()
+ * takes an IP in decimal dot format (for example, "192.168.0.1") as its parameter.
+ * FreeRTOS_inet_addr_quick() takes an IP address as four separate numerical octets
+ * (for example, 192, 168, 0, 1) as its parameters.  If
+ * ipconfigINCLUDE_FULL_INET_ADDR is set to 1 then both FreeRTOS_inet_addr() and
+ * FreeRTOS_indet_addr_quick() are available.  If ipconfigINCLUDE_FULL_INET_ADDR is
+ * not set to 1 then only FreeRTOS_indet_addr_quick() is available. */
+#define ipconfigINCLUDE_FULL_INET_ADDR            1
+
+/* ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS defines the total number of network buffer that
+ * are available to the IP stack.  The total number of network buffers is limited
+ * to ensure the total amount of RAM that can be consumed by the IP stack is capped
+ * to a pre-determinable value. */
+#define ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS    60
+
+/* A FreeRTOS queue is used to send events from application tasks to the IP
+ * stack.  ipconfigEVENT_QUEUE_LENGTH sets the maximum number of events that can
+ * be queued for processing at any one time.  The event queue must be a minimum of
+ * 5 greater than the total number of network buffers. */
+#define ipconfigEVENT_QUEUE_LENGTH \
+    ( ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS + 5 )
+
+/* The address of a socket is the combination of its IP address and its port
+ * number.  FreeRTOS_bind() is used to manually allocate a port number to a socket
+ * (to 'bind' the socket to a port), but manual binding is not normally necessary
+ * for client sockets (those sockets that initiate outgoing connections rather than
+ * wait for incoming connections on a known port number).  If
+ * ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND is set to 1 then calling
+ * FreeRTOS_sendto() on a socket that has not yet been bound will result in the IP
+ * stack automatically binding the socket to a port number from the range
+ * socketAUTO_PORT_ALLOCATION_START_NUMBER to 0xffff.  If
+ * ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND is set to 0 then calling FreeRTOS_sendto()
+ * on a socket that has not yet been bound will result in the send operation being
+ * aborted. */
+#define ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND         1
+
+/* Defines the Time To Live (TTL) values used in outgoing UDP packets. */
+#define ipconfigUDP_TIME_TO_LIVE                       128
+/* Also defined in FreeRTOSIPConfigDefaults.h. */
+#define ipconfigTCP_TIME_TO_LIVE                       128
+
+/* USE_TCP: Use TCP and all its features. */
+#define ipconfigUSE_TCP                                ( 1 )
+
+/* USE_WIN: Let TCP use windowing mechanism. */
+#define ipconfigUSE_TCP_WIN                            ( 1 )
+
+/* The MTU is the maximum number of bytes the payload of a network frame can
+ * contain.  For normal Ethernet V2 frames the maximum MTU is 1500.  Setting a
+ * lower value can save RAM, depending on the buffer management scheme used.  If
+ * ipconfigCAN_FRAGMENT_OUTGOING_PACKETS is 1 then (ipconfigNETWORK_MTU - 28) must
+ * be divisible by 8. */
+#define ipconfigNETWORK_MTU                            1200
+
+/* Set ipconfigUSE_DNS to 1 to include a basic DNS client/resolver.  DNS is used
+ * through the FreeRTOS_gethostbyname() API function. */
+#define ipconfigUSE_DNS                                1
+
+/* If ipconfigREPLY_TO_INCOMING_PINGS is set to 1 then the IP stack will
+ * generate replies to incoming ICMP echo (ping) requests. */
+#define ipconfigREPLY_TO_INCOMING_PINGS                1
+
+/* If ipconfigSUPPORT_OUTGOING_PINGS is set to 1 then the
+ * FreeRTOS_SendPingRequest() API function is available. */
+#define ipconfigSUPPORT_OUTGOING_PINGS                 0
+
+/* If ipconfigSUPPORT_SELECT_FUNCTION is set to 1 then the FreeRTOS_select()
+ * (and associated) API function is available. */
+#define ipconfigSUPPORT_SELECT_FUNCTION                0
+
+/* If ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES is set to 1 then Ethernet frames
+ * that are not in Ethernet II format will be dropped.  This option is included for
+ * potential future IP stack developments. */
+#define ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES      1
+
+/* If ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES is set to 1 then it is the
+ * responsibility of the Ethernet interface to filter out packets that are of no
+ * interest.  If the Ethernet interface does not implement this functionality, then
+ * set ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES to 0 to have the IP stack
+ * perform the filtering instead (it is much less efficient for the stack to do it
+ * because the packet will already have been passed into the stack).  If the
+ * Ethernet driver does all the necessary filtering in hardware then software
+ * filtering can be removed by using a value other than 1 or 0. */
+#define ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES    1
+
+/* The windows simulator cannot really simulate MAC interrupts, and needs to
+ * block occasionally to allow other tasks to run. */
+#define configWINDOWS_MAC_INTERRUPT_SIMULATOR_DELAY    ( 20 / portTICK_PERIOD_MS )
+
+/* Advanced only: in order to access 32-bit fields in the IP packets with
+ * 32-bit memory instructions, all packets will be stored 32-bit-aligned,
+ * plus 16-bits. This has to do with the contents of the IP-packets: all
+ * 32-bit fields are 32-bit-aligned, plus 16-bit. */
+#define ipconfigPACKET_FILLER_SIZE                     2
+
+/* Define the size of the pool of TCP window descriptors.  On the average, each
+ * TCP socket will use up to 2 x 6 descriptors, meaning that it can have 2 x 6
+ * outstanding packets (for Rx and Tx).  When using up to 10 TP sockets
+ * simultaneously, one could define TCP_WIN_SEG_COUNT as 120. */
+#define ipconfigTCP_WIN_SEG_COUNT                      240
+
+/* Each TCP socket has a circular buffers for Rx and Tx, which have a fixed
+ * maximum size.  Define the size of Rx buffer for TCP sockets. */
+#define ipconfigTCP_RX_BUFFER_LENGTH                   ( 10000 )
+
+/* Define the size of Tx buffer for TCP sockets. */
+#define ipconfigTCP_TX_BUFFER_LENGTH                   ( 10000 )
+
+/* When using call-back handlers, the driver may check if the handler points to
+ * real program memory (RAM or flash) or just has a random non-zero value. */
+#define ipconfigIS_VALID_PROG_ADDRESS( x )    ( ( x ) != NULL )
+
+/* Include support for TCP keep-alive messages. */
+#define ipconfigTCP_KEEP_ALIVE                   ( 1 )
+#define ipconfigTCP_KEEP_ALIVE_INTERVAL          ( 20 ) /* Seconds. */
+
+/* The socket semaphore is used to unblock the MQTT task. */
+#define ipconfigSOCKET_HAS_USER_SEMAPHORE        ( 0 )
+
+#define ipconfigSOCKET_HAS_USER_WAKE_CALLBACK    ( 1 )
+#define ipconfigUSE_CALLBACKS                    ( 0 )
+
+
+#define portINLINE                               __inline
+
+void vApplicationMQTTGetKeys( const char ** ppcRootCA,
+                              const char ** ppcClientCert,
+                              const char ** ppcClientPrivateKey );
+
+#endif /* FREERTOS_IP_CONFIG_H */
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/Makefile b/FreeRTOS-Plus/Test/CBMC/patches/Makefile
new file mode 100644
index 000000000..27888e63b
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/Makefile
@@ -0,0 +1,24 @@
+BRANCH=freertos
+
+PATCHED=patched
+
+default:
+	git format-patch $(BRANCH)..$(BRANCH)-cbmc-patches
+
+patch:
+	if [ ! -f $(PATCHED) ]; then \
+	  for p in *.patch; do \
+	    (cd ../../..; patch -p1 < CBMC/patches/$${p}) \
+	  done; \
+	  cat > $(PATCHED) < /dev/null; \
+	fi
+
+unpatch:
+	git checkout ../../../lib
+	$(RM) $(PATCHED)
+
+#patching file lib/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h
+#patching file lib/include/private/list.h
+#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DHCP.c
+#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c
+#patching file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_TCP_WIN.c
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/README.md b/FreeRTOS-Plus/Test/CBMC/patches/README.md
new file mode 100644
index 000000000..ec0e5d424
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/README.md
@@ -0,0 +1,6 @@
+This directory includes patches to FreeRTOS required to run the CBMC proofs.
+
+The patches fall into three classes:
+* First is a refactoring of prvCheckOptions
+* Second is the removal of static attributes from some functions
+* Third is two patches dealing with shortcomings of CBMC that should be removed soon.
\ No newline at end of file
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/__init__.py b/FreeRTOS-Plus/Test/CBMC/patches/__init__.py
new file mode 100755
index 000000000..e69de29bb
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/compute_patch.py b/FreeRTOS-Plus/Test/CBMC/patches/compute_patch.py
new file mode 100755
index 000000000..3e854177c
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/compute_patch.py
@@ -0,0 +1,241 @@
+#!/usr/bin/env python3
+#
+# Generation of patches for CBMC proofs.
+#
+# Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+
+import json
+import os
+import re
+import subprocess
+import textwrap
+import unittest
+
+from patches_constants import PATCHES_DIR
+from patches_constants import HEADERS
+
+
+DEFINE_REGEX_MAKEFILE = re.compile(r"(?:['\"])?([\w]+)")
+DEFINE_REGEX_HEADER = re.compile(r"\s*#\s*define\s*([\w]+)")
+
+class DirtyGitError(Exception):
+    pass
+
+class PatchCreationError(Exception):
+    pass
+
+def prolog():
+    return textwrap.dedent("""\
+        This script generates patch files for the header files used
+        in the cbmc proof. These patches permit setting values of preprocessor
+        macros as part of the proof configuration.
+    """)
+
+
+def find_all_defines():
+    """Collects all define values in Makefile.json.
+
+       Some of the Makefiles use # in the json to make comments.
+       As this is non standard json, we need to remove the comment
+       lines before parsing. Then we extract all defines from the file.
+    """
+    defines = set()
+
+    proof_dir = os.path.abspath(os.path.join(PATCHES_DIR, "..", "proofs"))
+
+    for fldr, _, fyles in os.walk(proof_dir):
+        if "Makefile.json" in fyles:
+            file = os.path.join(fldr, "Makefile.json")
+            key = "DEF"
+        elif "MakefileCommon.json" in fyles:
+            file = os.path.join(fldr, "MakefileCommon.json")
+            key = "DEF "
+        else:
+            continue
+        with open(file, "r") as source:
+            content = "".join([line for line in source
+                               if line and not line.strip().startswith("#")])
+            makefile = json.loads(content)
+            if key in makefile.keys():
+                """This regex parses the define declaration in Makefile.json
+                   'macro(x)=false' is an example for a declaration.
+                   'macro' is expected to be matched.
+                """
+                for define in makefile[key]:
+                    matched = DEFINE_REGEX_MAKEFILE.match(define)
+                    if matched:
+                        defines.add(matched.group(1))
+    return defines
+
+def manipulate_headerfile(defines, header_file):
+    """Wraps all defines used in an ifndef."""
+
+    # This regex matches the actual define in the header file.
+    modified_content = ""
+    with open(header_file, "r") as source:
+        last = ""
+        for line in source:
+            match = DEFINE_REGEX_HEADER.match(line)
+            if (match and
+                    match.group(1) in defines and
+                    not last.lstrip().startswith("#ifndef")):
+                full_def = line
+                # this loop deals with multiline definitions
+                while line.rstrip().endswith("\\"):
+                    line = next(source)
+                    full_def += line
+                # indentation for multiline definitions can be improved
+                modified_content += textwrap.dedent("""\
+                    #ifndef {target}
+                        {original}\
+                    #endif
+                    """.format(target=match.group(1), original=full_def))
+            else:
+                modified_content += line
+            last = line
+    with open(header_file, "w") as output:
+        output.write(modified_content)
+
+
+def header_dirty(header_files):
+    """Check that the header_file is not previously modified."""
+
+    # Git does not update the modified file list returned by diff-files on
+    # apply -R (at least not on MacOS).
+    # Running git status updates git's internal state.
+    status = subprocess.run(["git", "status"], stdout=subprocess.DEVNULL,
+                            stderr=subprocess.PIPE, universal_newlines=True)
+
+    diff_state = subprocess.run(["git", "diff-files"], stdout=subprocess.PIPE,
+                                stderr=subprocess.PIPE, universal_newlines=True)
+
+    if status.returncode:
+        raise DirtyGitError(textwrap.dedent("""\
+                Could not run git status. Exited: {}
+                stderr: {}
+                """.format(status.returncode, status.stderr)))
+
+    if diff_state.returncode:
+        raise DirtyGitError(textwrap.dedent("""\
+                Could not run git diff-files. Exited: {}
+                stderr: {}
+                """.format(diff_state.returncode, diff_state.stderr)))
+
+    for header_file in header_files:
+        if os.path.basename(header_file) + "\n" in diff_state.stdout:
+            return True
+    return False
+
+
+def create_patch(defines, header_file):
+    """Computes a patch enclosing defines used in CBMC proofs with #ifndef."""
+    manipulate_headerfile(defines, header_file)
+    patch = subprocess.run(["git", "diff", header_file],
+                           stdout=subprocess.PIPE,
+                           stderr=subprocess.PIPE, universal_newlines=True)
+    cleaned = subprocess.run(["git", "checkout", "--", header_file],
+                             stdout=subprocess.DEVNULL,
+                             stderr=subprocess.PIPE, universal_newlines=True)
+
+    if patch.returncode:
+        raise PatchCreationError(textwrap.dedent("""\
+                git diff exited with error code: {}
+                stderr: {}
+                """.format(patch.returncode, patch.stderr)))
+
+    if cleaned.returncode:
+        raise DirtyGitError(textwrap.dedent("""\
+                git checkout for cleaning files failed with error code: {}
+                on file {}
+                stderr: {}
+                """.format(cleaned.returncode, header_file, cleaned.stderr)))
+
+    header_path_part = header_file.replace(os.sep, "_")
+    path_name = "auto_patch_" + header_path_part + ".patch"
+    path_name = os.path.join(PATCHES_DIR, path_name)
+    if patch.stdout:
+        with open(path_name, "w") as patch_file:
+            patch_file.write(patch.stdout)
+
+
+def create_patches(headers):
+    defines = find_all_defines()
+
+    if not header_dirty(headers):
+        for header in headers:
+            create_patch(defines, header)
+    else:
+        raise DirtyGitError(textwrap.dedent("""\
+                It seems like one of the header files is in dirty state.
+                This script cannot patch files in dirty state.
+                """))
+
+# Invoke 'python3 -m unittest compute_patch.py" for running tests.
+class TestDefineRegexes(unittest.TestCase):
+    def test_makefile_regex(self):
+        input1 = "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}"
+        input2 = "ipconfigETHERNET_MINIMUM_PACKET_BYTES=50"
+        input3 = "'configASSERT(X)=__CPROVER_assert(x, \"must hold\")'"
+        input4 = '"configASSERT (X)=__CPROVER_assert(x, "must hold")"'
+        input5 = "configASSERT(X)=__CPROVER_assert(x,\"must hold\")"
+
+        match1 = DEFINE_REGEX_MAKEFILE.match(input1)
+        match2 = DEFINE_REGEX_MAKEFILE.match(input2)
+        match3 = DEFINE_REGEX_MAKEFILE.match(input3)
+        match4 = DEFINE_REGEX_MAKEFILE.match(input4)
+        match5 = DEFINE_REGEX_MAKEFILE.match(input5)
+
+        self.assertIsNotNone(match1)
+        self.assertIsNotNone(match2)
+        self.assertIsNotNone(match3)
+        self.assertIsNotNone(match4)
+        self.assertIsNotNone(match5)
+
+        self.assertEqual(match1.group(1),
+                         "ipconfigETHERNET_MINIMUM_PACKET_BYTES")
+        self.assertEqual(match2.group(1),
+                         "ipconfigETHERNET_MINIMUM_PACKET_BYTES")
+        self.assertEqual(match3.group(1), "configASSERT")
+        self.assertEqual(match4.group(1), "configASSERT")
+        self.assertEqual(match5.group(1), "configASSERT")
+
+
+    def test_header_regex(self):
+        input1 = ("#define configASSERT( x )    if( ( x ) == 0 )" +
+                  "vAssertCalled( __FILE__, __LINE__ )")
+        input2 = "#define ipconfigMAX_ARP_RETRANSMISSIONS           ( 5 )"
+        input3 = "#define ipconfigINCLUDE_FULL_INET_ADDR            1"
+
+        match1 = DEFINE_REGEX_HEADER.match(input1)
+        match2 = DEFINE_REGEX_HEADER.match(input2)
+        match3 = DEFINE_REGEX_HEADER.match(input3)
+
+        self.assertIsNotNone(match1)
+        self.assertIsNotNone(match2)
+        self.assertIsNotNone(match3)
+
+        self.assertEqual(match1.group(1), "configASSERT")
+        self.assertEqual(match2.group(1), "ipconfigMAX_ARP_RETRANSMISSIONS")
+        self.assertEqual(match3.group(1), "ipconfigINCLUDE_FULL_INET_ADDR")
+
+if __name__ == '__main__':
+    create_patches(HEADERS)
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/patch.py b/FreeRTOS-Plus/Test/CBMC/patches/patch.py
new file mode 100755
index 000000000..c2c0883a3
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/patch.py
@@ -0,0 +1,36 @@
+#!/usr/bin/env python3
+
+import logging
+import os
+import subprocess
+import sys
+from glob import glob
+
+from patches_constants import PATCHES_DIR
+
+def patch():
+    if os.path.isfile("patched"):
+        sys.exit()
+
+    applied_patches = []
+    failed_patches = []
+    for tmpfile in glob(os.path.join(PATCHES_DIR, "*.patch")):
+        print("patch", tmpfile)
+        result = subprocess.run(["git", "apply", "--ignore-space-change", "--ignore-whitespace", tmpfile],
+                                cwd=os.path.join("..", "..", "..", ".."))
+        if result.returncode:
+            failed_patches.append(tmpfile)
+            logging.error("patching failed: %s", tmpfile)
+        else:
+            applied_patches.append(tmpfile)
+
+    with open(os.path.join(PATCHES_DIR, "patched"), "w") as outp:
+        print("Success:", file=outp)
+        print("\n".join(map(lambda x: "\t" + x, applied_patches)), file=outp)
+
+        print("Failure:", file=outp)
+        print("\n".join(map(lambda x: "\t" + x, failed_patches)), file=outp)
+
+
+if __name__ == "__main__":
+    patch()
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/patches_constants.py b/FreeRTOS-Plus/Test/CBMC/patches/patches_constants.py
new file mode 100755
index 000000000..1093e6538
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/patches_constants.py
@@ -0,0 +1,42 @@
+#!/usr/bin/env python3
+#
+# Constants for the generation of patches for CBMC proofs.
+#
+# Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+import os
+
+PATCHES_DIR = os.path.dirname(os.path.abspath(__file__))
+
+
+shared_prefix = [
+    "."
+]
+shared_prefix_port = [
+    "..", "..", "..", "..", "FreeRTOS", "Source", "portable", "MSVC-MingW"
+]
+
+absolute_prefix = os.path.abspath(os.path.join(PATCHES_DIR, *shared_prefix))
+absolute_prefix_port = os.path.abspath(os.path.join(PATCHES_DIR, *shared_prefix_port))
+
+HEADERS = [os.path.join(absolute_prefix, "FreeRTOSConfig.h"),
+		   os.path.join(absolute_prefix, "FreeRTOSIPConfig.h"),
+           os.path.join(absolute_prefix_port, "portmacro.h")]
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/unpatch.py b/FreeRTOS-Plus/Test/CBMC/patches/unpatch.py
new file mode 100755
index 000000000..2162971fd
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/patches/unpatch.py
@@ -0,0 +1,42 @@
+#!/usr/bin/env python3
+#
+# unpatching changes for the CBMC proofs.
+#
+# Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+import subprocess
+import os
+import sys
+from glob import glob
+
+from patches_constants import PATCHES_DIR
+
+try:
+    os.remove(os.path.join(PATCHES_DIR, "patched"))
+except FileNotFoundError:
+    print("Nothing to do here.")
+    sys.exit(0)
+for tmpfile in glob(os.path.join(PATCHES_DIR, "*.patch")):
+    print("unpatch", tmpfile)
+    result = subprocess.run(["git", "apply", "-R", "--ignore-space-change", "--ignore-whitespace", tmpfile],
+                            cwd=os.path.join("..", "..", "..", ".."))
+    if result.returncode:
+        print("Unpatching failed: {}".format(tmpfile))
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/.gitignore b/FreeRTOS-Plus/Test/CBMC/proofs/.gitignore
new file mode 100644
index 000000000..3498c4b3b
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/.gitignore
@@ -0,0 +1,10 @@
+# These files are generated by make_type_header_files.py
+*_datastructure.h
+
+Makefile
+Makefile.common
+cbmc-batch.yaml
+**/*.txt
+**/*.goto
+
+!CMakeLists.txt
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c b/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c
new file mode 100644
index 000000000..3fe245f80
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.c
@@ -0,0 +1,47 @@
+#include "FreeRTOS.h"
+#include "task.h"
+#include "tasksStubs.h"
+
+#ifndef TASK_STUB_COUNTER
+	#define TASK_STUB_COUNTER 0;
+#endif
+
+/* 5 is a magic number, but we need some number here as a default value.
+   This value is used to bound any loop depending on xTaskCheckForTimeOut
+   as a loop bound. It should be overwritten in the Makefile.json adapting
+   to the performance requirements of the harness. */
+#ifndef TASK_STUB_COUNTER_LIMIT
+	#define TASK_STUB_COUNTER_LIMIT 5;
+#endif
+
+
+static BaseType_t xCounter = TASK_STUB_COUNTER;
+static BaseType_t xCounterLimit = TASK_STUB_COUNTER_LIMIT;
+
+BaseType_t xTaskGetSchedulerState( void )
+{
+	return xState;
+}
+
+/* This function is another method apart from overwritting the defines to init the max
+   loop bound. */
+void vInitTaskCheckForTimeOut(BaseType_t maxCounter, BaseType_t maxCounter_limit)
+{
+	xCounter = maxCounter;
+	xCounterLimit = maxCounter_limit;
+}
+
+/* This is mostly called in a loop. For CBMC, we have to bound the loop
+   to a max limits of calls. Therefore this Stub models a nondet timeout in
+   max TASK_STUB_COUNTER_LIMIT iterations.*/
+BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait ) {
+	++xCounter;
+	if(xCounter == xCounterLimit)
+	{
+		return pdTRUE;
+	}
+	else
+	{
+		return nondet_basetype();
+	}
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/CMakeLists.txt b/FreeRTOS-Plus/Test/CBMC/proofs/CMakeLists.txt
new file mode 100644
index 000000000..aaa2e3c8a
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/CMakeLists.txt
@@ -0,0 +1,40 @@
+list(APPEND cbmc_compile_options
+    -m32
+)
+
+list(APPEND cbmc_compile_definitions
+    CBMC
+    WINVER=0x400
+    _CONSOLE
+    _CRT_SECURE_NO_WARNINGS
+    _DEBUG
+    _WIN32_WINNT=0x0500
+    __PRETTY_FUNCTION__=__FUNCTION__
+    __free_rtos__
+)
+
+list(APPEND cbmc_compile_includes
+    ${CMAKE_SOURCE_DIR}/Source/include
+    ${CMAKE_SOURCE_DIR}/Source/portable/MSVC-MingW
+	${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement
+	${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include    
+    ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/Compiler/MSVC
+    ${cbmc_dir}/include
+    ${cbmc_dir}/windows
+)
+
+# Remove --flag for a specific proof with list(REMOVE_ITEM cbmc_flags --flag)
+list(APPEND cbmc_flags
+    --32
+    --bounds-check
+    --pointer-check
+    --div-by-zero-check
+    --float-overflow-check
+    --nan-check
+    --nondet-static
+    --pointer-overflow-check
+    --signed-overflow-check
+    --undefined-shift-check
+    --unsigned-overflow-check
+)
+
diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptions/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/CheckOptions/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/CheckOptions/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptionsInner/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/CheckOptionsInner/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsInner/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/DHCP/DHCPProcess/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSclear/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSclear/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSclear/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/Makefile.template b/FreeRTOS-Plus/Test/CBMC/proofs/Makefile.template
new file mode 100644
index 000000000..fa727023c
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/Makefile.template
@@ -0,0 +1,161 @@
+default: cbmc
+
+# ____________________________________________________________________
+# CBMC binaries
+#
+
+GOTO_CC = @GOTO_CC@
+GOTO_INSTRUMENT = goto-instrument
+GOTO_ANALYZER = goto-analyzer
+VIEWER = cbmc-viewer
+
+# ____________________________________________________________________
+# Variables
+#
+# Naming scheme:
+# ``````````````
+# FOO is the concatenation of the following:
+# FOO2: Set of command line
+# C_FOO: Value of $FOO common to all harnesses, set in this file
+# O_FOO: Value of $FOO specific to the OS we're running on, set in the
+#        makefile for the operating system
+# H_FOO: Value of $FOO specific to a particular harness, set in the
+#        makefile for that harness
+
+ENTRY = $(H_ENTRY)
+OBJS = $(H_OBJS)
+
+INC = \
+  $(INC2) \
+  $(C_INC) $(O_INC) $(H_INC) \
+  # empty
+
+CFLAGS = \
+  $(CFLAGS2) \
+  $(C_DEF) $(O_DEF) $(H_DEF) $(DEF) \
+  $(C_OPT) $(O_OPT) $(H_OPT) $(OPT) \
+  -m32 \
+  # empty
+
+CBMCFLAGS = \
+  $(CBMCFLAGS2) \
+  $(C_CBMCFLAGS) $(O_CBMCFLAGS) $(H_CBMCFLAGS) \
+  # empty
+
+INSTFLAGS = \
+  $(INSTFLAGS2) \
+  $(C_INSTFLAGS) $(O_INSTFLAGS) $(H_INSTFLAGS) \
+  # empty
+
+# ____________________________________________________________________
+# Rules
+#
+# Rules for building a:FR object files. These are not harness-specific,
+# and several harnesses might depend on a particular a:FR object, so
+# define them all once here.
+
+@RULE_GOTO@
+	$(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@
+
+# ____________________________________________________________________
+# Rules
+#
+# Rules for patching
+
+patch:
+	cd $(PROOFS)/../patches && ./patch.py
+
+unpatch:
+	cd $(PROOFS)/../patches && ./unpatch.py
+
+# ____________________________________________________________________
+# Rules
+#
+# Rules for building the CBMC harness
+
+queue_datastructure.h: $(H_OBJS_EXCEPT_HARNESS)
+	python3 @TYPE_HEADER_SCRIPT@ --binary $(FREERTOS)/Source/queue.goto --c-file $(FREERTOS)/Source/queue.c
+
+$(ENTRY)_harness.goto: $(ENTRY)_harness.c $(H_GENERATE_HEADER)
+	$(GOTO_CC) @COMPILE_ONLY@ @RULE_OUTPUT@ $(INC) $(CFLAGS) @RULE_INPUT@
+
+$(ENTRY)1.goto: $(OBJS)
+	$(GOTO_CC) @COMPILE_LINK@ @RULE_OUTPUT@ --function harness $(OBJS)
+
+$(ENTRY)2.goto: $(ENTRY)1.goto
+	 $(GOTO_INSTRUMENT) --add-library @RULE_INPUT@ @RULE_OUTPUT@ \
+		> $(ENTRY)2.txt 2>&1
+
+$(ENTRY)3.goto: $(ENTRY)2.goto
+	$(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \
+		> $(ENTRY)3.txt 2>&1
+
+$(ENTRY)4.goto: $(ENTRY)3.goto
+	$(GOTO_INSTRUMENT) $(INSTFLAGS) --slice-global-inits @RULE_INPUT@ @RULE_OUTPUT@ \
+		> $(ENTRY)4.txt 2>&1
+# ____________________________________________________________________
+# After running goto-instrument to remove function bodies the unused
+# functions need to be dropped again.
+
+$(ENTRY)5.goto: $(ENTRY)4.goto
+	$(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \
+		> $(ENTRY)5.txt 2>&1
+
+$(ENTRY).goto: $(ENTRY)5.goto
+	@CP@ @RULE_INPUT@ @RULE_OUTPUT@
+
+# ____________________________________________________________________
+# Rules
+#
+# Rules for running CBMC
+
+goto:
+	$(MAKE) patch
+	$(MAKE) $(ENTRY).goto
+
+cbmc.txt: $(ENTRY).goto
+	cbmc $(CBMCFLAGS) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1
+
+property.xml: $(ENTRY).goto
+	cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ \
+	  2>&1 > $@
+
+coverage.xml: $(ENTRY).goto
+	cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ 2>&1 > $@
+
+cbmc: cbmc.txt
+
+property: property.xml
+
+coverage: coverage.xml
+
+report: cbmc.txt property.xml coverage.xml
+	$(VIEWER) \
+	--goto $(ENTRY).goto \
+	--srcdir $(FREERTOS) \
+	--blddir $(FREERTOS) \
+	--htmldir html \
+	--srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \
+	--result cbmc.txt \
+	--property property.xml \
+	--block coverage.xml
+
+# ____________________________________________________________________
+# Rules
+#
+# Rules for cleaning up
+
+clean:
+	@RM@ $(OBJS) $(ENTRY).goto
+	@RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt
+	@RM@ cbmc.txt property.xml coverage.xml TAGS
+	@RM@ *~ \#*
+	@RM@ queue_datastructure.h
+
+
+veryclean: clean
+	@RM_RECURSIVE@ html
+
+distclean: veryclean
+	cd $(PROOFS)/../patches && ./unpatch.py
+	cd $(PROOFS) && ./make-remove-makefiles.py
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json
new file mode 100644
index 000000000..a71bb7fab
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json
@@ -0,0 +1,41 @@
+{
+    "FREERTOS": [ " ../../../../FreeRTOS" ],
+    "PROOFS": [ "." ],
+
+    "DEF ": [
+	"_DEBUG",
+	"__free_rtos__",
+	"_CONSOLE",
+	"_WIN32_WINNT=0x0500",
+	"WINVER=0x400",
+	"_CRT_SECURE_NO_WARNINGS",
+	"__PRETTY_FUNCTION__=__FUNCTION__",
+	"'configASSERT(X)=__CPROVER_assert(X,\"Assertion Error\")'",
+    "'configPRECONDITION(X)=__CPROVER_assume(X)'"
+    ],
+
+    "INC ": [
+	"$(FREERTOS)/Source/include",
+	"$(FREERTOS)/Source/portable/MSVC-MingW",
+	"$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include",
+	"$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement",
+	"$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/Compiler/MSVC",
+	"$(FREERTOS)/../FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Minimal_Windows_Simulator/WinPCap",
+	"$(FREERTOS)/Demo/Common/include",
+	"$(FREERTOS)/Test/CBMC/include",
+	"$(FREERTOS)/Test/CBMC/patches"
+    ],
+
+    "CBMCFLAGS ": [
+	"--object-bits 7",
+	"--32",
+	"--bounds-check",
+	"--pointer-check"
+    ],
+
+    "FORWARD_SLASH": ["/"],
+
+    "TYPE_HEADERS": [
+        "$(FREERTOS)/Source/queue.c"
+    ]
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileLinux.json b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileLinux.json
new file mode 100644
index 000000000..08442a2ab
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileLinux.json
@@ -0,0 +1,36 @@
+{
+    "GOTO_CC": [
+	"goto-cc"
+    ],
+    "COMPILE_LINK": [
+	"-o"
+    ],
+    "COMPILE_ONLY": [
+	"-c",
+	"-o"
+    ],
+    "RULE_INPUT": [
+	"$<"
+    ],
+    "RULE_OUTPUT": [
+	"$@"
+    ],
+    "RULE_GOTO": [
+	"%.goto : %.c"
+    ],
+    "INC": [
+	"$(PROOFS)/../windows"
+    ],
+    "RM": [
+	"$(RM)"
+    ],
+    "RM_RECURSIVE": [
+	"$(RM) -r"
+    ],
+    "CP": [
+	"cp"
+    ],
+    "TYPE_HEADER_SCRIPT": [
+      "$(PROOFS)/make_type_header_files.py"
+    ]
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileWindows.json b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileWindows.json
new file mode 100644
index 000000000..543dd6219
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileWindows.json
@@ -0,0 +1,44 @@
+{
+    "DEF": [
+	"WIN32"
+    ],
+    "GOTO_CC": [
+	"goto-cl"
+    ],
+    "COMPILE_LINK": [
+	"/Fe"
+    ],
+    "COMPILE_ONLY": [
+	"/c",
+	"/Fo"
+    ],
+    "RULE_INPUT": [
+	"$**"
+    ],
+    "RULE_OUTPUT": [
+	"$@"
+    ],
+    "RULE_GOTO": [
+	".c.goto:"
+    ],
+    "OPT": [
+	"/wd4210",
+	"/wd4127",
+	"/wd4214",
+	"/wd4201",
+	"/wd4244",
+	"/wd4310"
+    ],
+    "RM": [
+	"del"
+    ],
+    "RM_RECURSIVE": [
+	"del /s"
+    ],
+    "CP": [
+	"copy"
+    ],
+    "TYPE_HEADER_SCRIPT": [
+    "$(PROOFS)\\make_type_header_files.py"
+    ]
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/Makefile.json
new file mode 100644
index 000000000..cb6fe7fae
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/Makefile.json
@@ -0,0 +1,60 @@
+# The proof depends on one parameter:
+#   NETWORK_BUFFER_SIZE is the size of the network buffer being parsed
+# The buffer size must be bounded because we must bound the number of
+# iterations loops iterating over the buffer.
+
+{
+  "ENTRY": "ParseDNSReply",
+
+################################################################
+# This is the network buffer size.
+# Reasonable values are size > 12 = sizeof(xDNSMessage)
+  "NETWORK_BUFFER_SIZE": 40,
+
+################################################################
+# Loop prvParseDNSReply.0:
+# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 915
+  "PARSELOOP0": "prvParseDNSReply.0",
+
+# M = sizeof( DNSMessage_t ) = 12
+# U = sizeof( uint32_t) = 4
+# Loop bound is (NETWORK_BUFFER_SIZE - M) div (U+1) + 1 tight for SIZE >= M
+# Loop bound is 1 for 0 <= SIZE < M
+  "PARSELOOP0_UNWIND":
+    "__eval 1 if {NETWORK_BUFFER_SIZE} < 12 else ({NETWORK_BUFFER_SIZE} - 12) / 5 + 1",
+
+################################################################
+# Loop prvParseDNSReply.1:
+# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 989
+  "PARSELOOP1": "prvParseDNSReply.1",
+
+# A = sizeof( DNSAnswerRecord_t ) = 10
+# M = sizeof( DNSMessage_t ) = 12
+# U = sizeof( uint32_t) = 4
+# Loop bound is (NETWORK_BUFFER_SIZE - M - A) div (A+1) + A + 1 tight
+#    for SIZE >= M + A
+# Loop bound is (NETWORK_BUFFER_SIZE - M) + 1 for M <= SIZE < M + A
+# Loop bound is 1 for 0 <= SIZE < M
+  "PARSELOOP1_UNWIND":
+    "__eval 1 if {NETWORK_BUFFER_SIZE} < 12 else ({NETWORK_BUFFER_SIZE} - 11 if {NETWORK_BUFFER_SIZE} < 22 else ({NETWORK_BUFFER_SIZE} - 12 - 10) / 11 + 11)",
+
+################################################################
+
+  "CBMCFLAGS":
+  [
+    "--unwind 1",
+    "--unwindset {PARSELOOP0}:{PARSELOOP0_UNWIND},{PARSELOOP1}:{PARSELOOP1_UNWIND},prvProcessDNSCache.0:5"
+  ],
+
+  "OBJS":
+  [
+    "$(ENTRY)_harness.goto",
+    "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto",
+    "$(FREERTOS)/Source/tasks.goto"
+  ],
+
+  "DEF":
+  [
+    "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}"
+  ]
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c
new file mode 100644
index 000000000..7b55c9e8a
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ParseDNSReply/ParseDNSReply_harness.c
@@ -0,0 +1,165 @@
+/* Standard includes. */
+#include <stdint.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "task.h"
+#include "queue.h"
+#include "list.h"
+#include "semphr.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_Sockets.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_UDP_IP.h"
+#include "FreeRTOS_DNS.h"
+#include "NetworkBufferManagement.h"
+#include "NetworkInterface.h"
+#include "IPTraceMacroDefaults.h"
+
+#include "cbmc.h"
+
+uint32_t prvParseDNSReply(uint8_t *pucUDPPayloadBuffer,
+			  size_t xBufferLength,
+			  TickType_t xIdentifier);
+
+// Used in specification and abstraction of prvReadNameField, prvSkipNameField
+// Given unconstrained values in harness
+uint8_t *buffer;
+size_t buffer_size;
+
+// Abstraction of prvReadNameField
+uint8_t *prvReadNameField(uint8_t *pucByte,
+			  size_t xSourceLen,
+			  char *pcName,
+			  size_t xDestLen){
+
+  // Preconditions
+
+  // pointers are valid pointers into buffers
+  __CPROVER_assert(xSourceLen == 0 ||
+		   (buffer <= pucByte && pucByte < buffer + buffer_size),
+		   "pucByte valid pointer");
+  //  __CPROVER_assume(name <= pcName && pcName < name + name_size);
+  (void) *(pcName); // can only test for valid pointer
+
+  // lengths are valid values for space remaining in the buffers
+  __CPROVER_assert(pucByte + xSourceLen <= buffer + buffer_size,
+		   "xSourceLen valid length");
+  //  __CPROVER_assume(pcName + xDestLen <= name + name_size);
+  (void) *(pcName + (xDestLen-1)); // can only test for valid pointer
+
+  // CBMC loop unwinding: bounds depend on xSourceLen and xDestLen
+  __CPROVER_assert(xSourceLen <= NETWORK_BUFFER_SIZE,
+		   "xSourceLen loop unwinding");
+  //  __CPROVER_assume(xDestLen <= NAME_SIZE);
+
+  // Buffer overflow from integer overflow in expression len < xDestLen-1
+  // xDestLen == 254 in code
+  __CPROVER_assert(xDestLen > 0, "xDestLen nonzero");
+
+  SAVE_OLDVAL(pucByte, uint8_t *);
+  SAVE_OLDVAL(pcName, char *);
+  SAVE_OLDVAL(xSourceLen, size_t);
+  SAVE_OLDVAL(xDestLen, size_t);
+
+  // Function body
+  char bit;
+  size_t offset;
+  uint8_t *rc = bit ? pucByte + offset : 0;
+  __CPROVER_assume(offset <= NETWORK_BUFFER_SIZE);
+
+  // Postconditions
+  __CPROVER_assume((rc == 0) ||
+		   (rc - OLDVAL(pucByte) >= 1 &&
+		    rc - OLDVAL(pucByte) <= OLDVAL(xSourceLen) &&
+		    rc - OLDVAL(pucByte) <= OLDVAL(xDestLen)+2 &&
+		    pucByte == OLDVAL(pucByte) &&
+		    pcName == OLDVAL(pcName) &&
+		    buffer <= rc && rc <= buffer + buffer_size));
+
+  return rc;
+}
+
+// Abstraction of prvSkipNameField
+uint8_t *prvSkipNameField( uint8_t *pucByte, size_t xSourceLen ){
+
+  // Preconditions
+
+  // pointer is valid pointer into buffer
+  __CPROVER_assert(xSourceLen == 0 ||
+		   (buffer <= pucByte && pucByte < buffer + buffer_size),
+		   "pucByte valid pointer");
+
+  // length is valid value for space remaining in the buffer
+  __CPROVER_assert(pucByte + xSourceLen <= buffer + buffer_size,
+		   "xSourceLen valid length");
+
+  // CBMC loop unwinding: bound depend on xSourceLen
+  __CPROVER_assert(xSourceLen <= NETWORK_BUFFER_SIZE,
+		   "xSourceLen loop unwinding");
+
+  SAVE_OLDVAL(pucByte, uint8_t *);
+  SAVE_OLDVAL(xSourceLen, size_t);
+
+  // Function body
+  char bit;
+  size_t offset;
+  uint8_t *rc = bit ? pucByte + offset : 0;
+  __CPROVER_assume(offset <= NETWORK_BUFFER_SIZE);
+
+  // Postconditions
+  __CPROVER_assume((rc == 0) ||
+		   (rc - OLDVAL(pucByte) >= 1 &&
+		    rc - OLDVAL(pucByte) <= OLDVAL(xSourceLen) &&
+		    pucByte == OLDVAL(pucByte) &&
+		    buffer <= rc && rc <= buffer + buffer_size));
+
+  return rc;
+
+}
+
+void harness() {
+
+  // Choose arbitrary buffer of size at most NETWORK_BUFFER_SIZE
+  uint8_t my_buffer[NETWORK_BUFFER_SIZE];
+  size_t my_buffer_offset;
+  buffer = my_buffer + my_buffer_offset;
+  buffer_size = NETWORK_BUFFER_SIZE - my_buffer_offset;
+  __CPROVER_assume(my_buffer_offset <= NETWORK_BUFFER_SIZE);
+
+  __CPROVER_havoc_object(my_buffer);
+
+  // Choose arbitrary pointer into the buffer
+  size_t buffer_offset;
+  uint8_t *pucUDPPayloadBuffer = buffer + buffer_offset;
+
+  // Choose arbitrary value for space remaining in the buffer
+  size_t xBufferLength;
+
+  // Choose arbitrary identifier
+  TickType_t xIdentifier;
+
+  ////////////////////////////////////////////////////////////////
+  // Specification and proof of prvReadNameField
+
+  // CBMC pointer model (this is obviously true)
+  __CPROVER_assume(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE);
+
+  // Preconditions
+
+  // pointer is valid pointer into buffer
+  __CPROVER_assume(buffer <= pucUDPPayloadBuffer &&
+		   pucUDPPayloadBuffer < buffer + buffer_size);
+
+  // length is valid value for space remaining in the buffer
+  __CPROVER_assume(pucUDPPayloadBuffer + xBufferLength
+		   <= buffer + buffer_size);
+
+  // CBMC loop unwinding: bounds depend on xBufferLength
+  __CPROVER_assume(xBufferLength <= NETWORK_BUFFER_SIZE);
+
+  prvParseDNSReply(pucUDPPayloadBuffer, xBufferLength, xIdentifier);
+
+}
diff --git a/FreeRTOS/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/README.md
new file mode 100644
index 000000000..48fb7c48d
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/README.md
@@ -0,0 +1 @@
+This directory contains the proofs checked by CBMC.   For each entry point of FreeRTOS tested, there is a directory that contains the test harness and cbmc configuration information needed to check the proof.
\ No newline at end of file
diff --git a/FreeRTOS/Test/CBMC/proofs/ReadNameField/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ReadNameField/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/SkipNameField/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/SkipNameField/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md
rename to FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md
diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_cbmc_batch_files.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_cbmc_batch_files.py
new file mode 100755
index 000000000..622e000c3
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_cbmc_batch_files.py
@@ -0,0 +1,53 @@
+#!/usr/bin/env python3
+#
+# Generation of the cbmc-batch.yaml files for the CBMC proofs.
+#
+# Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+import os
+import platform
+import subprocess
+
+
+def remove_cbmc_yaml_files():
+    for dyr, _, files in os.walk("."):
+        cbmc_batch_files = [os.path.join(os.path.abspath(dyr), file)
+                            for file in files if file == "cbmc-batch.yaml"]
+        for file in cbmc_batch_files:
+            os.remove(file)
+
+
+def create_cbmc_yaml_files():
+    # The YAML files are only used by CI and are not needed on Windows.
+    if platform.system() == "Windows":
+        return
+    for dyr, _, files in os.walk("."):
+        harness = [file for file in files if file.endswith("_harness.c")]
+        if harness and "Makefile" in files:
+            subprocess.run(["make", "cbmc-batch.yaml"],
+                           stdout=subprocess.PIPE,
+                           stderr=subprocess.PIPE,
+                           cwd=os.path.abspath(dyr),
+                           check=True)
+
+if __name__ == '__main__':
+    remove_cbmc_yaml_files()
+    create_cbmc_yaml_files()
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_common_makefile.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_common_makefile.py
new file mode 100755
index 000000000..efcf1db8d
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_common_makefile.py
@@ -0,0 +1,240 @@
+#!/usr/bin/env python3
+#
+# Generation of common Makefile for CBMC proofs.
+#
+# Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+from pprint import pprint
+import json
+import sys
+import re
+import os
+import argparse
+
+def cleanup_whitespace(string):
+    return re.sub('\s+', ' ', string.strip())
+
+################################################################
+# Operating system specific values
+
+platform_definitions = {
+    "linux": {
+        "platform": "linux",
+        "separator": "/",
+        "define": "-D",
+        "include": "-I",
+    },
+    "macos": {
+        "platform": "darwin",
+        "separator": "/",
+        "define": "-D",
+        "include": "-I",
+    },
+    "windows": {
+        "platform": "win32",
+        "separator": "\\",
+        "define": "/D",
+        "include": "/I",
+    },
+}
+
+
+def default_platform():
+    for platform, definition in platform_definitions.items():
+        if sys.platform == definition["platform"]:
+            return platform
+    return "linux"
+
+
+def patch_path_separator(opsys, string):
+    from_separator = '/'
+    to_separator = platform_definitions[opsys]["separator"]
+
+    def escape_separator(string):
+        return string.split(from_separator + from_separator)
+
+    def change_separator(string):
+        return string.replace(from_separator, to_separator)
+
+    return from_separator.join([change_separator(escaped)
+                                for escaped in escape_separator(string)])
+
+def patch_compile_output(opsys, line, key, value):
+    if opsys != "windows":
+        return line
+
+    if key in ["COMPILE_ONLY", "COMPILE_LINK"] and value is not None:
+        if value[-1] == '/Fo':
+            return re.sub('/Fo\s+', '/Fo', line)
+        if value[-1] == '/Fe':
+            return re.sub('/Fe\s+', '/Fe', line)
+    return line
+
+################################################################
+# Argument parsing
+#
+
+def get_arguments():
+    parser = argparse.ArgumentParser()
+    parser.add_argument(
+        "--system",
+        metavar="OS",
+        choices=platform_definitions,
+        default=str(default_platform()),
+        help="Generate makefiles for operating system OS"
+    )
+    return parser.parse_args()
+
+################################################################
+# Variable definitions
+#
+# JSON files give variable definitions for common, operating system,
+# and harness specfic values
+#
+
+def read_variable_definitions(filename):
+    variable = {}
+    with open(filename) as _file:
+        for key, values in json.load(_file).items():
+            variable[cleanup_whitespace(key)] = [cleanup_whitespace(value)
+                                                 for value in values]
+    return variable
+
+def find_definition_once(key, defines, prefix=None):
+
+    # Try looking up key with and without prefix
+    prefix = "{}_".format(prefix.rstrip('_')) if prefix else ""
+    key2 = key[len(prefix):] if key.startswith(prefix) else prefix + key
+
+    for _key in [key, key2]:
+        _value = defines.get(_key)
+        if _value is not None:
+            return _value
+
+    return None
+
+def find_definition(key, defines):
+    common_defines, opsys_defines, harness_defines = defines
+    return (find_definition_once(key, harness_defines, "H") or
+            find_definition_once(key, opsys_defines, "O") or
+            find_definition_once(key, common_defines, "C"))
+
+################################################################
+# Makefile generation
+
+def construct_definition(opsys, key_prefix, value_prefix, key, definitions):
+    values = definitions.get(key)
+    if not values:
+        return ""
+    if key in ["INC", "DEF"]:
+        values = [patch_path_separator(opsys, value)
+                  for value in values]
+    lines = ["\t{}{} \\".format(value_prefix, value) for value in values]
+    return "{}_{} = \\\n{}\n\t# empty\n".format(key_prefix,
+                                                key,
+                                                '\n'.join(lines))
+
+def write_define(opsys, define, defines, makefile):
+    value = find_definition(define, defines)
+    if value:
+        if define in ["FREERTOS", "PROOFS"]:
+            value = os.path.abspath(value[0])
+        makefile.write("{} = {}\n".format(define, value))
+
+def write_common_defines(opsys, defines, makefile):
+    common_defines, opsys_defines, harness_defines = defines
+
+    for key_prefix, defines in zip(["C", "O", "H"],
+                                   [common_defines,
+                                    opsys_defines,
+                                    harness_defines]):
+        for value_prefix, key in zip([platform_definitions[opsys]["include"],
+                                      platform_definitions[opsys]["define"],
+                                      "", ""],
+                                     ["INC", "DEF", "OPT", "CBMCFLAGS"]):
+            define = construct_definition(opsys,
+                                          key_prefix, value_prefix,
+                                          key, defines)
+            if define:
+                makefile.write(define + "\n")
+
+
+def write_makefile(opsys, template, defines, makefile):
+    with open(template) as _template:
+        for line in _template:
+            line = patch_path_separator(opsys, line)
+            keys = re.findall('@(\w+)@', line)
+            values = [find_definition(key, defines) for key in keys]
+            for key, value in zip(keys, values):
+                if value is not None:
+                    line = line.replace('@{}@'.format(key), " ".join(value))
+                    line = patch_compile_output(opsys, line, key, value)
+            makefile.write(line)
+
+def write_cbmcbatchyaml_target(opsys, _makefile):
+    target = """
+################################################################
+# Build configuration file to run cbmc under cbmc-batch in CI
+
+define encode_options
+'=$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')='
+endef
+
+cbmc-batch.yaml:
+	@echo "Building $@"
+	@$(RM) $@
+	@echo "jobos: ubuntu16" >> $@
+	@echo "cbmcflags: $(call encode_options,$(CBMCFLAGS) --unwinding-assertions)" >> $@
+	@echo "goto: $(ENTRY).goto" >> $@
+	@echo "expected: $(H_EXPECTED)" >> $@
+
+################################################################
+"""
+    if opsys != "windows":
+        _makefile.write(target)
+
+def makefile_from_template(opsys, template, defines, makefile="Makefile"):
+    with open(makefile, "w") as _makefile:
+        write_define(opsys, "FREERTOS", defines, _makefile)
+        write_define(opsys, "PROOFS", defines, _makefile)
+        write_common_defines(opsys, defines, _makefile)
+        write_makefile(opsys, template, defines, _makefile)
+        write_cbmcbatchyaml_target(opsys, _makefile)
+
+################################################################
+# Main
+
+def main():
+    args = get_arguments()
+
+    common_defines = read_variable_definitions("MakefileCommon.json")
+    opsys_defines = read_variable_definitions("MakefileWindows.json"
+                                              if args.system == "windows"
+                                              else "MakefileLinux.json")
+    harness_defines = {}
+
+    makefile_from_template(args.system,
+                           "Makefile.template",
+                           (common_defines, opsys_defines, harness_defines),
+                           "Makefile.common")
+
+if __name__ == "__main__":
+    main()
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_configuration_directories.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_configuration_directories.py
new file mode 100755
index 000000000..9e006e9ed
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_configuration_directories.py
@@ -0,0 +1,163 @@
+#!/usr/bin/env python3
+#
+# Creating the CBMC proofs from Configurations.json.
+#
+# Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+import collections
+import json
+import logging
+import os
+import pathlib
+import shutil
+import textwrap
+
+from make_proof_makefiles import load_json_config_file
+
+LOGGER = logging.getLogger("ComputeConfigurations")
+
+def prolog():
+    return textwrap.dedent("""\
+        This script Generates Makefile.json from Configrations.json.
+
+        Starting in the current directory, it walks down every subdirectory
+        looking for Configurations.json files. Every found Configurations.json
+        file is assumed to look similar to the following format:
+
+        {
+          "ENTRY": "ARPProcessPacket",
+          "CBMCFLAGS":
+          [
+              "--unwind 1",
+              "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17",
+              "--nondet-static"
+          ],
+          "OBJS":
+          [
+            "$(ENTRY)_harness.goto",
+            "$(FREERTOS)/lib/FreeRTOS-Plus-TCP/source/FreeRTOS_ARP.goto"
+          ],
+          "DEF":
+          [
+            {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]},
+            {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]}
+          ]
+        }
+
+        The format is mainly taken from the Makefile.json files.
+        The only difference is that it expects a list of json object in the DEF
+        section. This script will generate a Makefile.json in a subdirectory and
+        copy the harness to each subdirectory.
+        The key is later taken as the name for the configuration subdirectory
+        prexied by 'config_'.
+
+        So for the above script, we get two subdirectories:
+        -config_disableClashDetection
+        -config_enableClashDetection
+
+        As an example, the resulting Makefile.json for the
+        config_disableClashDetection directory will be:
+
+        {
+          "ENTRY": "ARPProcessPacket",
+          "CBMCFLAGS": [
+            "--unwind 1",
+            "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17",
+            "--nondet-static"
+          ],
+          "OBJS": [
+            "$(ENTRY)_harness.goto",
+            "$(FREERTOS)/lib/FreeRTOS-Plus-TCP/source/FreeRTOS_ARP.goto"
+          ],
+          "DEF": [
+            "ipconfigARP_USE_CLASH_DETECTION=0"
+          ]
+        }
+
+        These Makefile.json files then can be turned into Makefiles for running
+        the proof by executing the make-proof-makefiles.py script.
+        """)
+
+
+def process(folder, files):
+    json_content = load_json_config_file(os.path.join(folder,
+                                                      "Configurations.json"))
+    try:
+        def_list = json_content["DEF"]
+    except KeyError:
+        LOGGER.error("Expected DEF as key in a Configurations.json files.")
+        return
+    for config in def_list:
+        logging.debug(config)
+        try:
+            configname = [name for name in config.keys()
+                          if name != "EXPECTED"][0]
+            configbody = config[configname]
+        except (AttributeError, IndexError) as e:
+            LOGGER.error(e)
+            LOGGER.error(textwrap.dedent("""\
+            The expected layout for an entry in the Configurations.json
+            file is a dictonary. Here is an example of the expected format:
+
+            "DEF":
+            [
+              {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]},
+              {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]}
+            ]
+                """))
+            LOGGER.error("The offending entry is %s", config)
+            return
+        new_config_folder = os.path.join(folder, "config_" + configname)
+        pathlib.Path(new_config_folder).mkdir(exist_ok=True, parents=True)
+        harness_copied = False
+        for file in files:
+            if file.endswith("harness.c"):
+                shutil.copy(os.path.join(folder, file),
+                            os.path.join(new_config_folder, file))
+                harness_copied = True
+
+        if not harness_copied:
+            LOGGER.error("Could not find a harness in folder %s.", folder)
+            LOGGER.error("This folder is not processed do the end!")
+            return
+        # The order of keys must be maintained as otherwise the
+        # make_proof_makefiles script might fail.
+        current_config = collections.OrderedDict(json_content)
+        current_config["DEF"] = configbody
+        if "EXPECTED" in config.keys():
+            current_config["EXPECTED"] = config["EXPECTED"]
+        else:
+            current_config["EXPECTED"] = True
+        with open(os.path.join(new_config_folder, "Makefile.json"),
+                  "w") as output_file:
+            json.dump(current_config, output_file, indent=2)
+
+
+def main():
+    for fldr, _, fyles in os.walk("."):
+        if "Configurations.json" in fyles:
+            process(fldr, fyles)
+
+
+if __name__ == '__main__':
+    logging.basicConfig(format="{script}: %(levelname)s %(message)s".format(
+        script=os.path.basename(__file__)))
+    main()
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_proof_makefiles.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_proof_makefiles.py
new file mode 100755
index 000000000..846942ee4
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_proof_makefiles.py
@@ -0,0 +1,416 @@
+#!/usr/bin/env python3
+#
+# Generation of Makefiles for CBMC proofs.
+#
+# Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+
+import argparse
+import ast
+import collections
+import json
+import logging
+import operator
+import os
+import os.path
+import platform
+import re
+import sys
+import textwrap
+import traceback
+
+
+# ______________________________________________________________________________
+# Compatibility between different python versions
+# ``````````````````````````````````````````````````````````````````````````````
+
+# Python 3 doesn't have basestring
+try:
+    basestring
+except NameError:
+    basestring = str
+
+# ast.Num was deprecated in python 3.8
+_plat = platform.python_version().split(".")
+if _plat[0] == "3" and int(_plat[1]) > 7:
+    ast_num = ast.Constant
+else:
+    ast_num = ast.Num
+# ______________________________________________________________________________
+
+
+def prolog():
+    return textwrap.dedent("""\
+        This script generates Makefiles that can be used either on Windows (with
+        NMake) or Linux (with GNU Make). The Makefiles consist only of variable
+        definitions; they are intended to be used with a common Makefile that
+        defines the actual rules.
+
+        The Makefiles are generated from JSON specifications. These are simple
+        key-value dicts, but can contain variables and computation, as
+        well as comments (lines whose first character is "#"). If the
+        JSON file contains the following information:
+
+                {
+                    # 'T was brillig, and the slithy toves
+                    "FOO": "BAR",
+                    "BAZ": "{FOO}",
+
+                    # Did gyre and gimble in the wabe;
+                    "QUUX": 30
+                    "XYZZY": "__eval 5 if {QUUZ} < 5 else min({QUUX}, 60)"
+                }
+
+        then the resulting Makefile will look like
+
+                H_FOO = BAR
+                H_BAZ = BAR
+                H_QUUX = 30
+                H_XYZZY = 30
+
+        The language used for evaluation is highly restricted; arbitrary
+        python is not allowed.  JSON values that are lists will be
+        joined with whitespace:
+
+                { "FOO": ["BAR", "BAZ", "QUX"] }
+
+                ->
+
+                H_FOO = BAR BAZ QUX
+
+        As a special case, if a key is equal to "DEF", "INC" (and maybe more,
+        read the code) the list of values is treated as a list of defines or
+        include paths. Thus, they have -D or /D, or -I or /I, prepended to them
+        as appropriate for the platform.
+
+
+                { "DEF": ["DEBUG", "FOO=BAR"] }
+
+                on Linux ->
+
+                H_DEF = -DDEBUG -DFOO=BAR
+
+        Pathnames are written with a forward slash in the JSON file. In
+        each value, all slashes are replaced with backslashes if
+        generating Makefiles for Windows. If you wish to generate a
+        slash even on Windows, use two slashes---that will be changed
+        into a single forward slash on both Windows and Linux.
+
+                {
+                    "INC": [ "my/cool/directory" ],
+                    "DEF": [ "HALF=//2" ]
+                }
+
+                On Windows ->
+
+                H_INC = /Imy\cool\directory
+                H_DEF = /DHALF=/2
+
+        When invoked, this script walks the directory tree looking for files
+        called "Makefile.json". It reads that file and dumps a Makefile in that
+        same directory. We assume that this script lives in the same directory
+        as a Makefile called "Makefile.common", which contains the actual Make
+        rules. The final line of each of the generated Makefiles will be an
+        include statement, including Makefile.common.
+    """)
+
+def load_json_config_file(file):
+    with open(file) as handle:
+        lines = handle.read().splitlines()
+    no_comments = "\n".join([line for line in lines
+                             if line and not line.lstrip().startswith("#")])
+    try:
+        data = json.loads(no_comments,
+                          object_pairs_hook=collections.OrderedDict)
+    except json.decoder.JSONDecodeError:
+        traceback.print_exc()
+        logging.error("parsing file %s", file)
+        sys.exit(1)
+    return data
+
+
+def dump_makefile(dyr, system):
+    data = load_json_config_file(os.path.join(dyr, "Makefile.json"))
+
+    makefile = collections.OrderedDict()
+
+    # Makefile.common expects a variable called OBJS_EXCEPT_HARNESS to be
+    # set to a list of all the object files except the harness.
+    if "OBJS" not in data:
+        logging.error(
+            "Expected a list of object files in %s/Makefile.json" % dyr)
+        exit(1)
+    makefile["OBJS_EXCEPT_HARNESS"] = " ".join(
+        o for o in data["OBJS"] if not o.endswith("_harness.goto"))
+
+    so_far = collections.OrderedDict()
+    for name, value in data.items():
+        if isinstance(value, list):
+            new_value = []
+            for item in value:
+                new_value.append(compute(item, so_far, system, name, dyr, True))
+            makefile[name] = " ".join(new_value)
+        else:
+            makefile[name] = compute(value, so_far, system, name, dyr)
+
+    if (("EXPECTED" not in makefile.keys()) or
+            str(makefile["EXPECTED"]).lower() == "true"):
+        makefile["EXPECTED"] = "SUCCESSFUL"
+    elif str(makefile["EXPECTED"]).lower() == "false":
+        makefile["EXPECTED"] = "FAILURE"
+    makefile = ["H_%s = %s" % (k, v) for k, v in makefile.items()]
+
+    # Deal with the case of a harness being nested several levels under
+    # the top-level proof directory, where the common Makefile lives
+    common_dir_path = "..%s" % _platform_choices[system]["path-sep"]
+    common_dir_path = common_dir_path * len(dyr.split(os.path.sep)[1:])
+
+    with open(os.path.join(dyr, "Makefile"), "w") as handle:
+        handle.write(("""{contents}
+
+{include} {common_dir_path}Makefile.common""").format(
+            contents="\n".join(makefile),
+            include=_platform_choices[system]["makefile-inc"],
+            common_dir_path=common_dir_path))
+
+
+def compute(value, so_far, system, key, harness, appending=False):
+    if not isinstance(value, (basestring, float, int)):
+        logging.error(wrap("""\
+                        in file %s, the key '%s' has value '%s',
+                        which is of the wrong type (%s)"""),
+                      os.path.join(harness, "Makefile.json"), key,
+                      str(value), str(type(value)))
+        exit(1)
+
+    value = str(value)
+    try:
+        var_subbed = value.format(**so_far)
+    except KeyError as e:
+        logging.error(wrap("""\
+                        in file %s, the key '%s' has value '%s', which
+                        contains the variable %s, but that variable has
+                        not previously been set in the file"""),
+                      os.path.join(harness, "Makefile.json"), key,
+                      value, str(e))
+        exit(1)
+
+    if var_subbed[:len("__eval")] != "__eval":
+        tmp = re.sub("//", "__DOUBLE_SLASH__", var_subbed)
+        tmp = re.sub("/", _platform_choices[system]["path-sep-re"], tmp)
+        evaluated = re.sub("__DOUBLE_SLASH__", "/", tmp)
+    else:
+        to_eval = var_subbed[len("__eval"):].strip()
+        logging.debug("About to evaluate '%s'", to_eval)
+        evaluated = eval_expr(to_eval,
+                              os.path.join(harness, "Makefile.json"),
+                              key, value)
+
+    if key == "DEF":
+        final_value = "%s%s" % (_platform_choices[system]["define"],
+                                evaluated)
+    elif key == "INC":
+        final_value = "%s%s" % (_platform_choices[system]["include"],
+                                evaluated)
+    else:
+        final_value = evaluated
+
+    # Allow this value to be used for future variable substitution
+    if appending:
+        try:
+            so_far[key] = "%s %s" % (so_far[key], final_value)
+        except KeyError:
+            so_far[key] = final_value
+        logging.debug("Appending final value '%s' to key '%s'",
+                      final_value, key)
+    else:
+        so_far[key] = final_value
+        logging.info("Key '%s' set to final value '%s'", key, final_value)
+
+    return final_value
+
+
+def eval_expr(expr_string, harness, key, value):
+    """
+    Safe evaluation of purely arithmetic expressions
+    """
+    try:
+        tree = ast.parse(expr_string, mode="eval").body
+    except SyntaxError:
+        traceback.print_exc()
+        logging.error(wrap("""\
+            in file %s at key '%s', value '%s' contained the expression
+            '%s' which is an invalid expression"""), harness, key,
+                      value, expr_string)
+        exit(1)
+
+    def eval_single_node(node):
+        logging.debug(node)
+        if isinstance(node, ast_num):
+            return node.n
+        # We're only doing IfExp, which is Python's ternary operator
+        # (i.e. it's an expression). NOT If, which is a statement.
+        if isinstance(node, ast.IfExp):
+            # Let's be strict and only allow actual booleans in the guard
+            guard = eval_single_node(node.test)
+            if guard is not True and guard is not False:
+                logging.error(wrap("""\
+                    in file %s at key '%s', there was an invalid guard
+                    for an if statement."""), harness, key)
+                exit(1)
+            if guard:
+                return eval_single_node(node.body)
+            return eval_single_node(node.orelse)
+        if isinstance(node, ast.Compare):
+            left = eval_single_node(node.left)
+            # Don't allow expressions like (a < b) < c
+            right = eval_single_node(node.comparators[0])
+            op = eval_single_node(node.ops[0])
+            return op(left, right)
+        if isinstance(node, ast.BinOp):
+            left = eval_single_node(node.left)
+            right = eval_single_node(node.right)
+            op = eval_single_node(node.op)
+            return op(left, right)
+        if isinstance(node, ast.Call):
+            valid_calls = {
+                "max": max,
+                "min": min,
+            }
+            if node.func.id not in valid_calls:
+                logging.error(wrap("""\
+                    in file %s at key '%s', there was an invalid
+                    call to %s()"""), harness, key, node.func.id)
+                exit(1)
+            left = eval_single_node(node.args[0])
+            right = eval_single_node(node.args[1])
+            return valid_calls[node.func.id](left, right)
+        try:
+            return {
+                ast.Eq: operator.eq,
+                ast.NotEq: operator.ne,
+                ast.Lt: operator.lt,
+                ast.LtE: operator.le,
+                ast.Gt: operator.gt,
+                ast.GtE: operator.ge,
+
+                ast.Add: operator.add,
+                ast.Sub: operator.sub,
+                ast.Mult: operator.mul,
+                # Use floordiv (i.e. //) so that we never need to
+                # cast to an int
+                ast.Div: operator.floordiv,
+            }[type(node)]
+        except KeyError:
+            logging.error(wrap("""\
+                in file %s at key '%s', there was expression that
+                was impossible to evaluate"""), harness, key)
+            exit(1)
+
+    return eval_single_node(tree)
+
+
+_platform_choices = {
+    "linux": {
+        "platform": "linux",
+        "path-sep": "/",
+        "path-sep-re": "/",
+        "define": "-D",
+        "include": "-I",
+        "makefile-inc": "include",
+    },
+    "windows": {
+        "platform": "win32",
+        "path-sep": "\\",
+        "path-sep-re": re.escape("\\"),
+        "define": "/D",
+        "include": "/I",
+        "makefile-inc": "!INCLUDE",
+    },
+}
+# Assuming macos is the same as linux
+_mac_os = dict(_platform_choices["linux"])
+_mac_os["platform"] = "darwin"
+_platform_choices["macos"] = _mac_os
+
+
+def default_platform():
+    for arg_string, os_data in _platform_choices.items():
+        if sys.platform == os_data["platform"]:
+            return arg_string
+    return "linux"
+
+
+_args = [{
+    "flags": ["-s", "--system"],
+    "metavar": "OS",
+    "choices": _platform_choices,
+    "default": str(default_platform()),
+    "help": textwrap.dedent("""\
+                which operating system to generate makefiles for.
+                Defaults to the current platform (%(default)s);
+                choices are {choices}""").format(
+                    choices="[%s]" % ", ".join(_platform_choices)),
+}, {
+    "flags": ["-v", "--verbose"],
+    "help": "verbose output",
+    "action": "store_true",
+}, {
+    "flags": ["-w", "--very-verbose"],
+    "help": "very verbose output",
+    "action": "store_true",
+    }]
+
+
+def get_args():
+    pars = argparse.ArgumentParser(
+        description=prolog(),
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    for arg in _args:
+        flags = arg.pop("flags")
+        pars.add_argument(*flags, **arg)
+    return pars.parse_args()
+
+
+def set_up_logging(args):
+    fmt = "{script}: %(levelname)s %(message)s".format(
+        script=os.path.basename(__file__))
+    if args.very_verbose:
+        logging.basicConfig(format=fmt, level=logging.DEBUG)
+    elif args.verbose:
+        logging.basicConfig(format=fmt, level=logging.INFO)
+    else:
+        logging.basicConfig(format=fmt, level=logging.WARNING)
+
+def wrap(string):
+    return re.sub(r"\s+", " ", re.sub("\n", " ", string))
+
+def main():
+    args = get_args()
+    set_up_logging(args)
+
+    for root, _, fyles in os.walk("."):
+        if "Makefile.json" in fyles:
+            dump_makefile(root, args.system)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_remove_makefiles.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_remove_makefiles.py
new file mode 100755
index 000000000..12d0c72f1
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_remove_makefiles.py
@@ -0,0 +1,48 @@
+#!/usr/bin/env python3
+#
+# Removing the generated Makefiles and cbmc-batch.yaml files.
+#
+# Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+import os
+
+from make_cbmc_batch_files import remove_cbmc_yaml_files
+
+def main():
+    try:
+        os.remove("Makefile.common")
+    except FileNotFoundError:
+        pass
+
+    for root, _, files in os.walk("."):
+        # We do not want to remove hand-written Makefiles, so
+        # only remove Makefiles that are in the same directory as
+        # a Makefile.json. Such Makefiles are generated from the
+        # JSON file.
+        if "Makefile.json" in files:
+            try:
+                os.remove(os.path.join(root, "Makefile"))
+            except FileNotFoundError:
+                pass
+
+if __name__ == "__main__":
+    remove_cbmc_yaml_files()
+    main()
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/make_type_header_files.py b/FreeRTOS-Plus/Test/CBMC/proofs/make_type_header_files.py
new file mode 100755
index 000000000..a8ac66384
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/make_type_header_files.py
@@ -0,0 +1,162 @@
+#!/usr/bin/env python3
+#
+# Compute type header files for c modules
+#
+# Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+
+import argparse
+import logging
+import os
+import re
+import shutil
+import subprocess
+import sys
+from tempfile import TemporaryDirectory
+
+def epilog():
+    return """\
+        This program dumps a header file containing the types and macros
+        contained in the C file passed as input. It uses `goto-instrument`
+        from the CBMC tool suite instead of the preprocessor, to dump types
+        and other constructs as well as preprocessor directives.
+
+        This program should be used in cases where types or macros declared
+        for internal use in a C file use are needed to write a test harness
+        or CBMC proof.  The intention is that the build process will run
+        this program to dump the header file, and the proof will #include
+        the header.
+    """
+
+_DEFINE_REGEX_HEADER = re.compile(r"\s*#\s*define\s*([\w]+)")
+
+
+def get_module_name(fyle):
+    base = os.path.basename(fyle)
+    return base.split(".")[0]
+
+
+def collect_defines(fyle):
+    collector_result = ""
+    continue_define = False
+    in_potential_def_scope = ""
+    potential_define = False
+    potential_define_confirmed = False
+    with open(fyle) as in_file:
+        for line in in_file:
+            matched = _DEFINE_REGEX_HEADER.match(line)
+            if line.strip().startswith("#if"):
+                potential_define = True
+                in_potential_def_scope += line
+            elif line.strip().startswith("#endif") and potential_define:
+                if potential_define_confirmed:
+                    in_potential_def_scope += line
+                    collector_result += in_potential_def_scope
+                in_potential_def_scope = ""
+                potential_define = False
+                potential_define_confirmed = False
+            elif matched and potential_define:
+                potential_define_confirmed = True
+                in_potential_def_scope += line
+            elif matched or continue_define:
+                continue_define = line.strip("\n").endswith("\\")
+                collector_result += line
+            elif potential_define:
+                in_potential_def_scope += line
+    return collector_result
+
+
+def make_header_file(goto_binary, fyle, target_folder):
+    fyle = os.path.normpath(fyle)
+    with TemporaryDirectory() as tmpdir:
+        module = get_module_name(fyle)
+        header_file = "{}_datastructure.h".format(module)
+
+        drop_header_cmd = ["goto-instrument",
+                           "--dump-c-type-header",
+                           module,
+                           goto_binary,
+                           header_file]
+        res = subprocess.run(drop_header_cmd,
+                             stdout=subprocess.PIPE,
+                             stderr=subprocess.STDOUT,
+                             universal_newlines=True,
+                             cwd=tmpdir)
+        if res.returncode:
+            logging.error("Dumping type header for file '%s' failed", fyle)
+            logging.error("The command `%s` returned %s",
+                          drop_header_cmd,
+                          res.stdout)
+            logging.error("The return code is %d", int(res.returncode))
+            sys.exit(1)
+
+        header = os.path.normpath(os.path.join(tmpdir, header_file))
+        collected = collect_defines(fyle)
+        logging.debug("Dumping the following header file to '%s':\n%s\n"
+                      "// END GENERATED HEADER FILE", header, collected)
+        with open(header, "a") as out:
+            print(collected, file=out)
+
+        target_file = os.path.normpath(os.path.join(target_folder, header_file))
+        shutil.move(header, target_file)
+
+
+_ARGS = [{
+    "flags": ["--c-file"],
+    "metavar": "F",
+    "help": "source file to extract types and headers from",
+    "required": True
+}, {
+    "flags": ["--binary"],
+    "metavar": "B",
+    "help": "file compiled from the source file with CBMC's goto-cc compiler",
+    "required": True
+}, {
+    "flags": ["--out-dir"],
+    "metavar": "D",
+    "help": ("directory to write the generated header file to "
+             "(default: %(default)s)"),
+    "default": os.path.abspath(os.getcwd()),
+}, {
+    "flags": ["--verbose", "-v"],
+    "help": "verbose output",
+    "action": "store_true"
+}]
+
+
+if __name__ == '__main__':
+    pars = argparse.ArgumentParser(
+        epilog=epilog(),
+        description="Dump a C file's types and macros to a separate file")
+    for arg in _ARGS:
+        flags = arg.pop("flags")
+        pars.add_argument(*flags, **arg)
+
+    args = pars.parse_args()
+
+    fmt = "{script}: %(levelname)s %(message)s".format(
+        script=os.path.basename(__file__))
+    if args.verbose:
+        logging.basicConfig(format=fmt, level=logging.DEBUG)
+    else:
+        logging.basicConfig(format=fmt, level=logging.INFO)
+
+    make_header_file(args.binary, args.c_file, args.out_dir)
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ninja.py b/FreeRTOS-Plus/Test/CBMC/proofs/ninja.py
new file mode 100755
index 000000000..4bfd3c8d4
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ninja.py
@@ -0,0 +1,219 @@
+#!/usr/bin/env python3
+
+"""
+Write a ninja build file to generate reports for cbmc proofs.
+
+Given a list of folders containing cbmc proofs, write a ninja build
+file the generate reports for these proofs.  The list of folders may
+be given on the command line, in a json file, or found in the file
+system.
+"""
+
+# Add task pool
+
+import sys
+import os
+import platform
+import argparse
+import json
+
+################################################################
+# The command line parser
+
+def argument_parser():
+    """Return the command line parser."""
+
+    parser = argparse.ArgumentParser(
+        description='Generate ninja build file for cbmc proofs.',
+        epilog="""
+            Given a list of folders containing cbmc proofs, write a ninja build
+            file the generate reports for these proofs.  The list of folders may
+            be given on the command line, in a json file, or found in the file
+            system.
+            In the json file, there should be a dict mapping the key "proofs"
+            to a list of folders containing proofs.
+            The file system, all folders folders under the current directory
+            containing a file named 'cbmc-batch.yaml' is considered a
+            proof folder.
+            This script assumes that the proof is driven by a Makefile
+            with targets goto, cbmc, coverage, property, and report.
+            This script does not work with Windows and Visual Studio.
+        """
+    )
+    parser.add_argument('folders', metavar='PROOF', nargs='*',
+                        help='Folder containing a cbmc proof')
+    parser.add_argument('--proofs', metavar='JSON',
+                        help='Json file listing folders containing cbmc proofs')
+    return parser
+
+################################################################
+# The list of folders containing proofs
+#
+# The list of folders will be taken from
+# 1. the list PROOFS defined here or
+# 2. the command line
+# 3. the json file specified on the command line containing a
+#    dict mapping the key JSON_KEY to a list of folders
+# 4. the folders below the current directory containing
+#    a file named FS_KEY
+#
+
+PROOFS = [
+]
+
+JSON_KEY = 'proofs'
+FS_KEY = 'cbmc-batch.yaml'
+
+def find_proofs_in_json_file(filename):
+    """Read the list of folders containing proofs from a json file."""
+
+    if not filename:
+        return []
+    try:
+        with open(filename) as proofs:
+            return json.load(proofs)[JSON_KEY]
+    except (FileNotFoundError, KeyError):
+        raise UserWarning("Can't find key {} in json file {}".format(JSON_KEY, filename))
+    except json.decoder.JSONDecodeError:
+        raise UserWarning("Can't parse json file {}".format(filename))
+
+def find_proofs_in_filesystem():
+    """Locate the folders containing proofs in the filesystem."""
+
+    proofs = []
+    for root, _, files in os.walk('.'):
+        if FS_KEY in files:
+            proofs.append(os.path.normpath(root))
+    return proofs
+
+################################################################
+# The strings used to write sections of the ninja file
+
+NINJA_RULES = """
+################################################################
+# task pool to force sequential builds of goto binaries
+
+pool goto_pool
+  depth = 1
+
+################################################################
+# proof target rules
+
+rule build_goto
+  command = make -C ${folder} goto
+  pool = goto_pool
+
+rule build_cbmc
+  command = make -C ${folder} cbmc
+
+rule build_coverage
+  command = make -C ${folder} coverage
+
+rule build_property
+  command = make -C ${folder} property
+
+rule build_report
+  command = make -C ${folder} report
+
+rule clean_folder
+  command = make -C ${folder} clean
+
+rule veryclean_folder
+  command = make -C ${folder} veryclean
+
+rule open_proof
+  command = open ${folder}/html/index.html
+
+"""
+
+NINJA_BUILDS = """
+################################################################
+# {folder} proof targets
+
+build {folder}/{entry}.goto: build_goto
+  folder={folder}
+
+build {folder}/cbmc.txt: build_cbmc {folder}/{entry}.goto
+  folder={folder}
+
+build {folder}/coverage.xml: build_coverage {folder}/{entry}.goto
+  folder={folder}
+
+build {folder}/property.xml: build_property {folder}/{entry}.goto
+  folder={folder}
+
+build {folder}/html/index.html: build_report {folder}/{entry}.goto {folder}/cbmc.txt {folder}/coverage.xml {folder}/property.xml
+  folder={folder}
+
+build clean_{folder}: clean_folder
+  folder={folder}
+
+build veryclean_{folder}: veryclean_folder
+  folder={folder}
+
+build open_{folder}: open_proof
+  folder={folder}
+
+build {folder}: phony {folder}/html/index.html
+
+default {folder}
+
+"""
+
+NINJA_GLOBALS = """
+################################################################
+# global targets
+
+build clean: phony {clean_targets}
+
+build veryclean: phony {veryclean_targets}
+
+build open: phony {open_targets}
+"""
+
+################################################################
+# The main function
+
+def get_entry(folder):
+    """Find the name of the proof in the proof Makefile."""
+
+    with open('{}/Makefile'.format(folder)) as makefile:
+        for line in makefile:
+            if line.strip().lower().startswith('entry'):
+                return line[line.find('=')+1:].strip()
+            if line.strip().lower().startswith('h_entry'):
+                return line[line.find('=')+1:].strip()
+    raise UserWarning("Can't find ENTRY in {}/Makefile".format(folder))
+
+def write_ninja_build_file():
+    """Write a ninja build file to generate proof results."""
+
+    if platform.system().lower() == 'windows':
+        print("This script does not run on Windows.")
+        sys.exit()
+
+    args = argument_parser().parse_args()
+
+    proofs = (PROOFS or
+              args.folders or
+              find_proofs_in_json_file(args.proofs) or
+              find_proofs_in_filesystem())
+
+    with open('build.ninja', 'w') as ninja:
+        ninja.write(NINJA_RULES)
+        for proof in proofs:
+            entry = get_entry(proof)
+            ninja.write(NINJA_BUILDS.format(folder=proof, entry=entry))
+        targets = lambda kind, folders: ' '.join(
+            ['{}_{}'.format(kind, folder) for folder in folders]
+        )
+        ninja.write(NINJA_GLOBALS.format(
+            clean_targets=targets('clean', proofs),
+            veryclean_targets=targets('veryclean', proofs),
+            open_targets=targets('open', proofs)
+        ))
+
+################################################################
+
+if __name__ == "__main__":
+    write_ninja_build_file()
diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json
rename to FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json
diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
similarity index 100%
rename from FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
rename to FreeRTOS-Plus/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/prepare.py b/FreeRTOS-Plus/Test/CBMC/proofs/prepare.py
new file mode 100755
index 000000000..58f9903db
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/prepare.py
@@ -0,0 +1,115 @@
+#!/usr/bin/env python3
+#
+# Python script for preparing the code base for the CBMC proofs.
+#
+# Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+import logging
+import os
+import sys
+import textwrap
+from subprocess import CalledProcessError
+
+from make_common_makefile import main as make_common_file
+from make_configuration_directories import main as process_configurations
+from make_proof_makefiles import main as make_proof_files
+from make_cbmc_batch_files import create_cbmc_yaml_files
+
+CWD = os.getcwd()
+sys.path.append(os.path.normpath(os.path.join(CWD, "..", "patches")))
+
+#from compute_patch import create_patches
+#from compute_patch import DirtyGitError
+#from compute_patch import PatchCreationError
+from patches_constants import HEADERS
+
+from compute_patch import find_all_defines
+from compute_patch import manipulate_headerfile
+
+import patch
+
+PROOFS_DIR = os.path.dirname(os.path.abspath(__file__))
+
+LOGGER = logging.getLogger("PrepareLogger")
+
+################################################################
+
+def patch_headers(headers):
+    """Patch headers so we can define symbols on the command line.
+
+    When building for CBMC, it is convenient to define symbols on the
+    command line and know that these definitions will override the
+    definitions of the same symbols in header files.
+
+    The create_patches function takes a list of header files, searches
+    the Makefile.json files for symbols that will be defined in the
+    Makefiles, and creates patch files that protect the definition of
+    those symbols in header files with #ifndef/#endif.  In this way,
+    command line definitions will override header file definitions.
+
+    The create_patches function, however, depends on the fact that all
+    header files being modified are included in the top-level git
+    repository.  This assumption is violated if header files live in
+    submodules.
+
+    This function just updates the header files in place without
+    creating patch files.  One potential vulnerability of this
+    function is that it could cause preexisting patch files to fail if
+    they patch a file being modified here.
+    """
+    defines = find_all_defines()
+    for header in headers:
+        manipulate_headerfile(defines, header)
+
+################################################################
+
+def build():
+    process_configurations()
+    make_common_file()
+    make_proof_files()
+    try:
+        create_cbmc_yaml_files()
+    except CalledProcessError as e:
+        logging.error(textwrap.dedent("""\
+            An error occured during cbmc-batch generation.
+            The error message is: {}
+            """.format(str(e))))
+        exit(1)
+
+    # Patch headers directly instead of creating patch files.
+    patch.patch()
+    patch_headers(HEADERS)
+
+    #try:
+    #    create_patches(HEADERS)
+    #except (DirtyGitError, PatchCreationError) as e:
+    #    logging.error(textwrap.dedent("""\
+    #        An error occured during patch creation.
+    #        The error message is: {}
+    #        """.format(str(e))))
+    #    exit(1)
+
+################################################################
+
+if __name__ == '__main__':
+    logging.basicConfig(format="{script}: %(levelname)s %(message)s".format(
+        script=os.path.basename(__file__)))
+    build()
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c b/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c
new file mode 100644
index 000000000..6bcb9319a
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/utility/memory_assignments.c
@@ -0,0 +1,24 @@
+#define ensure_memory_is_valid( px, length ) (px != NULL) && __CPROVER_w_ok((px), length)
+
+/* Implementation of safe malloc which returns NULL if the requested size is 0.
+ Warning: The behavior of malloc(0) is platform dependent.
+ It is possible for malloc(0) to return an address without allocating memory.*/
+void *safeMalloc(size_t xWantedSize) {
+        return nondet_bool() ? malloc(xWantedSize) : NULL;
+}
+
+/* Memory assignment for FreeRTOS_Socket_t */
+FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated () {
+	FreeRTOS_Socket_t *pxSocket = safeMalloc(sizeof(FreeRTOS_Socket_t));
+	if (ensure_memory_is_valid(pxSocket, sizeof(FreeRTOS_Socket_t))) {
+		pxSocket->u.xTCP.rxStream = safeMalloc(sizeof(StreamBuffer_t));
+		pxSocket->u.xTCP.txStream = safeMalloc(sizeof(StreamBuffer_t));
+		pxSocket->u.xTCP.pxPeerSocket = safeMalloc(sizeof(FreeRTOS_Socket_t));
+	}
+	return pxSocket;
+}
+
+/* Memory assignment for FreeRTOS_Network_Buffer */
+NetworkBufferDescriptor_t * ensure_FreeRTOS_NetworkBuffer_is_allocated () {
+	return safeMalloc(sizeof(NetworkBufferDescriptor_t));
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/windows/README.md b/FreeRTOS-Plus/Test/CBMC/windows/README.md
new file mode 100644
index 000000000..e9f415060
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/windows/README.md
@@ -0,0 +1,2 @@
+This directory contains include files used by the CBMC proofs:
+* Windows.h and WinBase.h are include files used to build FreeRTOS (the parts we currently test) on Linux
\ No newline at end of file
diff --git a/FreeRTOS-Plus/Test/CBMC/windows/WinBase.h b/FreeRTOS-Plus/Test/CBMC/windows/WinBase.h
new file mode 100644
index 000000000..e69de29bb
diff --git a/FreeRTOS-Plus/Test/CBMC/windows/Windows.h b/FreeRTOS-Plus/Test/CBMC/windows/Windows.h
new file mode 100644
index 000000000..e69de29bb
diff --git a/FreeRTOS-Plus/Test/CBMC/windows/direct.h b/FreeRTOS-Plus/Test/CBMC/windows/direct.h
new file mode 100644
index 000000000..8b1378917
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/windows/direct.h
@@ -0,0 +1 @@
+
diff --git a/FreeRTOS-Plus/Test/README.md b/FreeRTOS-Plus/Test/README.md
new file mode 100644
index 000000000..a85db2642
--- /dev/null
+++ b/FreeRTOS-Plus/Test/README.md
@@ -0,0 +1,9 @@
+## Testing in FreeRTOS
+FreeRTOS kernel consists of common code and porting layer. Extensive [static analysis](https://en.wikipedia.org/wiki/Static_program_analysis) and [dynamic analysis](https://en.wikipedia.org/wiki/Dynamic_program_analysis) are done on both to ensure functional correctness of FreeRTOS kernel. 
+
+For more information on FreeRTOS testing please refer to https://www.freertos.org/FreeRTOS-Coding-Standard-and-Style-Guide.html.
+
+## Directory structure
+This directory is in working progress -- we are migrating scattered test cases to this directory. Here only lists what's currently under this directory. 
+
+- ```./CBMC```: This directory contains automated proofs of the memory safety of various parts of the FreeRTOS code base.
\ No newline at end of file
diff --git a/FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h b/FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h
index 5e4c51eee..0ca56a7b3 100644
--- a/FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h
+++ b/FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h
@@ -46,10 +46,8 @@ CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  * FreeRTOS_netstat() command, and ping replies.  If ipconfigHAS_PRINTF is set to 1
  * then FreeRTOS_printf should be set to the function used to print out the
  * messages. */
-#define ipconfigHAS_PRINTF    0
-#if ( ipconfigHAS_PRINTF == 1 )
-    #define FreeRTOS_printf( X )    configPRINTF( X )
-#endif
+#define FreeRTOS_printf( X )
+
 
 /* Define the byte order of the target MCU (the MCU FreeRTOS+TCP is executing
  * on).  Valid options are pdFREERTOS_BIG_ENDIAN and pdFREERTOS_LITTLE_ENDIAN. */
@@ -188,7 +186,9 @@ extern uint32_t ulRand();
  * are available to the IP stack.  The total number of network buffers is limited
  * to ensure the total amount of RAM that can be consumed by the IP stack is capped
  * to a pre-determinable value. */
-#define ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS    60
+#ifndef ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS
+	#define ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS    60
+#endif
 
 /* A FreeRTOS queue is used to send events from application tasks to the IP
  * stack.  ipconfigEVENT_QUEUE_LENGTH sets the maximum number of events that can