From aa8e74197687ecc6d8f925babc8ba3cd6c739990 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 18 Jun 2024 22:47:35 +0200
Subject: Support for renaming using the rename attribute in charon (#239)

* support for renaming using the rename attribute in charon

* support for global decl

* add support for renaming field

* applied suggested changes and began adding support for variant

* finished support for renaming variant

* applied suggested changes

* add tests

* fixed variant and field renaming

* update charon-pin

* update flake.lock

* Update the charon pin

* Fix an issue with renaming trait method implementations

* Fix an issue with the renaming of trait implementations

* Fix an issue when renaming enumerations

* Update the Charon pin

* Fix the F* tests

* Fix an issue with the spans for the loops

* Fix the tests

* Update a comment

* Use fuel in the coq tests

* Generate the template decreases clauses by default

---------

Co-authored-by: Escherichia <escherichia@charlotte>
Co-authored-by: Son Ho <hosonmarc@gmail.com>---
 tests/src/rename_attribute.rs | 75 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)
 create mode 100644 tests/src/rename_attribute.rs

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

diff --git a/tests/src/rename_attribute.rs b/tests/src/rename_attribute.rs
new file mode 100644
index 00000000..78765817
--- /dev/null
+++ b/tests/src/rename_attribute.rs
@@ -0,0 +1,75 @@
+//@ [fstar] aeneas-args=-decreases-clauses -split-files
+//@ [coq] aeneas-args=-use-fuel
+#![feature(register_tool)]
+#![register_tool(charon)]
+#![register_tool(aeneas)]
+
+#[charon::rename("BoolTest")]
+pub trait BoolTrait {
+    // Required method
+    #[charon::rename("getTest")]
+    fn get_bool(&self) -> bool;
+
+    // Provided method
+    #[charon::rename("retTest")]
+    fn ret_true(&self) -> bool {
+        true
+    }
+}
+
+#[charon::rename("BoolImpl")]
+impl BoolTrait for bool {
+    fn get_bool(&self) -> bool {
+        *self
+    }
+}
+
+#[charon::rename("BoolFn")]
+pub fn test_bool_trait<T>(x: bool) -> bool {
+    x.get_bool() && x.ret_true()
+}
+
+#[charon::rename("TypeTest")]
+type Test = i32;
+
+#[charon::rename("VariantsTest")]
+enum SimpleEnum {
+    #[charon::rename("Variant1")]
+    FirstVariant,
+    SecondVariant,
+    ThirdVariant,
+}
+
+#[charon::rename("StructTest")]
+struct Foo {
+    #[charon::rename("FieldTest")]
+    field1: u32,
+}
+
+#[charon::rename("Const_Test")]
+const C: u32 = 100 + 10 + 1;
+
+#[aeneas::rename("Const_Aeneas11")]
+const CA: u32 = 10 + 1;
+
+#[charon::rename("Factfn")]
+fn factorial(n: u64) -> u64 {
+    if n <= 1 {
+        1
+    } else {
+        return n * factorial(n - 1);
+    }
+}
+
+#[charon::rename("No_borrows_sum")]
+pub fn sum(max: u32) -> u32 {
+    let mut i = 0;
+    let mut s = 0;
+    while i < max {
+        s += i;
+        i += 1;
+    }
+
+    s *= 2;
+    s
+}
-- 
cgit v1.2.3