Remove dependency of CBMC on Patches (#181)

* Changes to DHCP

* CBMC DNS changes

* Changes for TCP_IP

* Changes to TCP_WIN

* Define away static to nothing

* Remove patches

* Changes after Mark's comments v1

* Update MakefileCommon.json

* Correction!

15 files changed, 39 insertions, 551 deletions

diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
index 7f5981562..e12db9162 100644
--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
@@ -39,6 +39,8 @@
 #include "FreeRTOS_DHCP.h"
 #include "FreeRTOS_ARP.h"
 
+#include "FreeRTOSIPConfigDefaults.h"
+
 /* Exclude the entire file if DHCP is not enabled. */
 #if( ipconfigUSE_DHCP != 0 )
 
@@ -153,7 +155,7 @@ struct xDHCPMessage_IPv4
 typedef struct xDHCPMessage_IPv4 DHCPMessage_IPv4_t;
 
 /* The UDP socket used for all incoming and outgoing DHCP traffic. */
-static Socket_t xDHCPSocket;
+_static Socket_t xDHCPSocket;
 
 #if( ipconfigDHCP_FALL_BACK_AUTO_IP != 0 )
 	/* Define the Link Layer IP address: 169.254.x.x */
@@ -176,7 +178,7 @@ static void prvSendDHCPDiscover( void );
 /*
  * Interpret message received on the DHCP socket.
  */
-static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
+_static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
 
 /*
  * Generate a DHCP request packet, and send it on the DHCP socket.
@@ -201,7 +203,7 @@ static uint8_t *prvCreatePartDHCPMessage( struct freertos_sockaddr *pxAddress,
 /*
  * Create the DHCP socket, if it has not been created already.
  */
-static void prvCreateDHCPSocket( void );
+_static void prvCreateDHCPSocket( void );
 
 /*
  * Close the DHCP socket.
@@ -220,7 +222,7 @@ static void prvCloseDHCPSocket( void );
 /*-----------------------------------------------------------*/
 
 /* Hold information in between steps in the DHCP state machine. */
-static DHCPData_t xDHCPData;
+_static DHCPData_t xDHCPData;
 
 /*-----------------------------------------------------------*/
 
@@ -620,7 +622,7 @@ static void prvInitialiseDHCP( void )
 }
 /*-----------------------------------------------------------*/
 
-static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType )
+_static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType )
 {
 uint8_t *pucUDPPayload;
 int32_t lBytes;
diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
index aea9e2046..c63ba537a 100644
--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
@@ -42,6 +42,8 @@
 #include "NetworkBufferManagement.h"
 #include "NetworkInterface.h"
 
+#include "FreeRTOSIPConfigDefaults.h"
+
 /* Exclude the entire file if DNS is not enabled. */
 #if( ipconfigUSE_DNS != 0 )
 
@@ -124,7 +126,7 @@ static Socket_t prvCreateDNSSocket( void );
 /*
  * Create the DNS message in the zero copy buffer passed in the first parameter.
  */
-static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
+_static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
 								   const char *pcHostName,
 								   TickType_t uxIdentifier );
 
@@ -132,7 +134,7 @@ static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
  * Simple routine that jumps over the NAME field of a resource record.
  * It returns the number of bytes read.
  */
-static size_t prvSkipNameField( const uint8_t *pucByte,
+_static size_t prvSkipNameField( const uint8_t *pucByte,
 								size_t uxLength );
 
 /*
@@ -140,7 +142,7 @@ static size_t prvSkipNameField( const 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,
+_static uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
 								  size_t uxBufferLength,
 								  BaseType_t xExpected );
 
@@ -194,7 +196,7 @@ static uint32_t prvGetHostByName( const char *pcHostName,
 
 
 #if( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 )
-	static size_t prvReadNameField( const uint8_t *pucByte,
+	_static size_t prvReadNameField( const uint8_t *pucByte,
 									size_t uxRemainingBytes,
 									char *pcName,
 									size_t uxDestLen );
@@ -790,7 +792,7 @@ TickType_t uxWriteTimeOut_ticks = ipconfigDNS_SEND_BLOCK_TIME_TICKS;
 }
 /*-----------------------------------------------------------*/
 
-static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
+_static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
 								   const char *pcHostName,
 								   TickType_t uxIdentifier )
 {
@@ -871,7 +873,7 @@ static const DNSMessage_t xDefaultPartDNSHeader =
 
 #if( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 )
 
-	static size_t prvReadNameField( const uint8_t *pucByte,
+	_static size_t prvReadNameField( const uint8_t *pucByte,
 									size_t uxRemainingBytes,
 									char *pcName,
 									size_t uxDestLen )
@@ -966,7 +968,7 @@ static const DNSMessage_t xDefaultPartDNSHeader =
 #endif	/* ipconfigUSE_DNS_CACHE || ipconfigDNS_USE_CALLBACKS */
 /*-----------------------------------------------------------*/
 
-static size_t prvSkipNameField( const uint8_t *pucByte,
+_static size_t prvSkipNameField( const uint8_t *pucByte,
 								size_t uxLength )
 {
 size_t uxChunkLength;
@@ -1081,7 +1083,7 @@ size_t uxPayloadSize;
 #endif /* ipconfigUSE_NBNS */
 /*-----------------------------------------------------------*/
 
-static uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
+_static uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
 								  size_t uxBufferLength,
 								  BaseType_t xExpected )
 {
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 754c26a7f..0ce010d42 100644
--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c
+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c
@@ -54,6 +54,9 @@
 #include "FreeRTOS_ARP.h"
 
 
+#include "FreeRTOSIPConfigDefaults.h"
+
+
 /* Just make sure the contents doesn't get compiled if TCP is not enabled. */
 #if ipconfigUSE_TCP == 1
 
@@ -198,14 +201,14 @@ static BaseType_t prvTCPPrepareConnect( FreeRTOS_Socket_t *pxSocket );
 /*
  * Parse the TCP option(s) received, if present.
  */
-static void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const NetworkBufferDescriptor_t *pxNetworkBuffer );
+_static void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const 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 size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
+_static size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
 											 size_t uxTotalLength,
 											 FreeRTOS_Socket_t * const pxSocket,
 											 BaseType_t xHasSYNFlag );
@@ -215,7 +218,7 @@ static size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
 	 * Skip past TCP header options when doing Selective ACK, until there are no
 	 * more options left.
 	 */
-	static void prvReadSackOption( const uint8_t * const pucPtr,
+	_static void prvReadSackOption( const uint8_t * const pucPtr,
 								   size_t uxIndex,
 								   FreeRTOS_Socket_t * const pxSocket );
 #endif/* ( ipconfigUSE_TCP_WIN == 1 ) */
@@ -1139,7 +1142,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, const NetworkBufferDescriptor_t *pxNetworkBuffer )
+_static void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const NetworkBufferDescriptor_t *pxNetworkBuffer )
 {
 size_t uxTCPHeaderOffset = ipSIZE_OF_ETH_HEADER + xIPHeaderSize( pxNetworkBuffer );
 const ProtocolHeaders_t *pxProtocolHeaders = ipPOINTER_CAST( ProtocolHeaders_t *,
@@ -1205,7 +1208,7 @@ uint8_t ucLength;
 }
 /*-----------------------------------------------------------*/
 
-static size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
+_static size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
 											 size_t uxTotalLength,
 											 FreeRTOS_Socket_t * const pxSocket,
 											 BaseType_t xHasSYNFlag )
@@ -1355,7 +1358,7 @@ BaseType_t xReturn = pdFALSE;
 /*-----------------------------------------------------------*/
 
 #if( ipconfigUSE_TCP_WIN == 1 )
-	static void prvReadSackOption( const uint8_t * const pucPtr,
+	_static void prvReadSackOption( const uint8_t * const pucPtr,
 								   size_t uxIndex,
 								   FreeRTOS_Socket_t * const pxSocket )
 	{
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 5f8eb007e..5adcc9f31 100644
--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c
+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c
@@ -46,6 +46,8 @@
 #include "FreeRTOS_Sockets.h"
 #include "FreeRTOS_IP_Private.h"
 
+#include "FreeRTOSIPConfigDefaults.h"
+
 /* Constants used for Smoothed Round Trip Time (SRTT). */
 #define	winSRTT_INCREMENT_NEW 		2
 #define winSRTT_INCREMENT_CURRENT 	6
@@ -192,7 +194,7 @@ static void vListInsertGeneric( List_t * const pxList, ListItem_t * const pxNewL
 
 /* List of free TCP segments. */
 #if( ipconfigUSE_TCP_WIN == 1 )
-	static List_t xSegmentList;
+	_static List_t xSegmentList;
 #endif
 
 /* Logging verbosity level. */
diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOSIPConfigDefaults.h b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOSIPConfigDefaults.h
index 6d8e07f21..7194df3ee 100644
--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOSIPConfigDefaults.h
+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOSIPConfigDefaults.h
@@ -36,6 +36,10 @@ will be removed. */
 /* This file provides default values for configuration options that are missing
 from the FreeRTOSIPConfig.h configuration header file. */
 
+/* These macros are used to define away static keyword for CBMC proofs */
+#ifndef _static
+	#define _static static
+#endif
 
 /* Ensure defined configuration constants are using the most up to date naming. */
 #ifdef tcpconfigIP_TIME_TO_LIVE
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-dhcp.patch b/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-dhcp.patch
deleted file mode 100644
index 00b4f4a5b..000000000
--- a/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-dhcp.patch
+++ /dev/null
@@ -1,64 +0,0 @@
-diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
-index 04b0487..d6e74a9 100644
---- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
-+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
-@@ -156,7 +156,11 @@ struct xDHCPMessage_IPv4
- typedef struct xDHCPMessage_IPv4 DHCPMessage_IPv4_t;
- 
- /* The UDP socket used for all incoming and outgoing DHCP traffic. */
-+#ifdef CBMC
-+Socket_t xDHCPSocket;
-+#else
- static Socket_t xDHCPSocket;
-+#endif
- 
- #if( ipconfigDHCP_FALL_BACK_AUTO_IP != 0 )
- 	/* Define the Link Layer IP address: 169.254.x.x */
-@@ -179,7 +183,11 @@ static void prvSendDHCPDiscover( void );
- /*
-  * Interpret message received on the DHCP socket.
-  */
-+#ifdef CBMC
-+BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
-+#else
- static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
-+#endif
- 
- /*
-  * Generate a DHCP request packet, and send it on the DHCP socket.
-@@ -204,7 +212,11 @@ static uint8_t *prvCreatePartDHCPMessage( struct freertos_sockaddr *pxAddress,
- /*
-  * Create the DHCP socket, if it has not been created already.
-  */
-+#ifdef CBMC
-+void prvCreateDHCPSocket( void );
-+#else
- static void prvCreateDHCPSocket( void );
-+#endif
- 
- /*
-  * Close the DHCP socket.
-@@ -223,7 +235,11 @@ static void prvCloseDHCPSocket( void );
- /*-----------------------------------------------------------*/
- 
- /* Hold information in between steps in the DHCP state machine. */
-+#ifdef CBMC
-+DHCPData_t xDHCPData;
-+#else
- static DHCPData_t xDHCPData;
-+#endif
- 
- /*-----------------------------------------------------------*/
- 
-@@ -623,7 +639,11 @@ static void prvInitialiseDHCP( void )
- }
- /*-----------------------------------------------------------*/
- 
-+#ifdef CBMC
-+BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType )
-+#else
- static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType )
-+#endif
- {
- uint8_t *pucUDPPayload;
- int32_t lBytes;
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-dns.patch b/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-dns.patch
deleted file mode 100644
index 23184684e..000000000
--- a/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-dns.patch
+++ /dev/null
@@ -1,100 +0,0 @@
-diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
-index 480d50b..5557253 100644
---- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
-+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
-@@ -114,7 +114,11 @@ static Socket_t prvCreateDNSSocket( void );
- /*
-  * Create the DNS message in the zero copy buffer passed in the first parameter.
-  */
-+#ifdef CBMC
-+size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
-+#else
- static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
-+#endif
- 								   const char *pcHostName,
- 								   TickType_t uxIdentifier );
- 
-@@ -122,7 +126,11 @@ static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
-  * Simple routine that jumps over the NAME field of a resource record.
-  * It returns the number of bytes read.
-  */
-+#ifdef CBMC
-+size_t prvSkipNameField( const uint8_t *pucByte,
-+#else
- static size_t prvSkipNameField( const uint8_t *pucByte,
-+#endif
- 								size_t uxLength );
- 
- /*
-@@ -130,7 +138,11 @@ static size_t prvSkipNameField( const 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.
-  */
-+#ifdef CBMC
-+uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
-+#else
- static uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
-+#endif
- 								  size_t uxBufferLength,
- 								  BaseType_t xExpected );
- 
-@@ -184,7 +196,11 @@ static uint32_t prvGetHostByName( const char *pcHostName,
- 
- 
- #if( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 )
-+#ifdef CBMC
-+	size_t prvReadNameField( const uint8_t *pucByte,
-+#else
- 	static size_t prvReadNameField( const uint8_t *pucByte,
-+#endif
- 									size_t uxRemainingBytes,
- 									char *pcName,
- 									size_t uxDestLen );
-@@ -758,7 +774,11 @@ TickType_t uxWriteTimeOut_ticks = ipconfigDNS_SEND_BLOCK_TIME_TICKS;
- }
- /*-----------------------------------------------------------*/
- 
-+#ifdef CBMC
-+size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
-+#else
- static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
-+#endif
- 								   const char *pcHostName,
- 								   TickType_t uxIdentifier )
- {
-@@ -838,7 +858,11 @@ static const DNSMessage_t xDefaultPartDNSHeader =
- 
- #if( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 )
- 
-+#ifdef CBMC
-+	size_t prvReadNameField( const uint8_t *pucByte,
-+#else
- 	static size_t prvReadNameField( const uint8_t *pucByte,
-+#endif
- 									size_t uxRemainingBytes,
- 									char *pcName,
- 									size_t uxDestLen )
-@@ -932,7 +956,11 @@ static const DNSMessage_t xDefaultPartDNSHeader =
- #endif	/* ipconfigUSE_DNS_CACHE || ipconfigDNS_USE_CALLBACKS */
- /*-----------------------------------------------------------*/
- 
-+#ifdef CBMC
-+size_t prvSkipNameField( const uint8_t *pucByte,
-+#else
- static size_t prvSkipNameField( const uint8_t *pucByte,
-+#endif
- 								size_t uxLength )
- {
- size_t uxChunkLength;
-@@ -1050,7 +1078,11 @@ size_t uxPayloadSize;
- #endif /* ipconfigUSE_NBNS */
- /*-----------------------------------------------------------*/
- 
-+#ifdef CBMC
-+uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
-+#else
- static uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
-+#endif
- 								  size_t uxBufferLength,
- 								  BaseType_t xExpected )
- {
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch b/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch
deleted file mode 100644
index 689ccd7bc..000000000
--- a/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch
+++ /dev/null
@@ -1,83 +0,0 @@
-From: Aniruddha R Kanhere <kanherea@amazon.com>
-Date: Wed, 03 June 2020 09:51:25 +0000
-Subject: [PATCH] modified lib
-
----
- .../freertos_plus_tcp/source/FreeRTOS_TCP_IP.c     | 24 ++++++++++++++++++++++
- 1 file changed, 24 insertions(+)
-
-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 7a2c00c68..cb537b347 100644
---- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c
-+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c
-@@ -198,14 +198,22 @@ static BaseType_t prvTCPPrepareConnect( FreeRTOS_Socket_t *pxSocket );
- /*
-  * Parse the TCP option(s) received, if present.
-  */
-+#ifdef CBMC
-+void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const NetworkBufferDescriptor_t *pxNetworkBuffer );
-+#else
- static void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const NetworkBufferDescriptor_t *pxNetworkBuffer );
-+#endif
- 
- /*
-  * 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.
-  */
-+#ifdef CBMC
-+size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
-+#else
- static size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
-+#endif
- 											 size_t uxTotalLength,
- 											 FreeRTOS_Socket_t * const pxSocket,
- 											 BaseType_t xHasSYNFlag );
-@@ -215,7 +223,11 @@ static size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
- 	 * Skip past TCP header options when doing Selective ACK, until there are no
- 	 * more options left.
- 	 */
-+	#ifdef CBMC
-+	void prvReadSackOption( const uint8_t * const pucPtr,
-+	#else
- 	static void prvReadSackOption( const uint8_t * const pucPtr,
-+	#endif
- 								   size_t uxIndex,
- 								   FreeRTOS_Socket_t * const pxSocket );
- #endif/* ( ipconfigUSE_TCP_WIN == 1 ) */
-@@ -1137,7 +1149,11 @@ uint32_t ulInitialSequenceNumber = 0;
-  * that: ((pxTCPHeader->ucTCPOffset & 0xf0) > 0x50), meaning that the TP header
-  * is longer than the usual 20 (5 x 4) bytes.
-  */
-+#ifdef CBMC
-+void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const NetworkBufferDescriptor_t *pxNetworkBuffer )
-+#else
- static void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const NetworkBufferDescriptor_t *pxNetworkBuffer )
-+#endif
- {
- size_t uxTCPHeaderOffset = ipSIZE_OF_ETH_HEADER + xIPHeaderSize( pxNetworkBuffer );
- const ProtocolHeaders_t *pxProtocolHeaders = ipPOINTER_CAST( ProtocolHeaders_t *,
-@@ -1199,7 +1215,11 @@ uint8_t ucLength;
- }
- /*-----------------------------------------------------------*/
- 
-+#ifdef CBMC
-+size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
-+#else
- static size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
-+#endif
- 											 size_t uxTotalLength,
- 											 FreeRTOS_Socket_t * const pxSocket,
- 											 BaseType_t xHasSYNFlag )
-@@ -1331,7 +1351,11 @@ TCPWindow_t *pxTCPWindow = &( pxSocket->u.xTCP.xTCPWindow );
- /*-----------------------------------------------------------*/
- 
- #if( ipconfigUSE_TCP_WIN == 1 )
-+	#ifdef CBMC
-+	void prvReadSackOption( const uint8_t * const pucPtr,
-+	#else
- 	static void prvReadSackOption( const uint8_t * const pucPtr,
-+	#endif
- 								   size_t uxIndex,
- 								   FreeRTOS_Socket_t * const pxSocket )
- 	{
diff --git a/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-win.patch b/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-win.patch
deleted file mode 100644
index 216a48801..000000000
--- a/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-win.patch
+++ /dev/null
@@ -1,17 +0,0 @@
-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 0078ab313..b0cccbad8 100644
---- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c
-+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c
-@@ -192,8 +192,12 @@ extern void vListInsertGeneric( List_t * const pxList, ListItem_t * const pxNewL
- 
- /* List of free TCP segments. */
- #if( ipconfigUSE_TCP_WIN == 1 )
-+#ifdef CBMC
-+	List_t xSegmentList;
-+#else
- 	static List_t xSegmentList;
- #endif
-+#endif
- 
- /* Logging verbosity level. */
- BaseType_t xTCPWindowLoggingLevel = 0;
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json
index b900ee64a..1d49986d2 100644
--- a/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json
@@ -3,7 +3,6 @@
     "PROOFS": [ "." ],
 
     "DEF ": [
-    
 	"WIN32",
 	"WINVER=0x400",
 	"_CONSOLE",
@@ -15,7 +14,9 @@
 
         "CBMC",
 	"'configASSERT(X)=__CPROVER_assert(X,\"Assertion Error\")'",
-        "'configPRECONDITION(X)=__CPROVER_assume(X)'"
+        "'configPRECONDITION(X)=__CPROVER_assume(X)'",
+	"'_static='",
+	"'_volatile='"
     ],
 
   "INC ": [
diff --git a/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-dhcp.patch b/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-dhcp.patch
deleted file mode 100644
index 00b4f4a5b..000000000
--- a/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-dhcp.patch
+++ /dev/null
@@ -1,64 +0,0 @@
-diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
-index 04b0487..d6e74a9 100644
---- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
-+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
-@@ -156,7 +156,11 @@ struct xDHCPMessage_IPv4
- typedef struct xDHCPMessage_IPv4 DHCPMessage_IPv4_t;
- 
- /* The UDP socket used for all incoming and outgoing DHCP traffic. */
-+#ifdef CBMC
-+Socket_t xDHCPSocket;
-+#else
- static Socket_t xDHCPSocket;
-+#endif
- 
- #if( ipconfigDHCP_FALL_BACK_AUTO_IP != 0 )
- 	/* Define the Link Layer IP address: 169.254.x.x */
-@@ -179,7 +183,11 @@ static void prvSendDHCPDiscover( void );
- /*
-  * Interpret message received on the DHCP socket.
-  */
-+#ifdef CBMC
-+BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
-+#else
- static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
-+#endif
- 
- /*
-  * Generate a DHCP request packet, and send it on the DHCP socket.
-@@ -204,7 +212,11 @@ static uint8_t *prvCreatePartDHCPMessage( struct freertos_sockaddr *pxAddress,
- /*
-  * Create the DHCP socket, if it has not been created already.
-  */
-+#ifdef CBMC
-+void prvCreateDHCPSocket( void );
-+#else
- static void prvCreateDHCPSocket( void );
-+#endif
- 
- /*
-  * Close the DHCP socket.
-@@ -223,7 +235,11 @@ static void prvCloseDHCPSocket( void );
- /*-----------------------------------------------------------*/
- 
- /* Hold information in between steps in the DHCP state machine. */
-+#ifdef CBMC
-+DHCPData_t xDHCPData;
-+#else
- static DHCPData_t xDHCPData;
-+#endif
- 
- /*-----------------------------------------------------------*/
- 
-@@ -623,7 +639,11 @@ static void prvInitialiseDHCP( void )
- }
- /*-----------------------------------------------------------*/
- 
-+#ifdef CBMC
-+BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType )
-+#else
- static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType )
-+#endif
- {
- uint8_t *pucUDPPayload;
- int32_t lBytes;
diff --git a/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-dns.patch b/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-dns.patch
deleted file mode 100644
index 23184684e..000000000
--- a/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-dns.patch
+++ /dev/null
@@ -1,100 +0,0 @@
-diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
-index 480d50b..5557253 100644
---- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
-+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
-@@ -114,7 +114,11 @@ static Socket_t prvCreateDNSSocket( void );
- /*
-  * Create the DNS message in the zero copy buffer passed in the first parameter.
-  */
-+#ifdef CBMC
-+size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
-+#else
- static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
-+#endif
- 								   const char *pcHostName,
- 								   TickType_t uxIdentifier );
- 
-@@ -122,7 +126,11 @@ static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
-  * Simple routine that jumps over the NAME field of a resource record.
-  * It returns the number of bytes read.
-  */
-+#ifdef CBMC
-+size_t prvSkipNameField( const uint8_t *pucByte,
-+#else
- static size_t prvSkipNameField( const uint8_t *pucByte,
-+#endif
- 								size_t uxLength );
- 
- /*
-@@ -130,7 +138,11 @@ static size_t prvSkipNameField( const 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.
-  */
-+#ifdef CBMC
-+uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
-+#else
- static uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
-+#endif
- 								  size_t uxBufferLength,
- 								  BaseType_t xExpected );
- 
-@@ -184,7 +196,11 @@ static uint32_t prvGetHostByName( const char *pcHostName,
- 
- 
- #if( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 )
-+#ifdef CBMC
-+	size_t prvReadNameField( const uint8_t *pucByte,
-+#else
- 	static size_t prvReadNameField( const uint8_t *pucByte,
-+#endif
- 									size_t uxRemainingBytes,
- 									char *pcName,
- 									size_t uxDestLen );
-@@ -758,7 +774,11 @@ TickType_t uxWriteTimeOut_ticks = ipconfigDNS_SEND_BLOCK_TIME_TICKS;
- }
- /*-----------------------------------------------------------*/
- 
-+#ifdef CBMC
-+size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
-+#else
- static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer,
-+#endif
- 								   const char *pcHostName,
- 								   TickType_t uxIdentifier )
- {
-@@ -838,7 +858,11 @@ static const DNSMessage_t xDefaultPartDNSHeader =
- 
- #if( ipconfigUSE_DNS_CACHE == 1 ) || ( ipconfigDNS_USE_CALLBACKS == 1 )
- 
-+#ifdef CBMC
-+	size_t prvReadNameField( const uint8_t *pucByte,
-+#else
- 	static size_t prvReadNameField( const uint8_t *pucByte,
-+#endif
- 									size_t uxRemainingBytes,
- 									char *pcName,
- 									size_t uxDestLen )
-@@ -932,7 +956,11 @@ static const DNSMessage_t xDefaultPartDNSHeader =
- #endif	/* ipconfigUSE_DNS_CACHE || ipconfigDNS_USE_CALLBACKS */
- /*-----------------------------------------------------------*/
- 
-+#ifdef CBMC
-+size_t prvSkipNameField( const uint8_t *pucByte,
-+#else
- static size_t prvSkipNameField( const uint8_t *pucByte,
-+#endif
- 								size_t uxLength )
- {
- size_t uxChunkLength;
-@@ -1050,7 +1078,11 @@ size_t uxPayloadSize;
- #endif /* ipconfigUSE_NBNS */
- /*-----------------------------------------------------------*/
- 
-+#ifdef CBMC
-+uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
-+#else
- static uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer,
-+#endif
- 								  size_t uxBufferLength,
- 								  BaseType_t xExpected )
- {
diff --git a/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch b/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch
deleted file mode 100644
index 689ccd7bc..000000000
--- a/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch
+++ /dev/null
@@ -1,83 +0,0 @@
-From: Aniruddha R Kanhere <kanherea@amazon.com>
-Date: Wed, 03 June 2020 09:51:25 +0000
-Subject: [PATCH] modified lib
-
----
- .../freertos_plus_tcp/source/FreeRTOS_TCP_IP.c     | 24 ++++++++++++++++++++++
- 1 file changed, 24 insertions(+)
-
-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 7a2c00c68..cb537b347 100644
---- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c
-+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c
-@@ -198,14 +198,22 @@ static BaseType_t prvTCPPrepareConnect( FreeRTOS_Socket_t *pxSocket );
- /*
-  * Parse the TCP option(s) received, if present.
-  */
-+#ifdef CBMC
-+void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const NetworkBufferDescriptor_t *pxNetworkBuffer );
-+#else
- static void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const NetworkBufferDescriptor_t *pxNetworkBuffer );
-+#endif
- 
- /*
-  * 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.
-  */
-+#ifdef CBMC
-+size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
-+#else
- static size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
-+#endif
- 											 size_t uxTotalLength,
- 											 FreeRTOS_Socket_t * const pxSocket,
- 											 BaseType_t xHasSYNFlag );
-@@ -215,7 +223,11 @@ static size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
- 	 * Skip past TCP header options when doing Selective ACK, until there are no
- 	 * more options left.
- 	 */
-+	#ifdef CBMC
-+	void prvReadSackOption( const uint8_t * const pucPtr,
-+	#else
- 	static void prvReadSackOption( const uint8_t * const pucPtr,
-+	#endif
- 								   size_t uxIndex,
- 								   FreeRTOS_Socket_t * const pxSocket );
- #endif/* ( ipconfigUSE_TCP_WIN == 1 ) */
-@@ -1137,7 +1149,11 @@ uint32_t ulInitialSequenceNumber = 0;
-  * that: ((pxTCPHeader->ucTCPOffset & 0xf0) > 0x50), meaning that the TP header
-  * is longer than the usual 20 (5 x 4) bytes.
-  */
-+#ifdef CBMC
-+void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const NetworkBufferDescriptor_t *pxNetworkBuffer )
-+#else
- static void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, const NetworkBufferDescriptor_t *pxNetworkBuffer )
-+#endif
- {
- size_t uxTCPHeaderOffset = ipSIZE_OF_ETH_HEADER + xIPHeaderSize( pxNetworkBuffer );
- const ProtocolHeaders_t *pxProtocolHeaders = ipPOINTER_CAST( ProtocolHeaders_t *,
-@@ -1199,7 +1215,11 @@ uint8_t ucLength;
- }
- /*-----------------------------------------------------------*/
- 
-+#ifdef CBMC
-+size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
-+#else
- static size_t prvSingleStepTCPHeaderOptions( const uint8_t * const pucPtr,
-+#endif
- 											 size_t uxTotalLength,
- 											 FreeRTOS_Socket_t * const pxSocket,
- 											 BaseType_t xHasSYNFlag )
-@@ -1331,7 +1351,11 @@ TCPWindow_t *pxTCPWindow = &( pxSocket->u.xTCP.xTCPWindow );
- /*-----------------------------------------------------------*/
- 
- #if( ipconfigUSE_TCP_WIN == 1 )
-+	#ifdef CBMC
-+	void prvReadSackOption( const uint8_t * const pucPtr,
-+	#else
- 	static void prvReadSackOption( const uint8_t * const pucPtr,
-+	#endif
- 								   size_t uxIndex,
- 								   FreeRTOS_Socket_t * const pxSocket )
- 	{
diff --git a/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-win.patch b/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-win.patch
deleted file mode 100644
index 216a48801..000000000
--- a/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-win.patch
+++ /dev/null
@@ -1,17 +0,0 @@
-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 0078ab313..b0cccbad8 100644
---- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c
-+++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c
-@@ -192,8 +192,12 @@ extern void vListInsertGeneric( List_t * const pxList, ListItem_t * const pxNewL
- 
- /* List of free TCP segments. */
- #if( ipconfigUSE_TCP_WIN == 1 )
-+#ifdef CBMC
-+	List_t xSegmentList;
-+#else
- 	static List_t xSegmentList;
- #endif
-+#endif
- 
- /* Logging verbosity level. */
- BaseType_t xTCPWindowLoggingLevel = 0;
diff --git a/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json b/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json
index 8f43a2095..c7495bf29 100644
--- a/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json
+++ b/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json
@@ -12,7 +12,9 @@
 	"__PRETTY_FUNCTION__=__FUNCTION__",
          "CBMC",
 	"'configASSERT(X)=__CPROVER_assert(X,\"Assertion Error\")'",
-    "'configPRECONDITION(X)=__CPROVER_assume(X)'"
+    	"'configPRECONDITION(X)=__CPROVER_assume(X)'",
+	"'_static='",
+	"'_volatile='"
     ],
 
     "INC ": [