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] 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))); @*/
+}