bug related to pointers to members

Author: Daniel Kroening

regression/cbmc/struct9/main.c

@@ -0,0 +1,23 @@
+struct inner_struct {
+  char *GUARDp;
+};
+
+struct outer_struct {
+  char GUARD;
+  struct inner_struct inner;
+};
+
+void foo(struct inner_struct *inner) 
+{
+  assert(*(inner->GUARDp) != 1);
+}
+
+int main()
+{
+  struct outer_struct outer;  
+
+  outer.GUARD = 2;
+  outer.inner.GUARDp = &outer.GUARD;
+  
+  foo(&outer.inner);
+}

regression/cbmc/struct9/test.desc

@@ -0,0 +1,8 @@
+KNOWBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring