len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-12 14:45:09 -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 10:01:34 -04:00
parent 4431a1f5d6
commit f7316a77f0
2 changed files with 28 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
include/list.h
View file

@ -56,6 +56,20 @@
#ifndef LIST_H #ifndef LIST_H
#define LIST_H #define LIST_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 "FreeRTOS.h must be included before list.h" #error "FreeRTOS.h must be included before list.h"
#endif #endif

14
include/task.h
View file

@ -28,6 +28,20 @@
#ifndef INC_TASK_H #ifndef INC_TASK_H
#define INC_TASK_H #define INC_TASK_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 by `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 task.h" #error "include FreeRTOS.h must appear in source files before include task.h"
#endif #endif