RTOS/SDK_STM32F302x
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
Files
af0d1219b67bfe89853c8ca7d1faab3a46fdf881
SDK_STM32F302x/kernel/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/README.md
gaoyang3513 a345df017b [修改] 增加freeRTOS 
1. 版本FreeRTOSv202212.01，命名为kernel；
2023-05-06 16:43:01 +00:00

502 B
Raw Blame History

Given that the passed mutex storage area is not null, the QueueCreateMutexStatic function is memory safe.

Otherwise an assertion violation is triggered.

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
  • vPortGenerateSimulatedInterrupt
  • xTaskGetSchedulerState
  • xTaskPriorityDisinherit