From c71025fda02249a85aab771803de45d10917cdc1 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Thu, 13 Oct 2022 09:16:54 -0400
Subject: [PATCH] Added minimal example for VF bug involving testing for macro
 defines in headers.

---
 verification/verifast/problems/README.md      |  2 ++
 .../bugs/define_name/defining_header.h        | 10 ++++++++++
 .../verifast/problems/bugs/define_name/main.c | 20 +++++++++++++++++++
 .../bugs/define_name/testing_header.h         | 17 ++++++++++++++++
 4 files changed, 49 insertions(+)
 create mode 100644 verification/verifast/problems/README.md
 create mode 100644 verification/verifast/problems/bugs/define_name/defining_header.h
 create mode 100644 verification/verifast/problems/bugs/define_name/main.c
 create mode 100644 verification/verifast/problems/bugs/define_name/testing_header.h

diff --git a/verification/verifast/problems/README.md b/verification/verifast/problems/README.md
new file mode 100644
index 000000000..712ec2815
--- /dev/null
+++ b/verification/verifast/problems/README.md
@@ -0,0 +1,2 @@
+This directory contains collection of problems encountered with VeriFast that
+need to be fixed in order to verify the current code base as is.
diff --git a/verification/verifast/problems/bugs/define_name/defining_header.h b/verification/verifast/problems/bugs/define_name/defining_header.h
new file mode 100644
index 000000000..e63adcfa0
--- /dev/null
+++ b/verification/verifast/problems/bugs/define_name/defining_header.h
@@ -0,0 +1,10 @@
+#define ABC
+
+
+/*
+#ifdef ABC				// ok: evaluates to true
+    #error "ABC defined"		
+#else					// ok: evaluates to false
+    #error "ABC not defined"
+#endif
+*/
diff --git a/verification/verifast/problems/bugs/define_name/main.c b/verification/verifast/problems/bugs/define_name/main.c
new file mode 100644
index 000000000..c71f3ef2f
--- /dev/null
+++ b/verification/verifast/problems/bugs/define_name/main.c
@@ -0,0 +1,20 @@
+/* Bug:
+ * The header `defining_header.h` defines the constant `ABC` and
+ * the header `testing_header.h` checks whether `ABC` has been defined.
+ * In `testing_header.h` both checks `#ifdef ABC` and its negation
+ * `#ifndef ABC` evaluate to true.
+ */
+
+#include "defining_header.h"
+
+
+/*
+#ifdef ABC			// ok: evaluates to true
+    #error "ABC defined"		
+#else				// ok: evaluates to false
+    #error "ABC not defined"
+#endif
+*/
+
+
+#include "testing_header.h"
\ No newline at end of file
diff --git a/verification/verifast/problems/bugs/define_name/testing_header.h b/verification/verifast/problems/bugs/define_name/testing_header.h
new file mode 100644
index 000000000..9add91a69
--- /dev/null
+++ b/verification/verifast/problems/bugs/define_name/testing_header.h
@@ -0,0 +1,17 @@
+// Problem: Both branches branch conditions evaluate to true.
+
+/* `main.c` included this header after including `defining_header.h`.
+ * Hence, `#ifdef ABC` should evaluate to true and `#ifndef ABC should
+ * evaluate to false.
+ */
+
+/*
+#ifdef ABC			// ok: evaluates to true.
+    #error "ABC defined"	
+#endif
+*/
+
+
+#ifndef ABC			// bug: evaluates to true
+    #error "ABC defined"
+#endif
\ No newline at end of file