From 4ce3e9c7c11744abae52d7a3ae1a3962395784be Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 10:41:10 +0200
Subject: Import test suite from charon

---
 tests/src/polonius_list.rs | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 tests/src/polonius_list.rs

(limited to 'tests/src/polonius_list.rs')

diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
new file mode 100644
index 00000000..8c64110d
--- /dev/null
+++ b/tests/src/polonius_list.rs
@@ -0,0 +1,27 @@
+#![allow(dead_code)]
+
+pub enum List<T> {
+    Cons(T, Box<List<T>>),
+    Nil,
+}
+
+/// An example which comes from the b-epsilon tree.
+///
+/// Returns a mutable borrow to the first portion of the list where we
+/// can find [x]. This allows to do in-place modifications (insertion, filtering)
+/// in a natural manner (this piece of code was inspired by the C++ BeTree).
+pub fn get_list_at_x<'a>(ls: &'a mut List<u32>, x: u32) -> &'a mut List<u32> {
+    match ls {
+        List::Nil => {
+            // We reached the end: just return it
+            ls
+        }
+        List::Cons(hd, tl) => {
+            if *hd == x {
+                ls // Doing this requires NLL
+            } else {
+                get_list_at_x(tl, x)
+            }
+        }
+    }
+}
-- 
cgit v1.2.3