From f69a12c4c41327b2f714dc0eb72218c06f744779 Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@cl.cam.ac.uk>
Date: Wed, 6 Sep 2023 12:02:39 +0100
Subject: [PATCH 1/2] CN: add a test for required buddy-alloc behaviour

Make sure the test set contains a (fairly) minimal example which
fails for the same reason the buddy-allocator proof is currently
failing, to do with requiring alloc-ids to be the same between
argument pointers.
---
 tests/cn/get_from_array.c | 42 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 tests/cn/get_from_array.c

diff --git a/tests/cn/get_from_array.c b/tests/cn/get_from_array.c
new file mode 100644
index 000000000..fc9ad7859
--- /dev/null
+++ b/tests/cn/get_from_array.c
@@ -0,0 +1,42 @@
+
+
+/* Simple demo of a kind of situation where ownership is obtained via an array
+   that encloses an object passed by pointer. This kind of step is required by
+   the buddy-allocator proof. */
+
+int *global_array;
+
+enum {
+  global_array_width = 42,
+};
+
+/*@ function (integer) global_array_width () @*/
+
+static inline int get_global_array_width_for_cn (void)
+/*@ cn_function global_array_width @*/
+{
+  return global_array_width;
+}
+
+/*@
+predicate (map<integer, integer>) Global_Array (pointer p)
+{
+  take Arr = each (integer i; 0 <= i && i < global_array_width ())
+    { Owned<int>(p + (i * sizeof<int>)) };
+  return Arr;
+}
+@*/
+
+void set_a_pointer(int *p, int x)
+/*@ accesses global_array @*/
+/*@ requires take Arr = Global_Array(global_array) @*/
+/*@ requires let offs = ((integer)p - (integer)global_array) @*/
+/*@ requires mod(offs, sizeof<int>) == 0 @*/
+/*@ requires let idx = (offs / sizeof<int>) @*/
+/*@ requires 0 <= idx && idx < global_array_width () @*/
+/*@ ensures take Arr2 = Global_Array(global_array) @*/
+{
+  /*@ extract Owned<int>, idx; @*/
+  *p = x;
+}
+

From daaffc42a92d7e1853ceb8819ae45a69c0e4fdf5 Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@cl.cam.ac.uk>
Date: Wed, 6 Sep 2023 12:22:38 +0100
Subject: [PATCH 2/2] CN: simpler test of pointer eqs

This simpler test shows how alloc-ids change the behaviour of CN.
The assertion that pointer->integer->pointer conversion leaves a
pointer unchanged is now false, and was previously provable. A
more interesting question is, should this assertion be provable?
---
 tests/cn/test_pointer_eq.c | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 tests/cn/test_pointer_eq.c

diff --git a/tests/cn/test_pointer_eq.c b/tests/cn/test_pointer_eq.c
new file mode 100644
index 000000000..cfecfa772
--- /dev/null
+++ b/tests/cn/test_pointer_eq.c
@@ -0,0 +1,6 @@
+
+
+void f (int *p)
+{
+  /*@ assert (p == ((pointer) ((integer) p))); @*/
+}