From f7316a77f0370b250daf0636e59646389602d77a Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Thu, 13 Oct 2022 10:01:34 -0400
Subject: [PATCH] Added temporary work-around for VF's `define_name` bug.

For bug description, see minimal example `define_name`.
---
 include/list.h | 14 ++++++++++++++
 include/task.h | 14 ++++++++++++++
 2 files changed, 28 insertions(+)

diff --git a/include/list.h b/include/list.h
index 332f3f413..2e4d45823 100644
--- a/include/list.h
+++ b/include/list.h
@@ -56,6 +56,20 @@
 #ifndef 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
     #error "FreeRTOS.h must be included before list.h"
 #endif
diff --git a/include/task.h b/include/task.h
index 65cd86e8d..410f9283b 100644
--- a/include/task.h
+++ b/include/task.h
@@ -28,6 +28,20 @@
 #ifndef 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
     #error "include FreeRTOS.h must appear in source files before include task.h"
 #endif