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/hol4/hashmap_main | |
| parent | 4f26c7f6f1e554d8ec2f46e868d5dc66c4160d16 (diff) | |
| parent | c4d2af051c18c4c81b1e57a45210c37c89c8330f (diff) | |
Merge pull request #213 from AeneasVerif/cleanup-tests
Diffstat (limited to 'tests/hol4/hashmap_main')
| -rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_FunsScript.sml | 4 | ||||
| -rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig | 4 | ||||
| -rw-r--r-- | tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml | 4 |
3 files changed, 6 insertions, 6 deletions
diff --git a/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml index c1e30aa6..2a17d185 100644 --- a/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml +++ b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml @@ -628,9 +628,9 @@ val insert_on_disk_fwd_def = Define ‘ insert_on_disk_fwd (key : usize) (value : u64) (st : state) : (state # unit) result = do - (st0, hm) <- hashmap_utils_deserialize_fwd st; + (st0, hm) <- utils_deserialize_fwd st; hm0 <- hashmap_hash_map_insert_fwd_back hm key value; - (st1, _) <- hashmap_utils_serialize_fwd hm0 st0; + (st1, _) <- utils_serialize_fwd hm0 st0; Return (st1, ()) od ’ diff --git a/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig index d4e43d9a..c19673bb 100644 --- a/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig +++ b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig @@ -583,9 +583,9 @@ sig ⊢ ∀key value st. insert_on_disk_fwd key value st = do - (st0,hm) <- hashmap_utils_deserialize_fwd st; + (st0,hm) <- utils_deserialize_fwd st; hm0 <- hashmap_hash_map_insert_fwd_back hm key value; - (st1,_) <- hashmap_utils_serialize_fwd hm0 st0; + (st1,_) <- utils_serialize_fwd hm0 st0; Return (st1,()) od diff --git a/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml index f7221d92..9c29c0e0 100644 --- a/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml +++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml @@ -6,10 +6,10 @@ open hashmapMain_TypesTheory val _ = new_theory "hashmapMain_Opaque" -(** [hashmap_main::hashmap_utils::deserialize]: forward function *)val _ = new_constant ("hashmap_utils_deserialize_fwd", +(** [hashmap_main::utils::deserialize]: forward function *)val _ = new_constant ("utils_deserialize_fwd", “:state -> (state # u64 hashmap_hash_map_t) result”) -(** [hashmap_main::hashmap_utils::serialize]: forward function *)val _ = new_constant ("hashmap_utils_serialize_fwd", +(** [hashmap_main::utils::serialize]: forward function *)val _ = new_constant ("utils_serialize_fwd", “:u64 hashmap_hash_map_t -> state -> (state # unit) result”) val _ = export_theory () |