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 temporary work-around for VF's define_name bug.

Browse source 
For bug description, see minimal example `define_name`.
This commit is contained in:
Tobias Reinhard 2022-10-13 12:40:50 -04:00
parent 8aa7af3fd5
commit 997d39d894
1 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
include/timers.h
View file

@ -28,6 +28,20 @@
#ifndef TIMERS_H #ifndef TIMERS_H
#define TIMERS_H #define TIMERS_H
#ifdef VERIFAST
/* Reason for rewrite:
* VeriFast bug:
* Both `#ifdef INC_FREERTOS_H` and its negation `#ifdef INC_FREERTOS_H`
* evaluate to true. See minimal example `define_name`.
*/
#define INC_FREERTOS_H
/* Remember that this header is included indirectly `tasks.c` after it
* includes `FreeRTOS.h`.
*/
// TODO: Remove this work-around once VF has been fixed.
#endif /* VERIFAST */
#ifndef INC_FREERTOS_H #ifndef INC_FREERTOS_H
#error "include FreeRTOS.h must appear in source files before include timers.h" #error "include FreeRTOS.h must appear in source files before include timers.h"
#endif #endif