From c304913b640c0ad603348a2fb0b52595d2a42944 Mon Sep 17 00:00:00 2001 From: Monika Singh Date: Fri, 23 Aug 2024 12:18:51 +0530 Subject: [PATCH] Remove redundant TCP includes in FreeRTOS CBMC proofs (#1254) * Remove unnecessary TCP includes * Update comment --- ...reertos_ip_verification_access_ip_define.h | 31 ------------- ...ertos_tcp_verification_access_tcp_define.h | 46 ------------------- FreeRTOS/Test/CBMC/include/cbmc.h | 10 ---- 3 files changed, 87 deletions(-) delete mode 100644 FreeRTOS/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h delete mode 100644 FreeRTOS/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h diff --git a/FreeRTOS/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h b/FreeRTOS/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h deleted file mode 100644 index 8845621573..0000000000 --- a/FreeRTOS/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h +++ /dev/null @@ -1,31 +0,0 @@ -/* - * FreeRTOS V202212.00 - * Copyright (C) 2020 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. - * - * https://www.FreeRTOS.org - * https://github.com/FreeRTOS - * - */ - -eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket, - NetworkBufferDescriptor_t * const pxNetworkBuffer ) -{ - prvProcessIPPacket( pxIPPacket, pxNetworkBuffer ); -} diff --git a/FreeRTOS/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h b/FreeRTOS/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h deleted file mode 100644 index e0f9c7805e..0000000000 --- a/FreeRTOS/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h +++ /dev/null @@ -1,46 +0,0 @@ -/* - * FreeRTOS V202212.00 - * Copyright (C) 2020 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. - * - * https://www.FreeRTOS.org - * https://github.com/FreeRTOS - * - */ - -int32_t publicTCPPrepareSend( FreeRTOS_Socket_t * pxSocket, - NetworkBufferDescriptor_t ** ppxNetworkBuffer, - UBaseType_t uxOptionsLength ) -{ - prvTCPPrepareSend( pxSocket, ppxNetworkBuffer, uxOptionsLength ); -} - -BaseType_t publicTCPHandleState( FreeRTOS_Socket_t * pxSocket, - NetworkBufferDescriptor_t ** ppxNetworkBuffer ) -{ - prvTCPHandleState( pxSocket, ppxNetworkBuffer ); -} - -void publicTCPReturnPacket( FreeRTOS_Socket_t * pxSocket, - NetworkBufferDescriptor_t * pxNetworkBuffer, - uint32_t ulLen, - BaseType_t xReleaseAfterSend ) -{ - prvTCPReturnPacket( pxSocket, pxNetworkBuffer, ulLen, xReleaseAfterSend ); -} diff --git a/FreeRTOS/Test/CBMC/include/cbmc.h b/FreeRTOS/Test/CBMC/include/cbmc.h index 1d898296af..324e8ea520 100644 --- a/FreeRTOS/Test/CBMC/include/cbmc.h +++ b/FreeRTOS/Test/CBMC/include/cbmc.h @@ -33,16 +33,6 @@ #include "task.h" #include "semphr.h" -/* FreeRTOS+TCP includes. */ -#include "FreeRTOS_IP.h" -#include "FreeRTOS_Sockets.h" -#include "FreeRTOS_IP_Private.h" -#include "FreeRTOS_UDP_IP.h" -#include "FreeRTOS_DNS.h" -#include "FreeRTOS_DHCP.h" -#include "NetworkBufferManagement.h" -#include "NetworkInterface.h" - /* * CBMC models a pointer as an object id and an offset into that * object. The top bits of a pointer encode the object id and the