1 files changed, 12 insertions, 0 deletions
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
new file mode 100644
index 000000000..01075d2ba
--- /dev/null
+++ b/FreeRTOS/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h
@@ -0,0 +1,12 @@
+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 );
+}