From 734dafb987437db12fab0fe83a396b894ccf3a30 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 9 Sep 2018 11:14:38 +0100
Subject: [PATCH] Test for memcpy with struct pointers

---
 regression/cbmc/memcpy-struct-ptr/main.c    | 51 +++++++++++++++++++++
 regression/cbmc/memcpy-struct-ptr/test.desc | 12 +++++
 2 files changed, 63 insertions(+)
 create mode 100644 regression/cbmc/memcpy-struct-ptr/main.c
 create mode 100644 regression/cbmc/memcpy-struct-ptr/test.desc

diff --git a/regression/cbmc/memcpy-struct-ptr/main.c b/regression/cbmc/memcpy-struct-ptr/main.c
new file mode 100644
index 00000000000..e913dd4b4bb
--- /dev/null
+++ b/regression/cbmc/memcpy-struct-ptr/main.c
@@ -0,0 +1,51 @@
+#include <string.h>
+#include <assert.h>
+
+struct without_ptr
+{
+  int x;
+  int y;
+};
+struct with_int_ptr
+{
+  int *i;
+  int j;
+};
+struct with_struct_ptr
+{
+  struct without_ptr *s;
+  int t;
+};
+
+int main(int argc, char **argv)
+{
+  struct without_ptr w;
+  w.x = 42;
+  w.y = 43;
+
+  struct without_ptr v;
+  memcpy(&v, &w, sizeof(struct without_ptr));
+  assert(v.x == 42);
+  assert(v.y == 43);
+
+  struct with_int_ptr k;
+  k.i = (int *)44;
+  k.j = 45;
+
+  struct with_int_ptr m;
+  memcpy(&m, &k, sizeof(struct with_int_ptr));
+  assert(m.i == (int *)44);
+  assert(m.j == 45);
+  
+  struct with_struct_ptr p;
+  p.s = &w;
+  p.t = 46;
+
+  struct with_struct_ptr q;
+  memcpy(&q, &p, sizeof(struct with_struct_ptr));
+  assert(q.s->x == 42);
+  assert(q.s->y == 43);
+  assert(q.t == 46);
+  
+  return 0;
+}
diff --git a/regression/cbmc/memcpy-struct-ptr/test.desc b/regression/cbmc/memcpy-struct-ptr/test.desc
new file mode 100644
index 00000000000..37a7f2a9e72
--- /dev/null
+++ b/regression/cbmc/memcpy-struct-ptr/test.desc
@@ -0,0 +1,12 @@
+KNOWNBUG
+main.c
+--bounds-check --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^\[main\.assertion\.5\] assertion q\.s->x == 42: SUCCESS$
+^\[main\.assertion\.6\] assertion q\.s->y == 43: SUCCESS$
+--
+^warning: ignoring
+--
+Issue: 2925