From 612972650168df94096a8e6f4ba38f969418f0f9 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Thu, 13 Oct 2022 12:21:36 -0400
Subject: [PATCH] Resolved VF preprocessor error.

VF's preprocessor cannot handle context-sensitive macro expansion.
---
 include/task.h | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/include/task.h b/include/task.h
index 410f9283b..8bc75d1f3 100644
--- a/include/task.h
+++ b/include/task.h
@@ -42,6 +42,23 @@
 #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
     #error "include FreeRTOS.h must appear in source files before include task.h"
 #endif