len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-22 20:57:45 -04:00
Code Issues Projects Releases Packages Wiki Activity
FreeRTOS-Kernel/FreeRTOS-Plus/Test/CBMC/proofs/TCP/prvTCPPrepareSend
History
markrtuttle cdf6d93cb9
Modify CBMC proofs to make assumptions about malloc explicit. (#312) 
Some proofs assume that some pointers returned by malloc are not
NULL. This patch modifies those proofs to make these assumptions
explicit with `__CPROVER_assume(pointer != NULL)` for all such
pointers.

Co-authored-by: Mark R. Tuttle <mrtuttle@amazon.com>
Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
2020-10-02 18:18:16 -04:00
..
Makefile.json Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
README.md Move CBMC proofs to FreeRTOS+ directory (#64) 2020-05-05 09:57:18 -07:00
TCPPrepareSend_harness.c Modify CBMC proofs to make assumptions about malloc explicit. (#312) 2020-10-02 18:18:16 -04:00

README.md

This is the memory safety proof for prvTCPPrepareSend.

This proof is a work-in-progress. Proof assumptions are described in the harness. The proof also assumes the following functions are memory safe and have no side effects relevant to the memory safety of this function:

  • ulTCPWindowTxGet

  • xTCPWindowTxDone

  • xTaskGetTickCount

  • uxStreamBufferGet

  • vReleaseNetworkBufferAndDescriptor

  • vSocketWakeUpUser