diff options
| author | Sidney Congard | 2022-08-11 10:39:04 +0200 |
|---|---|---|
| committer | Sidney Congard | 2022-08-11 10:39:04 +0200 |
| commit | fa491861faed3ba5ed4fe806b55bea663a29579c (patch) | |
| tree | 05a4e268aedfdea0b14ac9e44f8ee66210aeae65 /tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst | |
| parent | cd754eabe3af025ca3465c5fc6d8cb48da66a1ae (diff) | |
Correct assertion for stateless globals
Diffstat (limited to '')
| -rw-r--r-- | tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst index 3c5ee819..0cf876d9 100644 --- a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst +++ b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst @@ -24,6 +24,10 @@ let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) : nat = admit () +(** [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]: decreases clause *) unfold let hashmap_hash_map_move_elements_from_list_decreases (t : Type0) |