diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Funs.fst | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst index d01046ec..83bf80d1 100644 --- a/tests/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst @@ -198,6 +198,10 @@ let hashmap_hash_map_insert_no_resize_fwd_back end end +(** [core::num::u32::{8}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list] *) let rec hashmap_hash_map_move_elements_from_list_fwd_back (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t) : @@ -257,7 +261,7 @@ let rec hashmap_hash_map_move_elements_fwd_back (** [hashmap_main::hashmap::HashMap::{0}::try_resize] *) let hashmap_hash_map_try_resize_fwd_back (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) = - begin match scalar_cast U32 Usize 4294967295 with + begin match scalar_cast U32 Usize core_num_u32_max_c with | Fail -> Fail | Return max_usize -> let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in |