summaryrefslogtreecommitdiff
path: root/tests/coq/misc/NoNestedBorrows.v
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/misc/NoNestedBorrows.v112
1 files changed, 57 insertions, 55 deletions
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 96d62711..470a2cde 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -45,47 +45,47 @@ Inductive Sum_t (T1 T2 : Type) :=
Arguments SumLeft {T1} {T2} _.
Arguments SumRight {T1} {T2} _.
-(** [no_nested_borrows::neg_test] *)
+(** [no_nested_borrows::neg_test]: forward function *)
Definition neg_test_fwd (x : i32) : result i32 :=
i32_neg x.
-(** [no_nested_borrows::add_test] *)
+(** [no_nested_borrows::add_test]: forward function *)
Definition add_test_fwd (x : u32) (y : u32) : result u32 :=
u32_add x y.
-(** [no_nested_borrows::subs_test] *)
+(** [no_nested_borrows::subs_test]: forward function *)
Definition subs_test_fwd (x : u32) (y : u32) : result u32 :=
u32_sub x y.
-(** [no_nested_borrows::div_test] *)
+(** [no_nested_borrows::div_test]: forward function *)
Definition div_test_fwd (x : u32) (y : u32) : result u32 :=
u32_div x y.
-(** [no_nested_borrows::div_test1] *)
+(** [no_nested_borrows::div_test1]: forward function *)
Definition div_test1_fwd (x : u32) : result u32 :=
u32_div x 2%u32.
-(** [no_nested_borrows::rem_test] *)
+(** [no_nested_borrows::rem_test]: forward function *)
Definition rem_test_fwd (x : u32) (y : u32) : result u32 :=
u32_rem x y.
-(** [no_nested_borrows::cast_test] *)
+(** [no_nested_borrows::cast_test]: forward function *)
Definition cast_test_fwd (x : u32) : result i32 :=
scalar_cast U32 I32 x.
-(** [no_nested_borrows::test2] *)
+(** [no_nested_borrows::test2]: forward function *)
Definition test2_fwd : result unit :=
_ <- u32_add 23%u32 44%u32; Return tt.
(** Unit test for [no_nested_borrows::test2] *)
Check (test2_fwd )%return.
-(** [no_nested_borrows::get_max] *)
+(** [no_nested_borrows::get_max]: forward function *)
Definition get_max_fwd (x : u32) (y : u32) : result u32 :=
if x s>= y then Return x else Return y
.
-(** [no_nested_borrows::test3] *)
+(** [no_nested_borrows::test3]: forward function *)
Definition test3_fwd : result unit :=
x <- get_max_fwd 4%u32 3%u32;
y <- get_max_fwd 10%u32 11%u32;
@@ -96,7 +96,7 @@ Definition test3_fwd : result unit :=
(** Unit test for [no_nested_borrows::test3] *)
Check (test3_fwd )%return.
-(** [no_nested_borrows::test_neg1] *)
+(** [no_nested_borrows::test_neg1]: forward function *)
Definition test_neg1_fwd : result unit :=
y <- i32_neg 3%i32; if negb (y s= (-3)%i32) then Fail_ Failure else Return tt
.
@@ -104,7 +104,7 @@ Definition test_neg1_fwd : result unit :=
(** Unit test for [no_nested_borrows::test_neg1] *)
Check (test_neg1_fwd )%return.
-(** [no_nested_borrows::refs_test1] *)
+(** [no_nested_borrows::refs_test1]: forward function *)
Definition refs_test1_fwd : result unit :=
if negb (1%i32 s= 1%i32) then Fail_ Failure else Return tt
.
@@ -112,7 +112,7 @@ Definition refs_test1_fwd : result unit :=
(** Unit test for [no_nested_borrows::refs_test1] *)
Check (refs_test1_fwd )%return.
-(** [no_nested_borrows::refs_test2] *)
+(** [no_nested_borrows::refs_test2]: forward function *)
Definition refs_test2_fwd : result unit :=
if negb (2%i32 s= 2%i32)
then Fail_ Failure
@@ -128,14 +128,14 @@ Definition refs_test2_fwd : result unit :=
(** Unit test for [no_nested_borrows::refs_test2] *)
Check (refs_test2_fwd )%return.
-(** [no_nested_borrows::test_list1] *)
+(** [no_nested_borrows::test_list1]: forward function *)
Definition test_list1_fwd : result unit :=
Return tt.
(** Unit test for [no_nested_borrows::test_list1] *)
Check (test_list1_fwd )%return.
-(** [no_nested_borrows::test_box1] *)
+(** [no_nested_borrows::test_box1]: forward function *)
Definition test_box1_fwd : result unit :=
let b := 1%i32 in
let x := b in
@@ -145,21 +145,21 @@ Definition test_box1_fwd : result unit :=
(** Unit test for [no_nested_borrows::test_box1] *)
Check (test_box1_fwd )%return.
-(** [no_nested_borrows::copy_int] *)
+(** [no_nested_borrows::copy_int]: forward function *)
Definition copy_int_fwd (x : i32) : result i32 :=
Return x.
-(** [no_nested_borrows::test_unreachable] *)
+(** [no_nested_borrows::test_unreachable]: forward function *)
Definition test_unreachable_fwd (b : bool) : result unit :=
if b then Fail_ Failure else Return tt
.
-(** [no_nested_borrows::test_panic] *)
+(** [no_nested_borrows::test_panic]: forward function *)
Definition test_panic_fwd (b : bool) : result unit :=
if b then Fail_ Failure else Return tt
.
-(** [no_nested_borrows::test_copy_int] *)
+(** [no_nested_borrows::test_copy_int]: forward function *)
Definition test_copy_int_fwd : result unit :=
y <- copy_int_fwd 0%i32;
if negb (0%i32 s= y) then Fail_ Failure else Return tt
@@ -168,12 +168,12 @@ Definition test_copy_int_fwd : result unit :=
(** Unit test for [no_nested_borrows::test_copy_int] *)
Check (test_copy_int_fwd )%return.
-(** [no_nested_borrows::is_cons] *)
+(** [no_nested_borrows::is_cons]: forward function *)
Definition is_cons_fwd (T : Type) (l : List_t T) : result bool :=
match l with | ListCons t l0 => Return true | ListNil => Return false end
.
-(** [no_nested_borrows::test_is_cons] *)
+(** [no_nested_borrows::test_is_cons]: forward function *)
Definition test_is_cons_fwd : result unit :=
let l := ListNil in
b <- is_cons_fwd i32 (ListCons 0%i32 l);
@@ -183,7 +183,7 @@ Definition test_is_cons_fwd : result unit :=
(** Unit test for [no_nested_borrows::test_is_cons] *)
Check (test_is_cons_fwd )%return.
-(** [no_nested_borrows::split_list] *)
+(** [no_nested_borrows::split_list]: forward function *)
Definition split_list_fwd
(T : Type) (l : List_t T) : result (T * (List_t T)) :=
match l with
@@ -192,7 +192,7 @@ Definition split_list_fwd
end
.
-(** [no_nested_borrows::test_split_list] *)
+(** [no_nested_borrows::test_split_list]: forward function *)
Definition test_split_list_fwd : result unit :=
let l := ListNil in
p <- split_list_fwd i32 (ListCons 0%i32 l);
@@ -203,18 +203,18 @@ Definition test_split_list_fwd : result unit :=
(** Unit test for [no_nested_borrows::test_split_list] *)
Check (test_split_list_fwd )%return.
-(** [no_nested_borrows::choose] *)
+(** [no_nested_borrows::choose]: forward function *)
Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T :=
if b then Return x else Return y
.
-(** [no_nested_borrows::choose] *)
+(** [no_nested_borrows::choose]: backward function 0 *)
Definition choose_back
(T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) :=
if b then Return (ret, y) else Return (x, ret)
.
-(** [no_nested_borrows::choose_test] *)
+(** [no_nested_borrows::choose_test]: forward function *)
Definition choose_test_fwd : result unit :=
z <- choose_fwd i32 true 0%i32 0%i32;
z0 <- i32_add z 1%i32;
@@ -231,7 +231,7 @@ Definition choose_test_fwd : result unit :=
(** Unit test for [no_nested_borrows::choose_test] *)
Check (choose_test_fwd )%return.
-(** [no_nested_borrows::test_char] *)
+(** [no_nested_borrows::test_char]: forward function *)
Definition test_char_fwd : result char :=
Return (char_of_byte Coq.Init.Byte.x61)
.
@@ -253,7 +253,7 @@ Arguments NodeElemNil {T}.
Arguments TreeLeaf {T} _.
Arguments TreeNode {T} _ _ _.
-(** [no_nested_borrows::list_length] *)
+(** [no_nested_borrows::list_length]: forward function *)
Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
match l with
| ListCons t l1 => i <- list_length_fwd T l1; u32_add 1%u32 i
@@ -261,7 +261,7 @@ Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
end
.
-(** [no_nested_borrows::list_nth_shared] *)
+(** [no_nested_borrows::list_nth_shared]: forward function *)
Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
match l with
| ListCons x tl =>
@@ -272,7 +272,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
end
.
-(** [no_nested_borrows::list_nth_mut] *)
+(** [no_nested_borrows::list_nth_mut]: forward function *)
Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
match l with
| ListCons x tl =>
@@ -283,7 +283,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
end
.
-(** [no_nested_borrows::list_nth_mut] *)
+(** [no_nested_borrows::list_nth_mut]: backward function 0 *)
Fixpoint list_nth_mut_back
(T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) :=
match l with
@@ -298,7 +298,7 @@ Fixpoint list_nth_mut_back
end
.
-(** [no_nested_borrows::list_rev_aux] *)
+(** [no_nested_borrows::list_rev_aux]: forward function *)
Fixpoint list_rev_aux_fwd
(T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) :=
match li with
@@ -307,13 +307,14 @@ Fixpoint list_rev_aux_fwd
end
.
-(** [no_nested_borrows::list_rev] *)
+(** [no_nested_borrows::list_rev]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition list_rev_fwd_back (T : Type) (l : List_t T) : result (List_t T) :=
let li := mem_replace_fwd (List_t T) l ListNil in
list_rev_aux_fwd T li ListNil
.
-(** [no_nested_borrows::test_list_functions] *)
+(** [no_nested_borrows::test_list_functions]: forward function *)
Definition test_list_functions_fwd : result unit :=
let l := ListNil in
let l0 := ListCons 2%i32 l in
@@ -350,61 +351,61 @@ Definition test_list_functions_fwd : result unit :=
(** Unit test for [no_nested_borrows::test_list_functions] *)
Check (test_list_functions_fwd )%return.
-(** [no_nested_borrows::id_mut_pair1] *)
+(** [no_nested_borrows::id_mut_pair1]: forward function *)
Definition id_mut_pair1_fwd
(T1 T2 : Type) (x : T1) (y : T2) : result (T1 * T2) :=
Return (x, y)
.
-(** [no_nested_borrows::id_mut_pair1] *)
+(** [no_nested_borrows::id_mut_pair1]: backward function 0 *)
Definition id_mut_pair1_back
(T1 T2 : Type) (x : T1) (y : T2) (ret : (T1 * T2)) : result (T1 * T2) :=
let (t, t0) := ret in Return (t, t0)
.
-(** [no_nested_borrows::id_mut_pair2] *)
+(** [no_nested_borrows::id_mut_pair2]: forward function *)
Definition id_mut_pair2_fwd
(T1 T2 : Type) (p : (T1 * T2)) : result (T1 * T2) :=
let (t, t0) := p in Return (t, t0)
.
-(** [no_nested_borrows::id_mut_pair2] *)
+(** [no_nested_borrows::id_mut_pair2]: backward function 0 *)
Definition id_mut_pair2_back
(T1 T2 : Type) (p : (T1 * T2)) (ret : (T1 * T2)) : result (T1 * T2) :=
let (t, t0) := ret in Return (t, t0)
.
-(** [no_nested_borrows::id_mut_pair3] *)
+(** [no_nested_borrows::id_mut_pair3]: forward function *)
Definition id_mut_pair3_fwd
(T1 T2 : Type) (x : T1) (y : T2) : result (T1 * T2) :=
Return (x, y)
.
-(** [no_nested_borrows::id_mut_pair3] *)
+(** [no_nested_borrows::id_mut_pair3]: backward function 0 *)
Definition id_mut_pair3_back'a
(T1 T2 : Type) (x : T1) (y : T2) (ret : T1) : result T1 :=
Return ret
.
-(** [no_nested_borrows::id_mut_pair3] *)
+(** [no_nested_borrows::id_mut_pair3]: backward function 1 *)
Definition id_mut_pair3_back'b
(T1 T2 : Type) (x : T1) (y : T2) (ret : T2) : result T2 :=
Return ret
.
-(** [no_nested_borrows::id_mut_pair4] *)
+(** [no_nested_borrows::id_mut_pair4]: forward function *)
Definition id_mut_pair4_fwd
(T1 T2 : Type) (p : (T1 * T2)) : result (T1 * T2) :=
let (t, t0) := p in Return (t, t0)
.
-(** [no_nested_borrows::id_mut_pair4] *)
+(** [no_nested_borrows::id_mut_pair4]: backward function 0 *)
Definition id_mut_pair4_back'a
(T1 T2 : Type) (p : (T1 * T2)) (ret : T1) : result T1 :=
Return ret
.
-(** [no_nested_borrows::id_mut_pair4] *)
+(** [no_nested_borrows::id_mut_pair4]: backward function 1 *)
Definition id_mut_pair4_back'b
(T1 T2 : Type) (p : (T1 * T2)) (ret : T2) : result T2 :=
Return ret
@@ -420,17 +421,17 @@ mkStruct_with_tuple_t {
Arguments mkStruct_with_tuple_t {T1} {T2} _.
Arguments Struct_with_tuple_p {T1} {T2}.
-(** [no_nested_borrows::new_tuple1] *)
+(** [no_nested_borrows::new_tuple1]: forward function *)
Definition new_tuple1_fwd : result (Struct_with_tuple_t u32 u32) :=
Return {| Struct_with_tuple_p := (1%u32, 2%u32) |}
.
-(** [no_nested_borrows::new_tuple2] *)
+(** [no_nested_borrows::new_tuple2]: forward function *)
Definition new_tuple2_fwd : result (Struct_with_tuple_t i16 i16) :=
Return {| Struct_with_tuple_p := (1%i16, 2%i16) |}
.
-(** [no_nested_borrows::new_tuple3] *)
+(** [no_nested_borrows::new_tuple3]: forward function *)
Definition new_tuple3_fwd : result (Struct_with_tuple_t u64 i64) :=
Return {| Struct_with_tuple_p := (1%u64, 2%i64) |}
.
@@ -445,12 +446,12 @@ mkStruct_with_pair_t {
Arguments mkStruct_with_pair_t {T1} {T2} _.
Arguments Struct_with_pair_p {T1} {T2}.
-(** [no_nested_borrows::new_pair1] *)
+(** [no_nested_borrows::new_pair1]: forward function *)
Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) :=
Return {| Struct_with_pair_p := {| Pair_x := 1%u32; Pair_y := 2%u32 |} |}
.
-(** [no_nested_borrows::test_constants] *)
+(** [no_nested_borrows::test_constants]: forward function *)
Definition test_constants_fwd : result unit :=
swt <- new_tuple1_fwd;
let (i, _) := swt.(Struct_with_tuple_p) in
@@ -476,34 +477,35 @@ Definition test_constants_fwd : result unit :=
(** Unit test for [no_nested_borrows::test_constants] *)
Check (test_constants_fwd )%return.
-(** [no_nested_borrows::test_weird_borrows1] *)
+(** [no_nested_borrows::test_weird_borrows1]: forward function *)
Definition test_weird_borrows1_fwd : result unit :=
Return tt.
(** Unit test for [no_nested_borrows::test_weird_borrows1] *)
Check (test_weird_borrows1_fwd )%return.
-(** [no_nested_borrows::test_mem_replace] *)
+(** [no_nested_borrows::test_mem_replace]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) *)
Definition test_mem_replace_fwd_back (px : u32) : result u32 :=
let y := mem_replace_fwd u32 px 1%u32 in
if negb (y s= 0%u32) then Fail_ Failure else Return 2%u32
.
-(** [no_nested_borrows::test_shared_borrow_bool1] *)
+(** [no_nested_borrows::test_shared_borrow_bool1]: forward function *)
Definition test_shared_borrow_bool1_fwd (b : bool) : result u32 :=
if b then Return 0%u32 else Return 1%u32
.
-(** [no_nested_borrows::test_shared_borrow_bool2] *)
+(** [no_nested_borrows::test_shared_borrow_bool2]: forward function *)
Definition test_shared_borrow_bool2_fwd : result u32 :=
Return 0%u32.
-(** [no_nested_borrows::test_shared_borrow_enum1] *)
+(** [no_nested_borrows::test_shared_borrow_enum1]: forward function *)
Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 :=
match l with | ListCons i l0 => Return 1%u32 | ListNil => Return 0%u32 end
.
-(** [no_nested_borrows::test_shared_borrow_enum2] *)
+(** [no_nested_borrows::test_shared_borrow_enum2]: forward function *)
Definition test_shared_borrow_enum2_fwd : result u32 :=
Return 0%u32.
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-24 02:20:31 +0000