summaryrefslogtreecommitdiff
path: root/tests/src/hashmap_main.rs
diff options
context:
space:
mode:
authorNadrieril2024-05-27 14:59:10 +0200
committerNadrieril2024-05-27 17:22:56 +0200
commit2b40c5c3de1ee2caca2c0072f812fea04b5a0238 (patch)
tree687a640232f17269ad33f1a841817491962d4de9 /tests/src/hashmap_main.rs
parent4f26c7f6f1e554d8ec2f46e868d5dc66c4160d16 (diff)
tests: Merge the hashmap test files
Diffstat (limited to '')
-rw-r--r--tests/src/hashmap_main.rs22
1 files changed, 0 insertions, 22 deletions
diff --git a/tests/src/hashmap_main.rs b/tests/src/hashmap_main.rs
deleted file mode 100644
index 0c827844..00000000
--- a/tests/src/hashmap_main.rs
+++ /dev/null
@@ -1,22 +0,0 @@
-//@ charon-args=--opaque=hashmap_utils
-//@ aeneas-args=-state -split-files
-//@ [coq] aeneas-args=-use-fuel
-//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
-// Possible to add `--no-code-duplication` if we use the optimized MIR
-// TODO: reactivate -test-trans-units
-mod hashmap;
-mod hashmap_utils;
-
-use crate::hashmap::*;
-use crate::hashmap_utils::*;
-
-pub fn insert_on_disk(key: Key, value: u64) {
- // Deserialize
- let mut hm = deserialize();
- // Update
- hm.insert(key, value);
- // Serialize
- serialize(hm);
-}
-
-pub fn main() {}