len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-15 08:05:15 -05:00
Code Issues Projects Releases Packages Wiki Activity
FreeRTOS-Kernel/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR
History
Mark Tuttle 0390b0fc9b
Add CBMC viewer configuration files (#683) 
* Revert cbmc-viewer flags

* Add cbmc-viewer configuration files

* Repair CBMC patch to prvCopyDataToQueue

Authored-by: Mark R. Tuttle <mrtuttle@amazon.com>
2021-09-13 21:23:35 -04:00
..
cbmc-viewer.json Add CBMC viewer configuration files (#683) 2021-09-13 21:23:35 -04:00
Configurations.json
QueueGenericSendFromISR_harness.c
README.md

README.md

The harness in this folder proves the memory safety of QueueGenericSendFromISR with and without QueueSets. It is abstracting away the task pool and concurrency related functions. Further, it uses a stub for prvCopyDataToQueue.

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:

  • vPortEnterCritical
  • vPortExitCritical
  • xTaskRemoveFromEventList