github-forks
/
FreeRTOS
mirror of https://github.com/FreeRTOS/FreeRTOS.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Remove dependency of CBMC on Patches (#181)

Browse Source 
* 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!
pull/189/head
Aniruddha Kanhere 5 years ago committed by GitHub
parent a7fec906a4
commit 08af68ef90
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
15 changed files with 39 additions and 551 deletions
Show Stats Download Patch File Download Diff File

12
FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c
Unescape Escape View File

@ -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;

18
FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c
Unescape Escape View File

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

15
FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c
Unescape Escape View File

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

4
FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c
Unescape Escape View File

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

4
FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOSIPConfigDefaults.h
Unescape Escape View File

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

64
FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-dhcp.patch
Unescape Escape View File

@ -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;

100
FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-dns.patch
Unescape Escape View File

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

83
FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch
Unescape Escape View File

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

17
FreeRTOS-Plus/Test/CBMC/patches/remove-static-in-freertos-tcp-win.patch
Unescape Escape View File

@ -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;

5
FreeRTOS-Plus/Test/CBMC/proofs/MakefileCommon.json
Unescape Escape View File

@ -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 ": [

64
FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-dhcp.patch
Unescape Escape View File

@ -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;

100
FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-dns.patch
Unescape Escape View File

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

83
FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-ip.patch
Unescape Escape View File

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

17
FreeRTOS/Test/CBMC/patches/remove-static-in-freertos-tcp-win.patch
Unescape Escape View File

@ -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;

4
FreeRTOS/Test/CBMC/proofs/MakefileCommon.json
Unescape Escape View File

@ -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 ": [

Write Preview
Loading…
Cancel
Save