From 08af68ef9049279b265c3d00e9c48fb9594129a8 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Sat, 1 Aug 2020 16:38:23 -0700 Subject: [PATCH] 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! --- .../Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c | 12 ++- .../Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c | 18 ++-- .../FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c | 15 +-- .../FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c | 4 +- .../include/FreeRTOSIPConfigDefaults.h | 4 + .../remove-static-in-freertos-dhcp.patch | 64 ----------- .../remove-static-in-freertos-dns.patch | 100 ------------------ .../remove-static-in-freertos-tcp-ip.patch | 83 --------------- .../remove-static-in-freertos-tcp-win.patch | 17 --- .../Test/CBMC/proofs/MakefileCommon.json | 5 +- .../remove-static-in-freertos-dhcp.patch | 64 ----------- .../remove-static-in-freertos-dns.patch | 100 ------------------ .../remove-static-in-freertos-tcp-ip.patch | 83 --------------- .../remove-static-in-freertos-tcp-win.patch | 17 --- FreeRTOS/Test/CBMC/proofs/MakefileCommon.json | 4 +- 15 files changed, 39 insertions(+), 551 deletions(-) delete mode 100644 FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-dhcp.patch delete mode 100644 FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-dns.patch delete mode 100644 FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch delete mode 100644 FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-win.patch delete mode 100644 FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-dhcp.patch delete mode 100644 FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-dns.patch delete mode 100644 FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch delete mode 100644 FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-win.patch diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c index 7f59815625..e12db9162c 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 aea9e20463..c63ba537a2 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 754c26a7fd..0ce010d429 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 5f8eb007e4..5adcc9f314 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 6d8e07f215..7194df3eee 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 00b4f4a5b1..0000000000 --- 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 23184684e5..0000000000 --- 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 689ccd7bc7..0000000000 --- a/FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch +++ /dev/null @@ -1,83 +0,0 @@ -From: Aniruddha R Kanhere -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 216a488017..0000000000 --- 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 b900ee64a2..1d49986d2a 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 00b4f4a5b1..0000000000 --- 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 23184684e5..0000000000 --- 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 689ccd7bc7..0000000000 --- a/FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch +++ /dev/null @@ -1,83 +0,0 @@ -From: Aniruddha R Kanhere -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 216a488017..0000000000 --- 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 8f43a20952..c7495bf29b 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 ": [