Added minimal example for VF bug involving testing for macro defines in headers.

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.

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
+*/

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"

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