diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/misc/Loops.Clauses.Template.fst | 10 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 10 |
2 files changed, 10 insertions, 10 deletions
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst index 5d450275..7c77ad50 100644 --- a/tests/fstar/misc/Loops.Clauses.Template.fst +++ b/tests/fstar/misc/Loops.Clauses.Template.fst @@ -7,31 +7,31 @@ open Loops.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [loops::sum]: decreases clause - Source: 'tests/src/loops.rs', lines 8:0-18:1 *) + Source: 'tests/src/loops.rs', lines 10:4-18:1 *) unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () (** [loops::sum_with_mut_borrows]: decreases clause - Source: 'tests/src/loops.rs', lines 23:0-35:1 *) + Source: 'tests/src/loops.rs', lines 25:4-35:1 *) unfold let sum_with_mut_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () (** [loops::sum_with_shared_borrows]: decreases clause - Source: 'tests/src/loops.rs', lines 38:0-52:1 *) + Source: 'tests/src/loops.rs', lines 40:4-52:1 *) unfold let sum_with_shared_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () (** [loops::sum_array]: decreases clause - Source: 'tests/src/loops.rs', lines 54:0-62:1 *) + Source: 'tests/src/loops.rs', lines 56:4-62:1 *) unfold let sum_array_loop_decreases (n : usize) (a : array u32 n) (i : usize) (s : u32) : nat = admit () (** [loops::clear]: decreases clause - Source: 'tests/src/loops.rs', lines 66:0-72:1 *) + Source: 'tests/src/loops.rs', lines 67:4-72:1 *) unfold let clear_loop_decreases (v : alloc_vec_Vec u32) (i : usize) : nat = admit () diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 05e77046..b9d4468a 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -8,7 +8,7 @@ include Loops.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [loops::sum]: loop 0: - Source: 'tests/src/loops.rs', lines 8:0-18:1 *) + Source: 'tests/src/loops.rs', lines 10:4-18:1 *) let rec sum_loop (max : u32) (i : u32) (s : u32) : Tot (result u32) (decreases (sum_loop_decreases max i s)) @@ -23,7 +23,7 @@ let sum (max : u32) : result u32 = sum_loop max 0 0 (** [loops::sum_with_mut_borrows]: loop 0: - Source: 'tests/src/loops.rs', lines 23:0-35:1 *) + Source: 'tests/src/loops.rs', lines 25:4-35:1 *) let rec sum_with_mut_borrows_loop (max : u32) (i : u32) (s : u32) : Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max i s)) @@ -41,7 +41,7 @@ let sum_with_mut_borrows (max : u32) : result u32 = sum_with_mut_borrows_loop max 0 0 (** [loops::sum_with_shared_borrows]: loop 0: - Source: 'tests/src/loops.rs', lines 38:0-52:1 *) + Source: 'tests/src/loops.rs', lines 40:4-52:1 *) let rec sum_with_shared_borrows_loop (max : u32) (i : u32) (s : u32) : Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s)) @@ -59,7 +59,7 @@ let sum_with_shared_borrows (max : u32) : result u32 = sum_with_shared_borrows_loop max 0 0 (** [loops::sum_array]: loop 0: - Source: 'tests/src/loops.rs', lines 54:0-62:1 *) + Source: 'tests/src/loops.rs', lines 56:4-62:1 *) let rec sum_array_loop (n : usize) (a : array u32 n) (i : usize) (s : u32) : Tot (result u32) (decreases (sum_array_loop_decreases n a i s)) @@ -78,7 +78,7 @@ let sum_array (n : usize) (a : array u32 n) : result u32 = sum_array_loop n a 0 0 (** [loops::clear]: loop 0: - Source: 'tests/src/loops.rs', lines 66:0-72:1 *) + Source: 'tests/src/loops.rs', lines 67:4-72:1 *) let rec clear_loop (v : alloc_vec_Vec u32) (i : usize) : Tot (result (alloc_vec_Vec u32)) (decreases (clear_loop_decreases v i)) |