summaryrefslogtreecommitdiff
path: root/tests/fstar/misc
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/misc')
-rw-r--r--tests/fstar/misc/Loops.Clauses.Template.fst13
-rw-r--r--tests/fstar/misc/Loops.Clauses.fst14
-rw-r--r--tests/fstar/misc/Loops.Funs.fst56
3 files changed, 83 insertions, 0 deletions
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst
index 244761d3..c8ed16f4 100644
--- a/tests/fstar/misc/Loops.Clauses.Template.fst
+++ b/tests/fstar/misc/Loops.Clauses.Template.fst
@@ -136,3 +136,16 @@ let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0)
(ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat =
admit ()
+(** [loops::ignore_input_mut_borrow]: decreases clause
+ Source: 'src/loops.rs', lines 345:0-349:1 *)
+unfold let ignore_input_mut_borrow_loop_decreases (i : u32) : nat = admit ()
+
+(** [loops::incr_ignore_input_mut_borrow]: decreases clause
+ Source: 'src/loops.rs', lines 353:0-358:1 *)
+unfold
+let incr_ignore_input_mut_borrow_loop_decreases (i : u32) : nat = admit ()
+
+(** [loops::ignore_input_shared_borrow]: decreases clause
+ Source: 'src/loops.rs', lines 362:0-366:1 *)
+unfold let ignore_input_shared_borrow_loop_decreases (i : u32) : nat = admit ()
+
diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst
index 13f5513d..7d3c3ae6 100644
--- a/tests/fstar/misc/Loops.Clauses.fst
+++ b/tests/fstar/misc/Loops.Clauses.fst
@@ -110,3 +110,17 @@ unfold
let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0) (l : list_t t)
(l0 : list_t t) (i : u32) : list_t t =
l
+
+(** [loops::ignore_input_mut_borrow]: decreases clause
+ Source: 'src/loops.rs', lines 345:0-349:1 *)
+unfold let ignore_input_mut_borrow_loop_decreases (i : u32) : nat = i
+
+(** [loops::incr_ignore_input_mut_borrow]: decreases clause
+ Source: 'src/loops.rs', lines 353:0-358:1 *)
+unfold
+let incr_ignore_input_mut_borrow_loop_decreases (i : u32) : nat = i
+
+(** [loops::ignore_input_shared_borrow]: decreases clause
+ Source: 'src/loops.rs', lines 362:0-366:1 *)
+unfold let ignore_input_shared_borrow_loop_decreases (i : u32) : nat = i
+
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 209c48cd..5f24fe7a 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -548,3 +548,59 @@ let list_nth_shared_mut_loop_pair_merge
let* (p, back_'a) = list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i in
Return (p, back_'a)
+(** [loops::ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 345:0-349:1 *)
+let rec ignore_input_mut_borrow_loop
+ (i : u32) :
+ Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i))
+ =
+ if i > 0
+ then
+ let* i1 = u32_sub i 1 in
+ let* _ = ignore_input_mut_borrow_loop i1 in
+ Return ()
+ else Return ()
+
+(** [loops::ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 345:0-345:56 *)
+let ignore_input_mut_borrow (_a : u32) (i : u32) : result u32 =
+ let* _ = ignore_input_mut_borrow_loop i in Return _a
+
+(** [loops::incr_ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 353:0-358:1 *)
+let rec incr_ignore_input_mut_borrow_loop
+ (i : u32) :
+ Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i))
+ =
+ if i > 0
+ then
+ let* i1 = u32_sub i 1 in
+ let* _ = incr_ignore_input_mut_borrow_loop i1 in
+ Return ()
+ else Return ()
+
+(** [loops::incr_ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 353:0-353:60 *)
+let incr_ignore_input_mut_borrow (a : u32) (i : u32) : result u32 =
+ let* a1 = u32_add a 1 in
+ let* _ = incr_ignore_input_mut_borrow_loop i in
+ Return a1
+
+(** [loops::ignore_input_shared_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 362:0-366:1 *)
+let rec ignore_input_shared_borrow_loop
+ (i : u32) :
+ Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i))
+ =
+ if i > 0
+ then
+ let* i1 = u32_sub i 1 in
+ let* _ = ignore_input_shared_borrow_loop i1 in
+ Return ()
+ else Return ()
+
+(** [loops::ignore_input_shared_borrow]:
+ Source: 'src/loops.rs', lines 362:0-362:59 *)
+let ignore_input_shared_borrow (_a : u32) (i : u32) : result u32 =
+ let* _ = ignore_input_shared_borrow_loop i in Return _a
+