Resolved VF preprocessor error.

VF's preprocessor cannot handle context-sensitive macro expansion.
This commit is contained in:
Tobias Reinhard 2022-10-13 12:21:36 -04:00
parent 50c5b21a59
commit 6129726501

View file

@ -42,6 +42,23 @@
#endif /* VERIFAST */ #endif /* VERIFAST */
/* Remark:
* Note that the following VF section renders the previous one obsolete.
* However, we keep the above as a reminder until the corresponding bug
* has been fixed.
*/
#ifdef VERIFAST
/* Reason for rewrite:
* Even though in the current verification setup, `FreeRTOS.h` is always
* included before this file is processed, VeriFast does not consider this
* context when processing this file. VeriFast forbids macro expansions to
* depend on a potentially variable context, e.g, `configSTACK_DEPTH_TYPE`
* which expands to 'uint16_t' if and only if `FreeRTOS.h` has been
* included.
*/
#include "FreeRTOS.h"
#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