From 530a5ae56209061f091bbcafee82de07039a8124 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 8 Nov 2023 14:28:44 +0100
Subject: Update the Makefile and regenerate some tests

---
 Makefile                             |  4 ++++
 tests/coq/misc/NoNestedBorrows.v     | 12 ++++++++++++
 tests/fstar/misc/NoNestedBorrows.fst | 12 ++++++++++++
 tests/lean/NoNestedBorrows.lean      | 12 ++++++++++++
 4 files changed, 40 insertions(+)

diff --git a/Makefile b/Makefile
index 694b47a3..486ba40e 100644
--- a/Makefile
+++ b/Makefile
@@ -143,6 +143,10 @@ thol4-traits: OPTIONS +=
 thol4-array:
 	echo "Ignoring the array test for HOL4"
 
+# TODO: activate the traits for all the backends
+thol4-traits:
+	echo "Ignoring the traits test for HOL4"
+
 trans-loops: OPTIONS += -no-state
 trans-loops: SUBDIR := misc
 tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
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
-- 
cgit v1.2.3