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

Replaced asm macro by failing assertion.

Browse source
This commit is contained in:
Tobias Reinhard 2022-10-22 12:39:54 -04:00
parent 75fa197ac9
commit eeae596776
3 changed files with 255 additions and 225 deletions
Download patch file Download diff file Expand all files Collapse all files

4
tasks.c
View file

@ -44,6 +44,10 @@
#include "timers.h" #include "timers.h"
#include "stack_macros.h" #include "stack_macros.h"
#ifdef VERIFAST
#include "verifast_asm.h"
#endif
/* Lint e9021, e961 and e750 are suppressed as a MISRA exception justified /* Lint e9021, e961 and e750 are suppressed as a MISRA exception justified
* because the MPU ports require MPU_WRAPPERS_INCLUDED_FROM_API_FILE to be defined * because the MPU ports require MPU_WRAPPERS_INCLUDED_FROM_API_FILE to be defined
* for the header files above, but not in this file, in order to generate the * for the header files above, but not in this file, in order to generate the

464
verification/verifast/preprocessed_files/tasks--pp.c
View file

File diff suppressed because it is too large Load diff

12
verification/verifast/proof_setup/verifast_asm.h Normal file
View file

@ -0,0 +1,12 @@
#ifndef VERIFAST_ASM_H
#define VERIFAST_ASM_H
bool assert_fct(bool b)
{
assert(b);
return b;
}
#undef portCHECK_IF_IN_ISR
#define portCHECK_IF_IN_ISR() assert_fct(false)
#endif /* VERIFAST_ASM_H */