Merge branch 'main' into afromher/recursive_projectors

1 files changed, 14 insertions, 0 deletions

diff --git a/tests/src/external.rs b/tests/src/external.rs
new file mode 100644
index 00000000..ddd5539f
--- /dev/null
+++ b/tests/src/external.rs
@@ -0,0 +1,14 @@
+//@ 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;
+
+pub fn use_get(rc: &Cell<u32>) -> u32 {
+    rc.get()
+}
+
+pub fn incr(rc: &mut Cell<u32>) {
+    *rc.get_mut() += 1;
+}