From b1f9e61e69b840d8c67d81d79ef9a6dc5d64247c Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@cl.cam.ac.uk>
Date: Wed, 16 Aug 2023 16:41:52 +0100
Subject: [PATCH] CN: fix the failing memcpy test

It turns out the issue was trivial and obvious.
---
 tests/cn/get_from_arr.c | 20 ++++++++++++++++++++
 tests/cn/memcpy.c       |  1 +
 2 files changed, 21 insertions(+)
 create mode 100644 tests/cn/get_from_arr.c

diff --git a/tests/cn/get_from_arr.c b/tests/cn/get_from_arr.c
new file mode 100644
index 000000000..76b0bb5d0
--- /dev/null
+++ b/tests/cn/get_from_arr.c
@@ -0,0 +1,20 @@
+
+/* originally made by minimising a problematic case from memcpy.c */
+
+
+char
+get_from_arr (char *in_arr)
+/*@ requires take IA = each (integer j; 0 <= j && j < 10)
+  {Owned<char>(in_arr + (j * sizeof<char>))} @*/
+/*@ ensures take IA2 = each (integer j; 0 <= j && j < 10)
+  {Owned<char>(in_arr + (j * sizeof<char>))} @*/
+{
+  char c;
+
+  /*@ extract Owned<char>, 4; @*/
+  /*@ instantiate good<char>, 4; @*/
+  c = in_arr[4];
+
+  return c;
+}
+
diff --git a/tests/cn/memcpy.c b/tests/cn/memcpy.c
index b32a16b0d..eb862cf91 100644
--- a/tests/cn/memcpy.c
+++ b/tests/cn/memcpy.c
@@ -24,6 +24,7 @@ naive_memcpy (char *in_arr, char *out_arr, int i)
   /*@ inv {out_arr} unchanged @*/
   {
     /*@ extract Owned<char>, j; @*/
+    /*@ instantiate good<char>, j; @*/
     out_arr[j] = in_arr[j];
   }