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


From 4d3778bea3112168645efc03308056ec341abb5f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 15:47:20 +0200
Subject: runner: Pass options in special comments

---
 tests/src/polonius_list.rs | 2 ++
 1 file changed, 2 insertions(+)

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

diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
index 8c64110d..a8d51e40 100644
--- a/tests/src/polonius_list.rs
+++ b/tests/src/polonius_list.rs
@@ -1,3 +1,5 @@
+//@ charon-args=--polonius
+//@ aeneas-args=-test-trans-units
 #![allow(dead_code)]
 
 pub enum List<T> {
-- 
cgit v1.2.3