From 50c5b21a59a88e91822c057bf8397ce5ef210bb7 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Thu, 13 Oct 2022 11:34:24 -0400 Subject: [PATCH] Resolved VF preprocessor error. VF's preprocessor cannot handle expansion of `PRIVILEGED_FUNCTION` macro because the normal and the context-free preprocessor consume different numbers of tokens. We resolved this temporarily by deleting the macro. --- include/list.h | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/include/list.h b/include/list.h index 2e4d45823..2b6283aa8 100644 --- a/include/list.h +++ b/include/list.h @@ -74,6 +74,17 @@ #error "FreeRTOS.h must be included before list.h" #endif +#ifdef VERIFAST + /* Reason for rewrite: + * VeriFast's normal and context-free preprocessor consume different + * numbers of tokens when expanding `PRIVILEGED_FUNCTION` in this file. + */ + #define PRIVILEGED_FUNCTION + // TODO: Figure out why the preprocessors consume different amounts of + // of tokens. This most likely has to do with the path/context + // from which this header is included. +#endif /* VERIFAST */ + /* * The list structure members are modified from within interrupts, and therefore * by rights should be declared volatile. However, they are only modified in a