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

For bug description, see minimal example `define_name`.
---
 include/timers.h | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/include/timers.h b/include/timers.h
index 2ef995114..344cbf395 100644
--- a/include/timers.h
+++ b/include/timers.h
@@ -28,6 +28,20 @@
 #ifndef TIMERS_H
 #define TIMERS_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 "include FreeRTOS.h must appear in source files before include timers.h"
 #endif