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