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

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

diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
new file mode 100644
index 00000000..9f48cb04
--- /dev/null
+++ b/tests/src/bitwise.rs
@@ -0,0 +1,27 @@
+//! Exercise the bitwise operations
+
+pub fn shift_u32(a: u32) -> u32 {
+    let i: usize = 16;
+    let mut t = a >> i;
+    t <<= i;
+    t
+}
+
+pub fn shift_i32(a: i32) -> i32 {
+    let i: isize = 16;
+    let mut t = a >> i;
+    t <<= i;
+    t
+}
+
+pub fn xor_u32(a: u32, b: u32) -> u32 {
+    a ^ b
+}
+
+pub fn or_u32(a: u32, b: u32) -> u32 {
+    a | b
+}
+
+pub fn and_u32(a: u32, b: u32) -> u32 {
+    a & b
+}
-- 
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/bitwise.rs | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
index 9f48cb04..15962047 100644
--- a/tests/src/bitwise.rs
+++ b/tests/src/bitwise.rs
@@ -1,3 +1,4 @@
+//@ aeneas-args=-test-trans-units
 //! Exercise the bitwise operations
 
 pub fn shift_u32(a: u32) -> u32 {
-- 
cgit v1.2.3