blob: d0b4838f012d6524d1533803dc1a097cee6fbd0f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
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
|
