summaryrefslogtreecommitdiff
path: root/tests/fstar/misc
diff options
context:
space:
mode:
authorSon Ho2023-11-08 14:28:44 +0100
committerSon Ho2023-11-08 14:28:44 +0100
commit530a5ae56209061f091bbcafee82de07039a8124 (patch)
tree6a82c5b7d34d734d83da1892f4fbb9a36cffec12 /tests/fstar/misc
parenta745e81c9949f24878f788fffd36667739c59330 (diff)
Update the Makefile and regenerate some tests
Diffstat (limited to '')
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst12
1 files changed, 12 insertions, 0 deletions
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 33142250..e97927aa 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -54,6 +54,18 @@ let div_test1 (x : u32) : result u32 =
let rem_test (x : u32) (y : u32) : result u32 =
u32_rem x y
+(** [no_nested_borrows::mul_test]: forward function *)
+let mul_test (x : u32) (y : u32) : result u32 =
+ u32_mul x y
+
+(** [no_nested_borrows::CONST0] *)
+let const0_body : result usize = usize_add 1 1
+let const0_c : usize = eval_global const0_body
+
+(** [no_nested_borrows::CONST1] *)
+let const1_body : result usize = usize_mul 2 2
+let const1_c : usize = eval_global const1_body
+
(** [no_nested_borrows::cast_test]: forward function *)
let cast_test (x : u32) : result i32 =
scalar_cast U32 I32 x