| Name | Date | Size | #Lines | LOC | ||
|---|---|---|---|---|---|---|
| .. | - | - | ||||
| Makefile.json | D | 18-Mar-2025 | 1.6 KiB | 52 | 23 | |
| README.md | D | 18-Mar-2025 | 414 | 16 | 11 | |
| TCPPrepareSend_harness.c | D | 18-Mar-2025 | 3.8 KiB | 102 | 49 |
README.md
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