diff options
Diffstat (limited to 'FreeRTOS-Plus/Test/CBMC/proofs/ARP')
36 files changed, 821 insertions, 0 deletions
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c new file mode 100644 index 000000000..523783564 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c @@ -0,0 +1,22 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +//We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. +//This is the mock to mimic the correct expected bahvior. If this allocation fails, this might invalidate the proof. +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + NetworkBufferDescriptor_t *pxNetworkBuffer = (NetworkBufferDescriptor_t *) malloc(sizeof(NetworkBufferDescriptor_t)); + pxNetworkBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + return pxNetworkBuffer; +} + +void harness() +{ + vARPAgeCache(); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json new file mode 100644 index 000000000..83c351d70 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json @@ -0,0 +1,18 @@ +{ + "ENTRY": "ARPAgeCache", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPAgeCache.0:7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md new file mode 100644 index 000000000..3352f8096 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPAgeCache/README.md @@ -0,0 +1,2 @@ +Assuming that xNetworkInterfaceOutput is memory safe, +this harness proves the memory safety of the vARPAgeCache function. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c new file mode 100644 index 000000000..3ec9500cc --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c @@ -0,0 +1,28 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + /* + * The assumption made here is that the buffer pointed by pucEthernerBuffer + * is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer. + * This is not checked inside vARPGenerateRequestPacket. + */ + uint8_t ucBUFFER_SIZE; + __CPROVER_assume( ucBUFFER_SIZE >= sizeof(ARPPacket_t) && ucBUFFER_SIZE < 2 * sizeof(ARPPacket_t) ); + void *xBuffer = malloc(ucBUFFER_SIZE); + + NetworkBufferDescriptor_t xNetworkBuffer2; + xNetworkBuffer2.pucEthernetBuffer = xBuffer; + xNetworkBuffer2.xDataLength = ucBUFFER_SIZE; + + /* vARPGenerateRequestPacket asserts buffer has room for a packet */ + __CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof(ARPPacket_t) ); + vARPGenerateRequestPacket( &xNetworkBuffer2 ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json new file mode 100644 index 000000000..65c352489 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json @@ -0,0 +1,15 @@ +{ + "ENTRY": "ARPGenerateRequestPacket", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md new file mode 100644 index 000000000..f8fdcc97d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md @@ -0,0 +1,3 @@ +Given that the pointer target of xNetworkDescriptor.pucEthernetBuffer is allocated +to the size claimed in xNetworkDescriptor.xDataLength, +this harness proves the memory safety of ARPGenerateRequestPacket.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c new file mode 100644 index 000000000..bf188efa1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c @@ -0,0 +1,17 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + + +void harness() +{ + uint32_t ulIPAddress; + MACAddress_t xMACAddress; + + eARPGetCacheEntry( &ulIPAddress, &xMACAddress ); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json new file mode 100644 index 000000000..ecc95a87f --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json @@ -0,0 +1,41 @@ +{ + "ENTRY": "ARPGetCacheEntry", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvCacheLookup.0:7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + { + "ARPGetCacheEntry_default":[ + "ipconfigARP_STORES_REMOTE_ADDRESSES=0", + "ipconfigUSE_LLMNR=0" + ] + }, + { + "ARPGetCacheEntry_LLMNR": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=0", + "ipconfigUSE_LLMNR=1" + ] + }, + { + "ARPGetCacheEntry_STORE_REMOTE": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=1", + "ipconfigUSE_LLMNR=0" + ] + }, + { + "ARPGetCacheEntry_REMOTE_LLMNR": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=1", + "ipconfigUSE_LLMNR=1" + ] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md new file mode 100644 index 000000000..03e987ebd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md @@ -0,0 +1,4 @@ +The combined proofs in the subdirectories prove that ARPGetCacheEntry +is memory safe for all possible combinations of ipconfigARP_STORES_REMOTE_ADDRESSES +and ipconfigUSE_LLMNR. These are the only configuration +parameters used inside the ARPGetCacheEntry. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c new file mode 100644 index 000000000..442b1df6b --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c @@ -0,0 +1,14 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness(){ + MACAddress_t xMACAddress; + uint32_t ulIPAddress; + eARPGetCacheEntryByMac( &xMACAddress, &ulIPAddress ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json new file mode 100644 index 000000000..0f589a8e2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json @@ -0,0 +1,17 @@ +{ + "ENTRY": "ARPGetCacheEntryByMac", + "CBMCFLAGS": + [ + "--unwind 7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + "ipconfigUSE_ARP_REVERSED_LOOKUP=1", "ipconfigARP_CACHE_ENTRIES=6" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md new file mode 100644 index 000000000..77c17e2e9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md @@ -0,0 +1,4 @@ +ARPGetCacheEntryByMac is memory safe, +if it is enabled. + +ARPGetCacheEntryByMac does not use multiple configurations internally. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c new file mode 100644 index 000000000..f2d8e61ae --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c @@ -0,0 +1,15 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + ARPPacket_t xARPFrame; + + eARPProcessPacket( &xARPFrame ); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json new file mode 100644 index 000000000..48d5d83c9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json @@ -0,0 +1,19 @@ +{ + "ENTRY": "ARPProcessPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]}, + {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]} + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md new file mode 100644 index 000000000..0197851b1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md @@ -0,0 +1,4 @@ +The proofs in the subdirectories show that +ARPProcessPacket is memory safe independent +of the configuration value of +ipconfigARP_USE_CLASH_DETECTION.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c new file mode 100644 index 000000000..6664d3cd0 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c @@ -0,0 +1,15 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + MACAddress_t xMACAddress; + uint32_t ulIPAddress; + vARPRefreshCacheEntry( &xMACAddress, ulIPAddress ); + vARPRefreshCacheEntry( NULL, ulIPAddress ); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json new file mode 100644 index 000000000..6cde60a51 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json @@ -0,0 +1,19 @@ +{ + "ENTRY": "ARPRefreshCacheEntry", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + {"NOT_STORE_REMOTE":["ipconfigARP_STORES_REMOTE_ADDRESSES=0"]}, + {"STORE_REMOTE":["ipconfigARP_STORES_REMOTE_ADDRESSES=1"]} + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md new file mode 100644 index 000000000..0f84300cf --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md @@ -0,0 +1,4 @@ +The proofs in this directory guarantee together that +ARPRefreshCacheEntry is memory safe independent +of the configuration value of +ipconfigARP_STORES_REMOTE_ADDRESSES. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c new file mode 100644 index 000000000..fd02b10a2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c @@ -0,0 +1,13 @@ +// /* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + + +void harness() +{ + vARPSendGratuitous(); +}
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json new file mode 100644 index 000000000..1f9616ef8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json @@ -0,0 +1,18 @@ +{ + "ENTRY": "ARPSendGratuitous", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md new file mode 100644 index 000000000..5bb155221 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md @@ -0,0 +1,6 @@ +Abstracting xQueueGenericSend away +and including tasks.c and FreeRTOS_IP.c: +The ARPSendGratutious function is memory safe, +if xQueueGenericSend is memory safe. + +queue.c is not compiled into the proof binary.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c new file mode 100644 index 000000000..957720133 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c @@ -0,0 +1,13 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + FreeRTOS_ClearARP(); +} + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json new file mode 100644 index 000000000..332106c4e --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json @@ -0,0 +1,15 @@ +{ + "ENTRY": "ClearARP", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md new file mode 100644 index 000000000..2447722c9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md @@ -0,0 +1,2 @@ +This proof demonstrates the memory safety of the ClearARP function in the FreeRTOS_ARP.c file. +No restrictions are made.
\ No newline at end of file diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json new file mode 100644 index 000000000..13792bb68 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json @@ -0,0 +1,57 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person +# obtaining a copy of this software and associated documentation +# files (the "Software"), to deal in the Software without +# restriction, including without limitation the rights to use, copy, +# modify, merge, publish, distribute, sublicense, and/or sell copies +# of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be +# included in all copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS +# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN +# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# +# http://aws.amazon.com/freertos +# http://www.FreeRTOS.org +# + +{ + "ENTRY": "OutputARPRequest", + "CBMCFLAGS": + [ + "--unwind 20" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + #That is the minimal required size for an ARPPacket_t plus offset in the buffer. + "MINIMUM_PACKET_BYTES": 50, + "DEF": + [ + { + "CBMC_PROOF_ASSUMPTION_HOLDS_Packet_bytes": [ + "CBMC_PROOF_ASSUMPTION_HOLDS=1", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + ] + }, + { + "CBMC_PROOF_ASSUMPTION_HOLDS_no_packet_bytes": ["CBMC_PROOF_ASSUMPTION_HOLDS=1"] + }, + { + "CBMC_PROOF_ASSUMPTION_DOES_NOT_HOLD": ["CBMC_PROOF_ASSUMPTION_HOLDS=0"] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c new file mode 100644 index 000000000..472f6b1e1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c @@ -0,0 +1,76 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + + +ARPPacket_t xARPPacket; +NetworkBufferDescriptor_t xNetworkBuffer; + +/* STUB! + * We assume that the pxGetNetworkBufferWithDescriptor function is + * implemented correctly and returns a valid data structure. + * This is the mock to mimic the expected behavior. + * If this allocation fails, this might invalidate the proof. + * FreeRTOS_OutputARPRequest calls pxGetNetworkBufferWithDescriptor + * to get a NetworkBufferDescriptor. Then it calls vARPGenerateRequestPacket + * passing this buffer along in the function call. vARPGenerateRequestPacket + * casts the pointer xNetworkBuffer.pucEthernetBuffer into an ARPPacket_t pointer + * and writes a complete ARPPacket to it. Therefore the buffer has to be at least of the size + * of an ARPPacket to gurantee memory safety. + */ +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + #ifdef CBMC_PROOF_ASSUMPTION_HOLDS + #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES + xNetworkBuffer.pucEthernetBuffer = malloc(ipconfigETHERNET_MINIMUM_PACKET_BYTES); + #else + xNetworkBuffer.pucEthernetBuffer = malloc(xRequestedSizeBytes); + #endif + #else + uint32_t malloc_size; + __CPROVER_assert(!__CPROVER_overflow_mult(2, xRequestedSizeBytes)); + __CPROVER_assume(malloc_size > 0 && malloc_size < 2 * xRequestedSizeBytes); + xNetworkBuffer.pucEthernetBuffer = malloc(malloc_size); + #endif + xNetworkBuffer.xDataLength = xRequestedSizeBytes; + return &xNetworkBuffer; +} + + +void harness() +{ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md new file mode 100644 index 000000000..8a868dda1 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md @@ -0,0 +1,29 @@ +This is the memory safety proof for FreeRTOS_OutputARPRequest. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* xNetworkInterfaceOutput + +This proof checks FreeRTOS_OutputARPRequest in multiple configuration: + +* The config_CBMC_PROOF_ASSUMPTION_HOLDS_no_packet_bytes proof + guarantees that for a buffer allocated to xDataLength, + the code executed by the FreeRTOS_OutputARPRequest function + call of FreeRTOS_ARP.c is memory safe. +* If the ipconfigETHERNET_MINIMUM_PACKET_BYTES is set and the + buffer allocated by pxGetNetworkBufferWithDescriptor allocates + a buffer of at least ipconfigETHERNET_MINIMUM_PACKET_BYTES, + the config_CBMC_PROOF_ASSUMPTION_HOLDS_Packet_bytes proof + guarantees that the code executed by the + FreeRTOS_OutputARPRequest function call + of FreeRTOS_ARP.c is memory safe. +* The third configuration in the subdirectory + config_CBMC_PROOF_ASSUMPTION_DOES_NOT_HOLD demonstrates + that the code is not memory safe, if the allocation + code violates our assumption. +* All proofs mock the pxGetNetworkBufferWithDescriptor + function for modelling the assumptions about the + buffer management layer. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c new file mode 100644 index 000000000..4975d66ee --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c @@ -0,0 +1,14 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOSIPConfig.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + FreeRTOS_PrintARPCache(); +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json new file mode 100644 index 000000000..6588b10d9 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json @@ -0,0 +1,17 @@ +{ + "ENTRY": "FreeRTOS_PrintARPCache", + "CBMCFLAGS": + [ + "--unwind 7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + "ipconfigARP_CACHE_ENTRIES=6" + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md new file mode 100644 index 000000000..2c44908cd --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md @@ -0,0 +1,4 @@ +FreeRTOS_PrintARPCache_harness.c is memory safe, +assuming vLoggingPrintf is correct and memory safe. + +FreeRTOS_PrintARPCache does not use multiple configurations. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json new file mode 100644 index 000000000..ed1a2aca8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json @@ -0,0 +1,47 @@ +{ + "ENTRY": "OutputARPRequest", + "MINIMUM_PACKET_BYTES": 50, + "CBMCFLAGS": + [ + "--unwind {MINIMUM_PACKET_BYTES}", + "--unwindset xNetworkBuffersInitialise.0:3,xNetworkBuffersInitialise.1:3,vListInsert.0:3,pxGetNetworkBufferWithDescriptor.0:3,pxGetNetworkBufferWithDescriptor.1:3,vNetworkInterfaceAllocateRAMToBuffers.0:3" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_1.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Source/queue.goto" + ], + "DEF": + [ + { + "minimal_configuration": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=0" + ] + }, + { + "minimal_configuration_minimal_packet_size": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + ] + }, + { + "minimal_configuration_linked_rx_messages": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=1" + ] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c new file mode 100644 index 000000000..3dae34a34 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c @@ -0,0 +1,71 @@ +/* This harness is linked against + * libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_1.goto + */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#if( ipconfigUSE_LLMNR == 1 ) + #include "FreeRTOS_DNS.h" +#endif /* ipconfigUSE_LLMNR */ +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" + +void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] ){ + for(int x = 0; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS; x++){ + NetworkBufferDescriptor_t *current = &pxNetworkBuffers[x]; + #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES + current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t) + (ipconfigETHERNET_MINIMUM_PACKET_BYTES- sizeof(ARPPacket_t))); + #else + current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t)); + #endif + current->xDataLength = sizeof(ARPPacket_t); + } +} + +/* The code expects that the Semaphore creation relying on pvPortMalloc + is successful. This is checked by an assert statement, that gets + triggered when the allocation fails. Nevertheless, the code is perfectly + guarded against a failing Semaphore allocation. To make the assert pass, + it is assumed for now, that pvPortMalloc doesn't fail. Using a model allowing + failures of the allocation might be possible + after removing the assert in l.105 of BufferAllocation_1.c, from a memory + safety point of view. */ +void *pvPortMalloc( size_t xWantedSize ){ + return malloc(xWantedSize); +} + +/* + * This function is implemented by a third party. + * After looking through a couple of samples in the demos folder, it seems + * like the only shared contract is that you want to add the if statement + * for releasing the buffer to the end. Apart from that, it is up to the vendor, + * how to write this code out to the network. + */ +BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){ + if( bReleaseAfterSend != pdFALSE ) + { + vReleaseNetworkBufferAndDescriptor( pxDescriptor ); + } +} + +void harness() +{ + BaseType_t xRes = xNetworkBuffersInitialise(); + if(xRes == pdPASS){ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); + } +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md new file mode 100644 index 000000000..ea5eac78d --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md @@ -0,0 +1,27 @@ +This is the memory safety proof for ```FreeRTOS_OutputARPRequest``` +method combined with the BufferAllocation_1.c allocation strategy. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* vPortEnterCritical +* vPortExitCritical +* vPortGenerateSimulatedInterrupt +* vAssertCalled +* xTaskGetSchedulerState +* pvTaskIncrementMutexHeldCount +* xTaskRemoveFromEventList +* xTaskPriorityDisinherit + +This proof checks ```FreeRTOS_OutputARPRequest``` in multiple configurations. +All assume the memory safety of vNetworkInterfaceAllocateRAMToBuffers. +* The ```config_minimal_configuration``` proof sets + ```ipconfigUSE_LINKED_RX_MESSAGES=0```. +* The ```config_minimal_configuration_linked_rx_messages``` proof sets + ```ipconfigUSE_LINKED_RX_MESSAGES=1```. +* The ```minimal_configuration_minimal_packet_size``` proof sets + ```ipconfigETHERNET_MINIMUM_PACKET_BYTES``` to 50. + +All harnesses include the queue.c file, but test only for the happy path. diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json new file mode 100644 index 000000000..fb5dd4be2 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json @@ -0,0 +1,48 @@ +{ + "ENTRY": "OutputARPRequest", + "MINIMUM_PACKET_BYTES": 50, + "CBMCFLAGS": + [ + "--unwind {MINIMUM_PACKET_BYTES}", + "--unwindset xNetworkBuffersInitialise.0:3,xNetworkBuffersInitialise.1:3,vListInsert.0:3,pxGetNetworkBufferWithDescriptor.0:3,pxGetNetworkBufferWithDescriptor.1:3,vNetworkInterfaceAllocateRAMToBuffers.0:3" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_2.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Source/queue.goto" + ], + "DEF": + [ + { + "minimal_configuration": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=0" + ] + }, + { + "minimal_configuration_minimal_packet_size": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}", + "ipconfigUSE_TCP=1" + ] + }, + { + "minimal_configuration_linked_rx_messages": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=1" + ] + } + ] +} diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c new file mode 100644 index 000000000..c047a2760 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c @@ -0,0 +1,54 @@ +/* This harness is linked against + * libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_2.goto + */ +#include <stdint.h> +#include <stdio.h> + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#if( ipconfigUSE_LLMNR == 1 ) + #include "FreeRTOS_DNS.h" +#endif /* ipconfigUSE_LLMNR */ +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" + +void *pvPortMalloc( size_t xWantedSize ){ + return malloc(xWantedSize); +} + + +void vPortFree( void *pv ){ + free(pv); +} + +/* + * This function function writes a buffer to the network. We stub it + * out here, and assume it has no side effects relevant to memory safety. + */ +BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){ + if( bReleaseAfterSend != pdFALSE ) + { + vReleaseNetworkBufferAndDescriptor( pxDescriptor ); + } +} + +void harness() +{ + BaseType_t xRes = xNetworkBuffersInitialise(); + if(xRes == pdPASS){ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); + } +} + diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md new file mode 100644 index 000000000..5d509a7e8 --- /dev/null +++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md @@ -0,0 +1,49 @@ +This is the memory safety proof for FreeRTOS_OutputARPRequest +method combined with the BufferAllocation_2.c allocation strategy. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* vPortEnterCritical +* vPortExitCritical +* vPortGenerateSimulatedInterrupt +* vAssertCalled +* xTaskGetSchedulerState +* pvTaskIncrementMutexHeldCount +* xTaskRemoveFromEventList +* xTaskPriorityDisinherit + +* pvPortMalloc +* pvPortFree +* xNetworkInterfaceOutput +* vNetworkInterfaceAllocateRAMToBuffers + +This proof disables the tracing library in the header. + +This proof checks FreeRTOS_OutputARPRequest in multiple configuration: + +* The proof in the directory config_minimal_configuration guarantees + that the implementation and interaction between + FreeRTOS_OutputARPRequest and + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + are memory save. This proof depends entirely of the implementation + correctness of vNetworkInterfaceAllocateRAMToBuffers. +* The proof in directory minimal_configuration_minimal_packet_size + guarantees that using + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + along with the ipconfigETHERNET_MINIMUM_PACKET_BYTES is memory save + as long as TCP is enabled ( ipconfigUSE_TCP 1 ) and + ipconfigETHERNET_MINIMUM_PACKET_BYTES < sizeof( TCPPacket_t ). +* The directory minimal_configuration_minimal_packet_size_no_tcp + reminds that ipconfigETHERNET_MINIMUM_PACKET_BYTES must not be used + if TCP is disabled ( ipconfigUSE_TCP 1 ) along with the + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + allocator. +* The proof in directory + config_minimal_configuration_linked_rx_messages guarantees that the + ipconfigUSE_LINKED_RX_MESSAGES define does not interfere with the + memory safety claim. + +All harnesses include the queue.c file, but test only for the happy path. |