summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/misc/NoNestedBorrows.v12
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst12
-rw-r--r--tests/lean/NoNestedBorrows.lean12
3 files changed, 36 insertions, 0 deletions
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 47cdc3af..e916ca4a 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -71,6 +71,18 @@ Definition div_test1 (x : u32) : result u32 :=
Definition rem_test (x : u32) (y : u32) : result u32 :=
u32_rem x y.
+(** [no_nested_borrows::mul_test]: forward function *)
+Definition mul_test (x : u32) (y : u32) : result u32 :=
+ u32_mul x y.
+
+(** [no_nested_borrows::CONST0] *)
+Definition const0_body : result usize := usize_add 1%usize 1%usize.
+Definition const0_c : usize := const0_body%global.
+
+(** [no_nested_borrows::CONST1] *)
+Definition const1_body : result usize := usize_mul 2%usize 2%usize.
+Definition const1_c : usize := const1_body%global.
+
(** [no_nested_borrows::cast_test]: forward function *)
Definition cast_test (x : u32) : result i32 :=
scalar_cast U32 I32 x.
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
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index d6d603ce..c4a6a265 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -60,6 +60,18 @@ def div_test1 (x : U32) : Result U32 :=
def rem_test (x : U32) (y : U32) : Result U32 :=
x % y
+/- [no_nested_borrows::mul_test]: forward function -/
+def mul_test (x : U32) (y : U32) : Result U32 :=
+ x * y
+
+/- [no_nested_borrows::CONST0] -/
+def const0_body : Result Usize := 1#usize + 1#usize
+def const0_c : Usize := eval_global const0_body (by simp)
+
+/- [no_nested_borrows::CONST1] -/
+def const1_body : Result Usize := 2#usize * 2#usize
+def const1_c : Usize := eval_global const1_body (by simp)
+
/- [no_nested_borrows::cast_test]: forward function -/
def cast_test (x : U32) : Result I32 :=
Scalar.cast .I32 x