From 9270fcfe38b4fcd617f36c62ac8b76ee3ddae64d Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@cl.cam.ac.uk>
Date: Wed, 16 Aug 2023 10:55:40 +0100
Subject: [PATCH] CN: add a test for the self-ref init case

Cerberus treats this as UB, whereas some Linux code seems to assume
it works. Add an "unknown" category to the CN tests for code where
it's not clear if it should be rejected or not.
---
 tests/cn/self_ref_init.unknown.c | 19 +++++++++++++++++++
 tests/run-cn.sh                  |  2 +-
 2 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 tests/cn/self_ref_init.unknown.c

diff --git a/tests/cn/self_ref_init.unknown.c b/tests/cn/self_ref_init.unknown.c
new file mode 100644
index 000000000..d58091adb
--- /dev/null
+++ b/tests/cn/self_ref_init.unknown.c
@@ -0,0 +1,19 @@
+
+/* based on a problematic example from linux kvm/pgtable.c */
+
+struct str {
+  int x;
+  int y;
+};
+
+int f (int x)
+/*@ requires (0 <= x) && (x < 200) @*/
+{
+  struct str str_inst = {
+    .x = x + 2,
+    .y = str_inst.x + 3,
+  };
+
+  return str_inst.y;
+}
+
diff --git a/tests/run-cn.sh b/tests/run-cn.sh
index 787d58255..d94c88ce6 100755
--- a/tests/run-cn.sh
+++ b/tests/run-cn.sh
@@ -6,7 +6,7 @@ DIRNAME=$(dirname $0)
 
 set -e
 
-SUCC=$(find $DIRNAME/cn -name '*.c' | grep -v '\.error\.c')
+SUCC=$(find $DIRNAME/cn -name '*.c' | grep -v '\.error\.c' | grep -v '\.unknown\.c')
 
 for TEST in $SUCC
 do