len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-12 06:35:19 -05:00
Code Issues Projects Releases Packages Wiki Activity

Added contract for portDISABLE_INTERRUPTS and dummy contracts for lock acquiring macros.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-04 14:20:58 -04:00
parent 5c9750eac4
commit ac798f9fb5
1 changed files with 27 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

27
verification/verifast/proof/verifast_port_contracts.h Normal file
View file

@ -0,0 +1,27 @@
#ifndef VERIFAST_PORT_CONTRACTS_H
#define VERIFAST_PORT_CONTRACTS_H
/*@
predicate interruptsOn_p(bool status);
@*/
#undef portDISABLE_INTERRUPTS
#define portDISABLE_INTERRUPTS VF__portDISABLE_INTERRUPTS
void VF__portDISABLE_INTERRUPTS();
//@ requires interruptsOn_p(_);
//@ ensures interruptsOn_p(false);
#undef portGET_TASK_LOCK
#define portGET_TASK_LOCK VF__portGET_TASK_LOCK
void VF__portGET_TaskLock();
//@ requires false;
//@ ensures true;
#undef portGET_ISR_LOCK
#define portGET_ISR_LOCK VF__portGET_ISR_LOCK
void VF__portGET_ISR_LOCK();
//@ requires false;
//@ ensures true;
#endif /* VERIFAST_PORT_CONTRACTS_H */