Move CBMC proofs to FreeRTOS+ directory (#64)

* move CBMC proofs to FreeRTOS+ directory

* Failing proofs corrected

* ParseDNSReply proof added back

* removed queue_init.h from -Plus/Test

Co-authored-by: Yuhui Zheng <10982575+yuhui-zheng@users.noreply.github.com>

FreeRTOS-Plus/Test/CBMC/.gitignore

@@ -0,0 +1,5 @@
+cbmc.txt
+property.xml
+coverage.xml
+*.goto
+**/html/*

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.

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()

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()

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()

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

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);
+}

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 );
+}

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();

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 */

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

FreeRTOS-Plus/Test/CBMC/patches/.gitignore

@@ -0,0 +1,2 @@
+auto_patch*
+patched

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)
+

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
+

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;

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;

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;

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. */
+

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)
+

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 */

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 */

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

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.

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)

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()

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")]

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))

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

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();
+	}
+}

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
+)
+

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

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"
+    ]
+}

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"
+    ]
+}

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"
+    ]
+}

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}"
+  ]
+}

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);
+
+}