1This is the memory safety proof for prvTCPPrepareSend. 2 3This proof is a work-in-progress. Proof assumptions are described in 4the harness. The proof also assumes the following functions are 5memory safe and have no side effects relevant to the memory safety of 6this function: 7 8* ulTCPWindowTxGet 9* xTCPWindowTxDone 10 11* xTaskGetTickCount 12 13* uxStreamBufferGet 14* vReleaseNetworkBufferAndDescriptor 15* vSocketWakeUpUser 16