diff options
author | Guillaume Boisseau | 2024-05-28 11:56:39 +0200 |
---|---|---|
committer | GitHub | 2024-05-28 11:56:39 +0200 |
commit | ef7792c106a1f33397c206fcb5124b5ddfe64378 (patch) | |
tree | a72fae46702fc4c2eb32e1361a2538eb7a5f5545 /tests/fstar/hashmap/Hashmap.Clauses.Template.fst | |
parent | 4f26c7f6f1e554d8ec2f46e868d5dc66c4160d16 (diff) | |
parent | c4d2af051c18c4c81b1e57a45210c37c89c8330f (diff) |
Merge pull request #213 from AeneasVerif/cleanup-tests
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Clauses.Template.fst | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst index 3119ded8..57003613 100644 --- a/tests/fstar/hashmap/Hashmap.Clauses.Template.fst +++ b/tests/fstar/hashmap/Hashmap.Clauses.Template.fst @@ -7,63 +7,63 @@ open Hashmap.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: decreases clause - Source: 'tests/src/hashmap.rs', lines 58:4-64:5 *) + Source: 'tests/src/hashmap.rs', lines 60:4-66:5 *) unfold let hashMap_allocate_slots_loop_decreases (t : Type0) (slots : alloc_vec_Vec (list_t t)) (n : usize) : nat = admit () (** [hashmap::{hashmap::HashMap<T>}::clear]: decreases clause - Source: 'tests/src/hashmap.rs', lines 88:4-96:5 *) + Source: 'tests/src/hashmap.rs', lines 90:4-98:5 *) unfold let hashMap_clear_loop_decreases (t : Type0) (slots : alloc_vec_Vec (list_t t)) (i : usize) : nat = admit () (** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 105:4-122:5 *) + Source: 'tests/src/hashmap.rs', lines 107:4-124:5 *) unfold let hashMap_insert_in_list_loop_decreases (t : Type0) (key : usize) (value : t) (ls : list_t t) : nat = admit () (** [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 191:4-204:5 *) + Source: 'tests/src/hashmap.rs', lines 193:4-206:5 *) unfold let hashMap_move_elements_from_list_loop_decreases (t : Type0) (ntable : hashMap_t t) (ls : list_t t) : nat = admit () (** [hashmap::{hashmap::HashMap<T>}::move_elements]: decreases clause - Source: 'tests/src/hashmap.rs', lines 179:4-188:5 *) + Source: 'tests/src/hashmap.rs', lines 181:4-190:5 *) unfold let hashMap_move_elements_loop_decreases (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (list_t t)) (i : usize) : nat = admit () (** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 214:4-227:5 *) + Source: 'tests/src/hashmap.rs', lines 216:4-229:5 *) unfold let hashMap_contains_key_in_list_loop_decreases (t : Type0) (key : usize) (ls : list_t t) : nat = admit () (** [hashmap::{hashmap::HashMap<T>}::get_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 232:4-245:5 *) + Source: 'tests/src/hashmap.rs', lines 234:4-247:5 *) unfold let hashMap_get_in_list_loop_decreases (t : Type0) (key : usize) (ls : list_t t) : nat = admit () (** [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 253:4-262:5 *) + Source: 'tests/src/hashmap.rs', lines 255:4-264:5 *) unfold let hashMap_get_mut_in_list_loop_decreases (t : Type0) (ls : list_t t) (key : usize) : nat = admit () (** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: decreases clause - Source: 'tests/src/hashmap.rs', lines 273:4-299:5 *) + Source: 'tests/src/hashmap.rs', lines 275:4-301:5 *) unfold let hashMap_remove_from_list_loop_decreases (t : Type0) (key : usize) (ls : list_t t) : nat = |