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

@@ -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;
+}
+