1This is the memory safety proof for prvTCPHandleState.
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* prvTCPPrepareSend (proved independently)
9* prvTCPReturnPacket (proved independently)
10
11* lTCPAddRxdata
12* lTCPWindowRxCheck
13* lTCPWindowTxAdd
14* ulTCPWindowTxAck
15* vTCPWindowInit
16* xTCPWindowRxEmpty
17* xTCPWindowTxDone
18
19* uxStreamBufferGet
20* vReleaseNetworkBufferAndDescriptor
21* vSocketWakeUpUser
22* xTaskGetTickCount
23