diff options
Diffstat (limited to 'tests/src/hashmap.rs')
-rw-r--r-- | tests/src/hashmap.rs | 29 |
1 files changed, 28 insertions, 1 deletions
diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs index 4552e4f2..ccb96e1e 100644 --- a/tests/src/hashmap.rs +++ b/tests/src/hashmap.rs @@ -1,9 +1,11 @@ +//@ charon-args=--opaque=hashmap_utils +//@ aeneas-args=-state -split-files //@ [coq] aeneas-args=-use-fuel -//@ aeneas-args=-split-files //@ [fstar] aeneas-args=-decreases-clauses -template-clauses //@ [lean] aeneas-args=-no-gen-lib-entry // ^ the `-no-gen-lib-entry` is because we add a custom import in the Hashmap.lean file: we do not // want to overwrite it. +// Possible to add `--no-code-duplication` if we use the optimized MIR // TODO: reactivate -test-trans-units //! A hashmap implementation. @@ -314,6 +316,31 @@ impl<T> HashMap<T> { } } +// This is a module so we can tell charon to leave it opaque +mod hashmap_utils { + use crate::*; + + /// Serialize a hash map - we don't have traits, so we fix the type of the + /// values (this is not the interesting part anyway) + pub(crate) fn serialize(_hm: HashMap<u64>) { + unimplemented!(); + } + /// Deserialize a hash map - we don't have traits, so we fix the type of the + /// values (this is not the interesting part anyway) + pub(crate) fn deserialize() -> HashMap<u64> { + unimplemented!(); + } +} + +pub fn insert_on_disk(key: Key, value: u64) { + // Deserialize + let mut hm = hashmap_utils::deserialize(); + // Update + hm.insert(key, value); + // Serialize + hashmap_utils::serialize(hm); +} + /// I currently can't retrieve functions marked with the attribute #[test], /// while I want to extract the unit tests and use the normalize on them, /// so I have to define the test functions somewhere and call them from |