1 files changed, 67 insertions, 0 deletions
diff --git a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst
new file mode 100644
index 00000000..d0b4838f
--- /dev/null
+++ b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst
@@ -0,0 +1,67 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [rename_attribute]: function definitions *)
+module RenameAttribute.Funs
+open Primitives
+include RenameAttribute.Types
+include RenameAttribute.Clauses
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [rename_attribute::{(rename_attribute::BoolTrait for bool)}::get_bool]:
+    Source: 'tests/src/rename_attribute.rs', lines 22:4-22:30 *)
+let boolTraitBool_getTest (self : bool) : result bool =
+  Ok self
+
+(** Trait implementation: [rename_attribute::{(rename_attribute::BoolTrait for bool)}]
+    Source: 'tests/src/rename_attribute.rs', lines 21:0-21:23 *)
+let boolImpl : boolTest_t bool = { getTest = boolTraitBool_getTest; }
+
+(** [rename_attribute::BoolTrait::ret_true]:
+    Source: 'tests/src/rename_attribute.rs', lines 15:4-15:30 *)
+let boolTrait_retTest
+  (#self : Type0) (self_clause : boolTest_t self) (self1 : self) :
+  result bool
+  =
+  Ok true
+
+(** [rename_attribute::test_bool_trait]:
+    Source: 'tests/src/rename_attribute.rs', lines 28:0-28:42 *)
+let boolFn (t : Type0) (x : bool) : result bool =
+  let* b = boolTraitBool_getTest x in
+  if b then boolTrait_retTest boolImpl x else Ok false
+
+(** [rename_attribute::C]
+    Source: 'tests/src/rename_attribute.rs', lines 50:0-50:12 *)
+let const_test_body : result u32 = let* i = u32_add 100 10 in u32_add i 1
+let const_test : u32 = eval_global const_test_body
+
+(** [rename_attribute::CA]
+    Source: 'tests/src/rename_attribute.rs', lines 53:0-53:13 *)
+let const_aeneas11_body : result u32 = u32_add 10 1
+let const_aeneas11 : u32 = eval_global const_aeneas11_body
+
+(** [rename_attribute::factorial]:
+    Source: 'tests/src/rename_attribute.rs', lines 56:0-56:27 *)
+let rec factfn (n : u64) : Tot (result u64) (decreases (factfn_decreases n)) =
+  if n <= 1
+  then Ok 1
+  else let* i = u64_sub n 1 in let* i1 = factfn i in u64_mul n i1
+
+(** [rename_attribute::sum]: loop 0:
+    Source: 'tests/src/rename_attribute.rs', lines 67:4-75:1 *)
+let rec no_borrows_sum_loop
+  (max : u32) (i : u32) (s : u32) :
+  Tot (result u32) (decreases (no_borrows_sum_loop_decreases max i s))
+  =
+  if i < max
+  then
+    let* s1 = u32_add s i in
+    let* i1 = u32_add i 1 in
+    no_borrows_sum_loop max i1 s1
+  else u32_mul s 2
+
+(** [rename_attribute::sum]:
+    Source: 'tests/src/rename_attribute.rs', lines 65:0-65:27 *)
+let no_borrows_sum (max : u32) : result u32 =
+  no_borrows_sum_loop max 0 0
+