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/external.rs | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 tests/src/external.rs

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

diff --git a/tests/src/external.rs b/tests/src/external.rs
new file mode 100644
index 00000000..521749d6
--- /dev/null
+++ b/tests/src/external.rs
@@ -0,0 +1,11 @@
+//! This module uses external types and functions
+
+use std::cell::Cell;
+
+pub fn use_get(rc: &Cell<u32>) -> u32 {
+    rc.get()
+}
+
+pub fn incr(rc: &mut Cell<u32>) {
+    *rc.get_mut() += 1;
+}
-- 
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/external.rs | 3 +++
 1 file changed, 3 insertions(+)

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

diff --git a/tests/src/external.rs b/tests/src/external.rs
index 521749d6..ddd5539f 100644
--- a/tests/src/external.rs
+++ b/tests/src/external.rs
@@ -1,3 +1,6 @@
+//@ charon-args=--no-code-duplication
+//@ aeneas-args=-state -split-files
+//@ aeneas-args=-test-trans-units
 //! This module uses external types and functions
 
 use std::cell::Cell;
-- 
cgit v1.2.3