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>

1 files changed, 18 insertions, 0 deletions

diff --git a/tests/fstar/rename_attribute/RenameAttribute.Clauses.Template.fst b/tests/fstar/rename_attribute/RenameAttribute.Clauses.Template.fst
new file mode 100644
index 00000000..d2229a71
--- /dev/null
+++ b/tests/fstar/rename_attribute/RenameAttribute.Clauses.Template.fst
@@ -0,0 +1,18 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [rename_attribute]: templates for the decreases clauses *)
+module RenameAttribute.Clauses.Template
+open Primitives
+open RenameAttribute.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [rename_attribute::factorial]: decreases clause
+    Source: 'tests/src/rename_attribute.rs', lines 56:0-56:27 *)
+unfold let factfn_decreases (n : u64) : nat = admit ()
+
+(** [rename_attribute::sum]: decreases clause
+    Source: 'tests/src/rename_attribute.rs', lines 67:4-75:1 *)
+unfold
+let no_borrows_sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat =
+  admit ()
+